|
|||||
|
|
| 应用时序逻辑分析密钥分配协议 | |
| 引用本文： | 肖德琴,林丕源,周权,张焕国. 应用时序逻辑分析密钥分配协议[J]. 小型微型计算机系统, 2002, 23(11): 1340-1343 |
| 作者姓名： | 肖德琴 林丕源 周权 张焕国 |
| 作者单位： | 1. 华南农业大学,理学院,计算机系,广东,广州,510642;中国科学院,研究生院,信息安全国家重点实验室,北京,100080 2. 华南农业大学,理学院,计算机系,广东,广州,510642 3. 广州大学理学院,数学系,信息安全研究所,广东,广州,510405 4. 武汉大学,数学与计算机科学学院,湖北,武汉,430072 |
| 基金项目： | 国家自然科学基金 (编号 199310 10和 6 6 9730 34)资助 |
| 摘 要： | 文中 ,在密码系统状态间的关联性和时序逻辑的可达性间建立联系 ,探讨了一种基于时序逻辑的密钥分配协议的描述办法 .该途径从形式上规定密码设备的构成成分以及有关的密码操作 ,使用了时序逻辑的常量和状态不变量来表达这些构成成分 .有关的密码操作表达为状态转换 ,加密协议应保留的必要特性表达为临界不变性表达式 ,然后验证这些不变性表达式 .本方法的优点在于可以隐式地刻画攻击者的行为 ,具有形式化程度高等特点 .我们希望能为研究规范化、简洁化的形式化分析工具提供一些借鉴 . |
| 关 键 词： | 密钥分配协议 协议分析 时序逻辑 |
| 文章编号： | 1000-1220(2002)11-1340-04 |
Analysis Key Distribution Protocols Using Temporal Logic |
|
| XIAO De-qin ,,LIN Pi-yuan,ZHOU Quan ,ZHANG Huan-guo. Analysis Key Distribution Protocols Using Temporal Logic[J]. Mini-micro Systems, 2002, 23(11): 1340-1343 | |
| Authors: | XIAO De-qin LIN Pi-yuan ZHOU Quan ZHANG Huan-guo |
| Affiliation: | XIAO De-qin 1,2,LIN Pi-yuan,ZHOU Quan 3,ZHANG Huan-guo 4 1 |
| Abstract: | In this paper, we made related states contact with the reachability of temporal logic. We proposed formal method to model Key distribution Protocols' properties using the theory of Temporal Logic. It defined encryption device and encryption device and encryption operators in formally. For example, we used temporal logic constants and status invariable to express these factors. Those encryption operators were expressed by states' transitions. Those security conditions were been expressed by some invariant expressions, then proved those expressions. This method can specify intruders' actions stealthily, we argue that using standard temporal logic provides greater formally in the verification results. We hope to provide some help for researching standardization and simplification formal tools. |
| Keywords: | distribution protocols protocol analysis temporal logic |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |
