一种复合协议验证逻辑模型  

Logic model for formal analysis of composed protocols

作　　者：赵娟[1] 韩继红[1] 王亚弟[1] 黄卿[1] 朱玉娜[2] 

机构地区：[1]解放军信息工程大学电子技术学院 [2]91033部队

出　　处：《计算机应用研究》2010年第1期274-277,共4页Application Research of Computers

摘　　要：针对协议复合时需要解决的问题,研究提出一种复合协议验证逻辑模型,给出了协议描述、逻辑语法、逻辑语义和相应的证明系统,对协议的秘密性和认证性进行建模,将协议复合分为并行复合和顺序复合,并提出相应的协议复合定理。最后以IKEv2协议为例进行分析,证明了IKEv2两个分别安全的阶段子协议复合后还是安全的。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.

关 键 词：复合协议 形式化分析 逻辑模型 并行复合 顺序复合 IKEV2协议 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]