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

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