SPA: A New Efficient System for Security Protocol Analysis
Jian Li · Chinese Journal of Computers · 2005
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.