一种基于规划理论的密码协议形式模型

• 作者: 张超 王亚弟 范钰丹 赵宇 韩继红
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: 密码协议 形式化模型 规划系统 规划问题 基本消息元素
• 年，卷（期）: 2008,（9）
• 所属期刊栏目: 信息安全
• 页码范围: 1567-1577
• 页数: 11页
• 分类号: TP309
• 字数: 11482字
• 语种: 中文

摘要

将规划理论引入到密码协议形式化分析领域,结合密码协议在实际网络环境中的运行特点和规律,提出了密码协议攻击规划理论;建立了一种对密码协议进行安全性验证的形式化模型,即密码协议攻击规划问题模型;给出了模型的一阶语法、形式定义及相关运算语义.同时,分析了Dolev-Yao模型的不足之处,基于基本消息元素策略对其进行了改进;并通过增强应用语义来保证改进模型的可行性,从而避免了"状态空间爆炸"问题的发生,提高了密码协议攻击规划问题模型的完备性;并给出了基于该模型的NS公钥协议分析实例.提出的密码协议形式模型是证伪的,目的在于对密码协议进行验证,并查找协议中可能存在的漏洞,既可以方便地进行手工推导证明,也非常易于自动化实现.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王亚弟	解放军信息工程大学电子技术学院	68	257	9.0	11.0
2	韩继红	解放军信息工程大学电子技术学院	59	243	9.0	11.0
3	张超	解放军信息工程大学电子技术学院	16	63	4.0	7.0
4	范钰丹	解放军信息工程大学电子技术学院	12	24	2.0	4.0
5	赵宇	解放军信息工程大学电子技术学院	2	7	1.0	2.0