Security Protocols, Formal Verification Methods

Security protocol is a type of communication protocol based on cryptography, which runs over the computer network or distributed systems, and provides security services.The correctness of security protocols is critical for the transactions over the open networks.The cunnings of the security protocols do not always achieve their design objectives for its flaws.The analysis and the verification of security protocols have been proved to be an effective way for finding flaws of security protocols. At present, the analysis on security protocol has been developed from primal informal method to many kinds of formal methods.The analysis and the verification of security protocols have been the focus in the domain of formal methods.In this dissertation, security protocols are the main research objectives, and the theory of strand space model is the main research content. Based on strand space model, we study formal techniques on security protocols from theory to practice.Primary innovative work in this paper can be summarized as following:This dissertation give a survey on the formal methods for verifying security protocols from the technical ways,characteristics used in verification of security protocols.Based on the theory of current strand space, This dissertation address security protocol correctness and two ways by which security protocols are described, and at the end of the third chapter, Three typital formalisms for verifying protocol correctness are proposed.The last part provides concluding remarks on this work and discusses potential future research.Based on three formal methods that be proposed in the third part, the NSL protocol,the modified version of Yahalom protocol and the modified version of X.509 protocol are analyzed.