Research On Checking Security Protocols Technology Based On CPN Models

From 1970s, using formal methods to analyze cryptographic protocols remains the key issue in the field of computer security. There have been many effective methods, such as Ban logic, CSP, strand spaces, Paulson's inductive set of rules, and Petri nets methods, etc. Although many methods are available for protocol verification, each of them has their own deficiency when they are used to check the security protocols. Hence, it is very significant to improve these methods or find a more effective method. This paper focus on several problems of the traditional security protocol analysis method based on Colored Petri nets, and has finished the following research:(1) After analyzing the message structure, a three-layer structure of message is prosed, which include information element, cryptograph, and message. Then after studying the intruding process, a new intruder model is proposed. In the intruder model a new mechanism is set, in which the intruder interrupt all the message, compose a new message set according to his own knowledge and the message structure, then transfer the messages in the message set to other users. The intruder model has more material description than the traditional intruder model.(2) According to the intruder mode above, we propose a new security protocol checking method based on Colored Petri nets models. In our method it is avoided to predict the insecure state before analyse protocols as in the traditional method. The intruder in our method compose messages which can be received by other users as much as he can, then a state space is set up by sending the messages according to broad fist search order, thus we can search insecure state in the state space.To verify the method we have proposed, we have checked Neeham-Schroedor public key protocol and TMN cryptographic protocol by our method. We construct Colored Petri nets models for the protocols, then analyse the protocols by CPN tools, which is an automatic tool for Colored Petri nets. In the experiment of Neeham-Schroedor public key protocol a known flaw is found. In the experiment of the TMN cryptographic protocol, an integrated intruder model is constructed, and a state space of the protocol is generated. The experiment proved the security checking method based on Colored Petri nets models we have proposed is feasible. The method owns the advantages of analysing protocols more thoroughly, universal, comprehensible, interactive, and easy to apply.