论文部分内容阅读
基于形式化方法开发自动分析工具是密码协议安全性分析的一种有效的方法,然而,由于密码协议参与主体的任意性、消息运算复杂性和运行的并发性,密码协议的安全性分析是高度计算复杂性的难题.基于最近提出的密码协议代数(CPA)模型,采用代数方法描述密码协议活动,精简密码协议描述,提出一个高效的密码协议安全性自动分析算法.该算法通过泛多项式方程求解技术,减少密码协议安全性分析过程中产生的冗余状态数量,并可提供在无限状态空间运行的协议安全性分析.根据该算法,实现了一个密码协议自动分析系统ACT-SPA,应用该系统分析了二十多个密码协议,结果显示系统显著提高了运行效率,并发现了新的密码协议攻击.
However, due to the arbitrariness of the participant in the cryptographic protocol, the complexity of the operation of the message and the concurrency of the operation, the security analysis of the cryptographic protocol is a highly effective method for analyzing the security of the cryptographic protocol. However, Based on the recently proposed cryptographic protocol algebra (CPA) model, using algebraic methods to describe the activity of cryptographic protocols and streamlining cryptographic protocol description, an efficient cryptographic protocol security automatic analysis algorithm is proposed.The algorithm is solved by a generalized polynomial equation Technology to reduce the number of redundant states generated during cryptographic protocol security analysis and provide protocol security analysis running in an infinite state space.According to the algorithm, ACT-SPA, a cryptographic protocol automatic analysis system, is implemented. With this system Analyzing more than twenty cryptographic protocols, the results show that the system significantly improves operational efficiency and finds new cryptographic protocol attacks.