Analysis And Verification Of Security Protocols Based On Visual Methods And Formal Methods

Security protocol, also known as cryptographic protocol, is one interactive communication protocol based on the cryptosystem, which runs within the computer communication networks and distributed systems, by means of cryptographic algorithms to achieve the key distribution, authentication or other purposes. At present, the security protocol has become one of the mainstream research directions in the international information security field.Security protocol constitutes the cornerstone of a safty network environment, and its correctness and security is vital to network security. Safety analysis on security protocol is an important means to reveal the existence of loopholes in it. The methods of analysis include:attack detecting method and formal analysis. In the late 1980s and early 1990s, the formal analysis of security protocols to become hotspot. At present, the formal analysis methods of security protocols can be broadly classified into three categories:formal logic, model checking and theorem proving methods. They have both strength and weakness at the moment. For this reason, this paper explores a new way which combines the visual modeling language and formal method to analyse security protocol through combining UML2.0 and timed automata to analyse it. The specific studies are as follows:(1) Introduce the background, basic conceptions and classifications of security protocols. Give Analysis and comparison of the three main formal analysis methods of the security protocols. Propose a new analysis method of security protocols based on visual method and formal method.(2) Firstly, introduce the Unified Modeling Language UML2.0 and its extension mechanism. Then extend the UML2.0 sequence diagram. Finally, give the formal description of the UML2.0 sequence diagram in interactive view.(3) Give a converting method from UML2.0 sequence diagram model to timed automata model. The method converts the simple fragments which are obtained by decomposition on the sequence diagram to the corresponding timed automata, and then merges these automata according to the combined fragments convertion method. At last, the final timed automata are obtained.(4) The method presented in this paper, which is to combine visual method and formal method, is applied to the anlysis of simplified Needham-Schroeder authentication protocol (NS Authentication Protocol for short). Experimental results show that an intruder's attack upon the NS protocol. It shows that the method can be used for security protocol analysis.Typically, methods for formal verification of security protocols do not take time into account, and this choice simplifies the analysis. In the analysis of the NS protocol, we consider the times required by agents to encrypt values, decrypt values and generate nonces and that takes the sending. Thus, timed automata for the protocol are obtained. This approach allows a more realistic analysis of security protocols.