The Analysis Of Security Protocols Based On Colored Petri Nets

With the development of computer network application, analyzation and investigation security protocol is becoming a very important aspect in the area of information security . Because of its compactness, fineness and unambiguity, formal analysis of security protocol has been an efficient and correct method step by step. 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.The dissertation mainly discusses formal methods for analysis and evaluation of security protocols based on colored Petri nets (CPN). The main results obtained are as follows:1. A new way is introduced to describe cryptographic protocol based on colored Petri net. Meanwhile, the concrete steps using CPN is expounded. This method specifies the structure and dynamic properties .2. Applying CPN to model and analysis NSSK protocol, this thesis verifies the replay and pretend attacks on it and points out two executive scenarios and attacking scenarios. An improvement on replay attack and an improvement on pretend attack is proposed.3. Applying time-stamp to prevent the restrain-replay attack may exist a hidden defect. An improvement on restrain-replay attack based on challenge is proposed. Verifying the advantage and disadvantage by the challenge and time-stamp insure the protocol security.