Research And Application 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 security 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 used to analyze and design practical security protocols. Following are the main results of this thesis:Introduce the background and basic conceptions of security protocols, expatiate the three classifications of the formal analysis methods.Introduce the running-mode analysis based on the two-party security protocol. Conclude the running-mode analysis based on the three-party security protocol including only one server which acts as the trusted third party. Put forward the running-mode analysis based on the security protocol including more than one server which acts as the trusted third party.Calculate the maximum of the running-modes and suggest the effective limited conditions. Create the combined set of running-modes which is independent of the model checking tools. Furthermore, put forward the running-mode analysis based on the muti-party security protocol.Analyze the practical protocols, such as SSL3.0, TMN, Kerberos protocol, by using the running-mode analysis method, which achieves the good results.Put forward the design principles of security protocol on the basis of the security flaw which protocol can avoid.Design a secure key establishment protocol using these design priciples.Sum up the model checking technology and compare it with other formal analysis methods.