Study On Key Technologies Of Formal Analysis Method Of Security Protocols

The computer network is penetrating into all kinds of realm, this makes the security problem becomes more and more outstanding and complicated. Addressing security problems for many network applications is already the major event. Judging from the current solution to security problems, the security protocol is one of the most effective means to resolve the network security problems. How to analyze the security protocols to ensure their safety and validity is one of the key problems should be solved by formal methods for security protocols. After developing for more than twenty years, the formal method of security protocols has been rapid development and wide application, and accepted as the most effective and reasonable method in the field of security protocol verification. The formal method builds up the scientific theory model to carry out the strict mathematics and logic on security protocols to verify their security or point out their security flaws. Meanwhile, the formal method can be used to guide the design of security protocols.Although the formal methods have been succeeded in finding flaws and attacks of many security protocols, they still suffer from lots of problems. By comprehensive analysis of these methods, we have found two inherence drawbacks: do not unite the description of the security property with a clear formal method; lack of a more generalized formal language used as the unified framework to analyze security protocols.Aiming at the above-mentioned two inherent drawbacks, we gradually carry out the study from three levels: first of all, we in-depth study three kinds of typical and important formal methods: BAN-like logic, strand space, SPI calculus, analyze their inherent drawbacks, and effectively improve their partial drawbacks. Secondly, we present a method based on directed graph. This method partially solved the second inherent drawback. Finally, we put forward a unified framework to analyze the security protocol. This method models the protocol run, the security property and its verification at a high-level logic abstraction. Guided by this framework, we also design a new analysis method based on symbolic trace method. Examples show that this method is effective.The unified framework we presented in this dissertation is a significative attempt to solve the two inherent drawbacks of current security protocols. The main innovations are as follows:1. In order to overcome the flows of BAN-like logics in their“idealization protocol”step and monotony trust relationship, we present a dynamic logic based on the concept of MUO (Message Unique Origin). The concept of MUO resolves the difference between“believe the occurrence of the event”and“believe the truth of the event”, based on this, a dynamic logic is built up.2. Proposing a new semantic model to analyze the syntax flow of BAN-like logics. This model defines the possible worlds and their relationships of BAN-like logic, and under this modal logic frame, evaluation function is presented. We theoretically prove that the logic semantic flow of BAN-like logic is insurmountable.3. Proposing the unified formal method to description the security property, we attempt to use match relationship to depict the security property. But in the research process, we have made the improvement regarding this, and then the security property is finally defined as the deduction relationship between the messages based on time and the property messages. This definition is separated from the concrete protocol, therefore, has the universality.4. Proposing a combined analysis model which uses the matching relationship to depict security properties. This model combines the process calculus and the message deduction relationship. On the one hand, the method makes up the lack of the data structure in process calculus; on the other hand, the method makes it clear that how and when to carry out the symbolic message deduction.5. Proposing a directed-graph-based method to analyze security protocols, this preliminarily solves the flows in formally modeling the security protocol. This method decomposes each protocol step into the sequence of actions, and then defines the rules to generate the directed graph, as well as the converse-searching algorithm which can accurately tracks the ways to construct the protocol messages.6. Proposing a unified framework based on the pattern of“security property modeling + protocol run modeling”. We use time-based message deduction relationship to depict the security properties, and add time concept and time-based message reasoning rules to symbolic trace method, thus we effectively construct the symbolic-trace-based method to analyze security protocols. The unified framework is of great significance for the design of security protocols, as well as the design of the analysis method.