密码协议形式化分析的计算合理性

计算机工程与应用 ›› 2007, Vol. 43 ›› Issue (21): 8-11.

密码协议形式化分析的计算合理性

王全来^1,2，王亚弟¹，韩继红¹

1.解放军信息工程大学电子技术学院，郑州 450004
2.解放军防空兵指挥学院，郑州 450052

收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2007-07-21 发布日期:2007-07-21
通讯作者: 王全来

Computational soundness of formal analysis of cryptographic protocols

WANG Quan-lai^1,2，WANG Ya-di¹，HAN Ji-hong¹

1.Institute of Electronic Technology，the PLA Information Engineering University，Zhengzhou 450004，China
2.The PLA Air Defense Forces Command College，Zhengzhou 450052，China

Received:1900-01-01 Revised:1900-01-01 Online:2007-07-21 Published:2007-07-21
Contact: WANG Quan-lai

摘要/Abstract

摘要： 基于Abadi-Rowgaway的形式化加密的计算合理性定理，提出和证明了密码协议形式化分析的计算合理性定理。通过对群密钥分配协议安全性的分析，说明定理对协议的可选择攻击具有较强的分析能力，提出了群密钥分配协议的形式化方法与计算方法下安全性的形式化定义，并证明了其合理性。

关键词: 形式化方法, 计算方法, 合理性定理, 密码协议分析

Abstract: Based on the Abadi-Rowgaway computational soundness theorem of formal encryption，this paper proposes and proves our computational soundness theorem of formal analysis of cryptographic protocols.Through the analysis for group key distribution protocols，our soundness theorem is stronger and powerful in adaptive attacks.This paper proposes formal definitions of security for group key distribution protocols both in the formal methods and the computational methods，then proves soundness of the formal definition.

Key words: formal method, computational method, soundness theorem, cryptographic protocol analysis

王全来^1,2，王亚弟¹，韩继红¹. 密码协议形式化分析的计算合理性[J]. 计算机工程与应用, 2007, 43(21): 8-11.

WANG Quan-lai^1,2，WANG Ya-di¹，HAN Ji-hong¹. Computational soundness of formal analysis of cryptographic protocols[J]. Computer Engineering and Applications, 2007, 43(21): 8-11.

[1]	刘友林，郑巍，谭莉娟，樊鑫，杨丰玉. 面向适航标准的机载软件测试验证工具综述[J]. 计算机工程与应用, 2021, 57(11): 1-10.
[2]	雷斌，王菀莹，赵佳欣. 货位分配优化研究综述[J]. 计算机工程与应用, 2021, 57(1): 48-55.
[3]	唐伟. 一种有效的模糊关联规则挖掘的形式化方法[J]. 计算机工程与应用, 2015, 51(18): 114-119.
[4]	邢洪智1，罗颖2，罗长远1，霍士伟1. 移动环境中多级网络安全切换策略设计[J]. 计算机工程与应用, 2011, 47(36): 127-130.
[5]	曾一，孙政，周吉，胡小威. 一种状态图到B规格说明的自动转换方法研究实现[J]. 计算机工程与应用, 2011, 47(35): 77-80.
[6]	胡海波，张雷. 基于SWRL的软件需求一致性验证方法[J]. 计算机工程与应用, 2010, 46(21): 72-75.
[7]	王向云¹,赵雷²,蔡开元². 基于监控理论的EFSM设计方法[J]. 计算机工程与应用, 2009, 45(6): 20-24.
[8]	洪振杰^1，2，张翼鹏^1，3，李磊¹，徐贤胜¹. 掩星数据变分同化的算法讨论[J]. 计算机工程与应用, 2009, 45(31): 237-240.
[9]	陈付龙¹,樊晓桠². 嵌入式系统建模理论与方法[J]. 计算机工程与应用, 2009, 45(13): 8-12.
[10]	胡启敏^1,2,薛锦云^1,2. 形式化方法Designware、B的比较[J]. 计算机工程与应用, 2007, 43(31): 96-99.
[11]	刘喆，王跃宗，杨建坤，李德胜. 一种基于BP网络的错帖检测新算法[J]. 计算机工程与应用, 2007, 43(15): 221-223.
[12]	王鹏，李谢华，陆松年. 基于认证测试方法的EAP-AKA协议分析[J]. 计算机工程与应用, 2007, 43(15): 157-159.
[13]	石海鹤石海鹏薛锦云. 形式化开发Hanoi塔问题非递归算法[J]. 计算机工程与应用, 2007, 43(11): 96-99.