Research On Formal Verification And Design Of Security Protocols

Computer network is widely being used in the world now. Security problems of computer network have been exposed more and more, so people are attaching more importance to it. In the area of network security, because all kinds of security services are all based on security protocols, it is most important that the security protocols are secure. In the past 20 years, people introduced many security protocols in order to fulfill all sorts of network applications. However, later research proved that there were security leaks in most security protocols. How to design secure security protocols and how to verify security protocols become the most important two areas in the research on security protocols.Security protocols belong to communication protocols. The main aim of security protocols is to realize key agreement and authentication using cryptography. However, many facts show that there are still some leaks in the security protocols which have been carefully analyzed and designed by security experts. Some security protocols are so much as attacked after using many years. Firstly, this paper analyzes all kinds of security protocols, proposes a new classification standard and based on the standard, enumerates some typical security protocols. And then, this paper researches all sorts of security protocol leaks to summarize 5 kinds of typical security protocol leaks.Formal methods arose in the end of 1970s and now it is widely used in solving academic and practical problems. Computer security is a relatively successful area in using formal methods and there are many great achievements in using formal methods to verify security protocols. Formal verification is in effect to detect security protocols. The development of BAN-like logics promotes the research of this area. This paper describes the formal methods and the application of formal methods on verification of security protocols. Based on summarizing all kinds of formal methods about security protocol verification, the paper introduces a new kind of formal verification method of security protocols. The new formal method is based on belief logics and can realize all verification functions of current BAN-like logics. It extends verification support about key agreement protocols using Diffie-Hellman and makes the verification process implements conveniently. Consequently verification can be easy to be realized automatically. This logic gives a new approach to formal verification of security protocols.There are not some certain rules about security protocol design now. This paper proposes a new kind of rules about security protocol design. This paper also gives a brief introduction about a new model of security protocol design, layer-based security protocol model design. In the end, this paper introduces a new idea about security protocol design, dynamic security protocols. I hope that this new idea can open the view about security protocol design in order to bring new discussion and development.