| 一种复合协议验证逻辑模型 |
| |
| 引用本文： | 赵娟,韩继红,王亚弟,黄卿,朱玉娜.一种复合协议验证逻辑模型[J].计算机应用研究,2010,27(1):274-277. |
| |
| 作者姓名： | 赵娟 韩继红 王亚弟 黄卿 朱玉娜 |
| |
| 作者单位： | 1. 解放军信息工程大学,电子技术学院,郑州,450004
2. 91033部队,山东,青岛,266101 |
| |
| 摘 要： | 针对协议复合时需要解决的问题，研究提出一种复合协议验证逻辑模型，给出了协议描述、逻辑语法、逻辑语义和相应的证明系统，对协议的秘密性和认证性进行建模，将协议复合分为并行复合和顺序复合，并提出相应的协议复合定理。最后以IKEv2协议为例进行分析，证明了IKEv2两个分别安全的阶段子协议复合后还是安全的。
|
| 关 键 词： | 复合协议 形式化分析 逻辑模型 并行复合 顺序复合 IKEv2协议 |
Logic model for formal analysis of composed protocols |
| |
| ZHAO Juan,HAN Ji-hong,WANG Ya-di,HUANG Qing,ZHU Yu-na.Logic model for formal analysis of composed protocols[J].Application Research of Computers,2010,27(1):274-277. |
| |
| Authors: | ZHAO Juan HAN Ji-hong WANG Ya-di HUANG Qing ZHU Yu-na |
| |
| Affiliation: | (1.Institute of Electronic Technology, PLA Information Engineering University, Zhengzhou 450004, China;2.91033 Unit, Qingdao Shandong 266101, China) |
| |
| Abstract: | 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. |
| |
| Keywords: | composed protocols formal analysis logic model parallel composition sequential composition IKEv2 protocol |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《计算机应用研究》浏览原始摘要信息 |
|
点击此处可从《计算机应用研究》下载全文 |
|
