Research On Model Checking Of Security Protocol Of Network

The security of security protocols is the foundation of the network security. Presently the analysis of security of cryptographic protocols using the formal method has become a hotspot of research. This dissertation makes a research on the theory and technique of the formal analysis of the security protocols and focuses on the running-mode analysis method based on the model checking technology. Furthermore, this method is extended to analyze and design fair exchange protocols. Following are the main results of this thesis:Introduce the background and basic conceptions, evolvement and the future trend of security protocols, expatiate the three classifications of the formal analysis methods of the cryptographic protocols analysis.Introduce the running-mode analysis based on the two-party and the three-party security protocol. Put forward the running-mode analysis of two-party optimistic fair exchange protocols.Analyze several electronic commerce protocols, such as SET, Micali's and FPH protocol, by using the running-mode analysis method, which achieves the good results。Put forward the design principles of fair exchange protocol on the basis of the characteristics of fair exchange protocols. Design a fair exchange protocol using these design priciples。...