Logic model for formal analysis of composed protocols
Zhu Yu-na · Jisuanji yingyong yanjiu · 2010
Aiming at the problems in analyzing composed protocols,this paper presented a logic model for formal analysis of composed protocols with its protocol specification,logic syntax,logic semantics and corresponding proof system.It defined secrecy and authentication properties,classify protocol composition into parallel composition and sequential composition,and proposed the corresponding composition theorems.At last,it discussed the IKEv2 protocol and the result shows that the IKEv2 protocol composed of two safe sub-protocols is safe.