The Research Of Automatic Validation Algorithm For Security Protocols Based On Formal Methods

As the safety guarantee of network communication, security protocols are the secure base of the whole information system architecture. In order to ensure the correctness of security protocols, the researchers propose a series of automatic validation algorithms based on formal methods to verify the safety of security protocols, and have successfully found many flaws and attacks of security protocols.But these algorithms can only point out the vulnerabilities, can not automatically generate improved security protocols. In addition, There algorithms are inefficient and difficult to use. Whereas, on the foundation of the string space model and authentication test methods, I make further research on the above issues in this paper, the research content mainly includes the following aspects:Firstly, on the basis of studying intensively formal methods, I analyze detailedly several widely used automatic verification algorithms, and propose the IVAP (Intelligent Validator for Authentication Protocols) algorithm aiming at the shortcomings of the existing automatic verification algorithm for security protocols. The IVAP algorithm not only can automatically complete protocol verification, but also generate the improved security protocol by using the unsafe attributes to search backward the tree of the primary strand, and validate improved security protocol until the protocol is safe.Secondly, I design and develop the automatic security protocol validation prototype system based on the IVAP algorithm.The prototype system adopts the B/S architecture, including four function modules:security protocol graphics display interface, security protocol formal description interface, automatic verification and improved protocol generatation.Finally, I validate some classic authentication protocols by using the implemented system, analyze the time complexity and space complexity in the process of validating the security protocols, and also compare the experimental data of the IVAP algorithm and the other similar algorithms. The result indicates the effectiveness and the efficiency of the IVAP algorithm.The innovative works mainly have the following two points:1. I propose the IVAP algorithm based on string space. If the algorithm finds theflaws in the process of validating the protocols, it can generate the improved security protocol. The algorithm is innovative in the application of the theory.2. I develop the automatic security protocol validation prototype system based on the IVAP algorithm.The system is more efficient than other similar systems by experiment results.The system is innovative in the application of the theory.