Research On Formal Verification Methods Of Security Protocols Based On Strand Space Model

Security protocols works as a kind of the kernel technology for the secure network communication, thus their correctness are very crucial to network security. However, the security protocol design is an error-prone process. The problems, which are how to analyze the security protocols to ensure their safety and validity, how to deign the security protocols to ensure their correctness, and how to improve the efficiency of the automatic verification tools, should be solved by formal methods for security protocols. Until now, many kinds of formal methods have been presented for security protocol analysis and design. Although the formal methods have been succeeded in finding flaws and attacks of many security protocols, they still suffer from lots of problems, such as the faultiness of the formal method itself, lack of automatic tool support because of the complex theoretic model, and resource-exhausting problem in current automatic verification tools. Whereas, in this thesis, we make further research on the above areas based on the strand space model and authentication tests, propose some efficient solutions and obtain several research achievements. The main research contents in this thesis include three aspects, which are described as follows:Firstly, we do the research on how to apply the strand space model and authentication tests to analyze the existing security protocols, point out the flaws in these protocols and construct the possible attacks. According to the result, we propose the improvements of these protocols, and finally verify the correctness of the improved ones based on the formal methods. The security protocols studied in this thesis have universal theoretical significance and practical sense. We also...