基于Abadi-Rowgaway 的形式化加密的計(jì)算合理性定理，論文提出和證明了密碼協(xié)議形式化分析的計(jì)算合理性定理。通過對(duì)群密鑰分配協(xié)議的分析，說明本文的定理對(duì)協(xié)議的可選擇攻擊具有較強(qiáng)的分析能力，論文提出了群密鑰分配協(xié)議的形式化方法與計(jì)算方法下安全性的形式化定義，并證明了其合理性。
關(guān)鍵詞：形式化方法；計(jì)算方法；合理性定理；密碼協(xié)議分析

The Computational Soundness of Formal Analysis of Cryptographic Protocols WANG Quan-lai1, 2 WANG Ya-di 1 HAN Ji-hong1 (1Institute of Electronic Technology, the PLA Information Engineering University, Zhengzhou 450004； 2The PLA Air Defense Forces Command College, Zhengzhou 450052) 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.
Keywords: formal method; computational method; soundness theorem; cryptographic protocol analysis