Research On Security Protocol Formal Method Based On Colored Petri Nets Model

With the rapid development of the Internet, and increasing attention to the security of communication system, security protocols are widely deployed in the Internet. As the increasingly attacking capabilities and complexity of the applications, the design and analysis of security protocols are difficult to achieve. Model checking and attack trace generation method are major technologies to validate the correctness of security protocol.The Security protocol analysis and validation include security protocol modeling, attack trace generation and selection. Major causes of complexity of security protocol execution are resulted by the Dolev-Yao based attacker model and protocol multi concurrent sessions. A new improved attacker model is introduced. A new session configuration based dividing analysis method is effectively controlled the number of concurrent session. Attack states are characterized by security properties voilation events in the non secure states. Two attack sequence generation approach based on security properties voilation events are proposed:state exploration method and on-the-fly generation method. The security properties voilation events based attack sequence generation approach can effectively control the exploration scope and improve efficiency. Finally, by analyzing the data features of the security protocols, extract the attack tactics capable of form a successful attack. Based on attak tactics, modeling attack purpose and generating attack traces generally can reduce the workload of searching the state space.The main contributions of this dissertation are as follows:(1) A new multi concurrent session partition analysis method for security protocol model is presented.We proposed a new improved attacker model without reduce the capability of the Dolev-Yao attacker. Attacker’s function is divided into the decomposition and synthesis of two front and rear stages. Formal analysis of security protocol with an attacker needs to consider whether the attack was successful in the case of multiple concurrent sessions. By setting session configuration and session sequence, we proposed a multiple concurrent sessions partition analysis method, which is effectively reduce the state space of the model checking.(2) New attack sequence generation methods based on the security property voilation events are proposed.Attack Trace Generation Oriented CP-nets (ATG-CPN) is formally defined to model the security protocol with an attacker. Formal definition of security properties, including confidentiality property and authencation property, are given according to the security specification and formal model. Attack states are characterized by security property voilation events. Based on ATG-CPN models and security property voilation events, an attack sequence generation method is proposed. This novel CP-nets model based attack sequence generation approach improves the error coverage and avoids generating false attacks. A new CP-nets model based On-the-fly attack sequence generation method is also proposed, which does not need to explore the entire state space, so can effectively generate attack sequences.(3) A method of attack tactics based attack sequence selection method is presented.Using attack sequence generation method may generate a lot of attack sequences, to fit the model checking demand, a new attack tactics based attack sequence selection method is given. The limited attack sequences obtained after selection process meet coverage of attack trace generation purposes.