The Analysis Of Model Checking And Verification System Of Network Security Protocol

It is very important that analysis of network security with the rapid development of the computer age. It has been one of the most popular topics in network security area to ensure the safety and secret of security protocols. But defects of Security protocols threatened badly to network security. In order to guarantee that the information and data the network transmits will not be lost; we must analyze and can verify these protocols by formal and non formal methods. In order to solve the state space explosion problem, we should improve the protocol model by the search optimization algorithm. So, we can know formalization analysis and testing method is the key technology in the network security. And it is very important to regulate cryptographic protocols properties and describe them by LTL properties.This paper studies the formal analysis methods and tools of model checking, in order to detect the hidden flaws of network security protocol, and improves the protocol. The main tasks and contributions are:1. Through using the powerful model checking tool with authentication cryptographic protocol—SPIN, and applying static analysis technique and automatic reduction method, simplified the manner of inputing in order to achieve the purpose of improving the SPIN operating environment, so that the model is more straightforward.2. By the SPIN tool embedded verification system of security protocol, using the search method of states to meet the design specifications of the protocol, and testing the structural method (such as the single step model and complete model), and collecting the data flow information with the analysis and verification of internet security protocol. By reducing the number of transitions in the model space, effectively reducing the state space explosion problem.3. Designed and implemented the verification system of network security protocol, modeling a trusted third party symmetric cryptographic protocol and commerce protocol SSL3.0 handshake protocol, and using LTL to describe the property of protocol in order to improve the search efficiency to prove the security and reliability of protocol itself, by the case of the protocol analyzing the availability of the verification system.