| 一种基于规划理论的密码协议形式模型 |
| |
| 引用本文： | 赵宇,王亚弟,韩继红,范钰丹,张超.一种基于规划理论的密码协议形式模型[J].计算机研究与发展,2008,45(9). |
| |
| 作者姓名： | 赵宇 王亚弟 韩继红 范钰丹 张超 |
| |
| 作者单位： | 解放军信息工程大学电子技术学院,郑州,450004 |
| |
| 摘 要： | 将规划理论引入到密码协议形式化分析领域,结合密码协议在实际网络环境中的运行特点和规律,提出了密码协议攻击规划理论;建立了一种对密码协议进行安全性验证的形式化模型,即密码协议攻击规划问题模型;给出了模型的一阶语法、形式定义及相关运算语义.同时,分析了Dolev-Yao模型的不足之处,基于基本消息元素策略对其进行了改进;并通过增强应用语义来保证改进模型的可行性,从而避免了"状态空间爆炸"问题的发生,提高了密码协议攻击规划问题模型的完备性;并给出了基于该模型的NS公钥协议分析实例.提出的密码协议形式模型是证伪的,目的在于对密码协议进行验证,并查找协议中可能存在的漏洞,既可以方便地进行手工推导证明,也非常易于自动化实现.
|
| 关 键 词： | 密码协议 形式化模型 规划系统 规划问题 基本消息元素 |
A Formal Model for Cryptographic Protocols Based on Planning Theory |
| |
| Zhao Yu,Wang Yadi,Han Jihong,Fan Yudan,Zhang Chao.A Formal Model for Cryptographic Protocols Based on Planning Theory[J].Journal of Computer Research and Development,2008,45(9). |
| |
| Authors: | Zhao Yu Wang Yadi Han Jihong Fan Yudan Zhang Chao |
| |
| Affiliation: | Zhao Yu,Wang Yadi,Han Jihong,Fan Yudan,, Zhang Chao(Institute of Electronic Technique,Information Engineering University of the PLA,Zhengzhou 450004) |
| |
| Abstract: | Planning theory is brought into the area of formal analysis for cryptographic protocols. Based on the running characteristics and laws of cryptographic protocols in the real networks, an attack planning theory for cryptographic protocols is presented, and a formal model, namely attack planning problem model of cryptographic protocols, is established for verifying the security properties of cryptographic protocols, including its first-order syntax, formal definitions and operational semantics. Meanwhile, the... |
| |
| Keywords: | cryptographic protocol formal model planning system planning problem basic message element |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
