SPA:新的高效安全协议分析系统

研制高效的自动分析系统是密码协议安全性分析的一项关键任务，然而由于密码协议的分析非常复杂，存在大量未解决的问题，使得很多现有分析系统在可靠性和效率方面仍存在许多局限性．该文基于一种新提出的密码协议代数模型和安全性分析技术，设计并实现了一个高效的安全协议安全性自动分析系统(Security Protocol Analyzer，SPA)．首先对协议安全目标进行规范，然后从初始状态出发，采用有效的搜索算法进行分析证明，试图发现针对协议的安全漏洞．使用该系统分析了10多个密码协议的安全性，发现了一个未见公开的密码协议攻击实例．实验数据显示，该系统与现有分析工具相比，具有较高的分析可靠性和效率，可作为网络系统安全性评测以及密码协议设计的有效辅助工具．

SPA: A New Efficient System for Security Protocol Analysis

Cryptographic protocols are c ommunication protocols of distributed systems that use cryptography to achieve v arious goals such as authentication and key distribution in the open network env ironment. Developing efficient automatic system is a crucial task in the area of security analysis for cryptographic protocols. However, the security analysis f or cryptographic protocols is very complex and difficult and a lot of unresolved problems still present in it, which causes some limitations on reliability and efficiency of previously available automatic systems. An efficient automatic ana lysis system (Security Protocol Analyzer, SPA) for cryptographic protocols is designed and implemented based on the CPA (Cryptographic Protocol Algebra) mod el and new analysis techniques. In this system, security properties of the crypt ographic protocols are specified firstly, and then an effective proof search alg orithm starting with the initial state is applied and tries to find all possible attack sequences on them. More than ten cryptographic protocols are analyzed su ccessfully with this system, and moreover, a new attack instance is also found. The analysis results show that SPA has improved the analysis reliability and eff iciency compared with other existing tools. It can be used as an efficient tool for the evaluation of the network security and the design of cryptographic proto cols.