Cryptographic protocol security analysis based on bounded constructing algorithm
An efficient approach to analyzing cryptographic protocols is to develop automatic analysis tools based on formal methods. However, the approach has encountered the high computational complexity problem due to reasons that participants of protocols are arbitrary, their message structures are complex and their executions are concurrent. We propose an efficient automatic verifying algorithm for analyzing cryptographic protocols based on the Cryptographic Protocol Algebra (CPA) model proposed recently, in which algebraic techniques are used to simplify the description of cryptographic protocols and their executions. Redundant states generated in the analysis processes are much reduced by introducing a new algebraic technique called Universal Polynomial Equation and the algorithm can be used to verify the correctness of protocols in the infinite states space. We have implemented an efficient automatic analysis tool for cryptographic protocols, called ACT-SPA, based on this algorithm, and used the tool to check more than 20 cryptographic protocols. The analysis results show that this tool is more efficient, and an attack instance not offered previously is checked by using this tool.
作 者： LI Xianxian HUAI Jinpeng 作者单位： School of Computer, Beihang University, Beijing 100083, China 刊 名： 中国科学F辑（英文版） SCI 英文刊名： SCIENCE IN CHINA SERIES F:INFORMATION SCIENCES 年，卷(期)： 2006 49(1) 分类号： O1 关键词： cryptographic protocol formal analysis security verification