The Analysis Of Cryptographic Protocols Based On Petri Nets

Analysis of cryptographic protocol is significant for secure communication between computer systems through networks. Using formal methods to analyze cryptographic protocol remains the key issue in this field. At present the formal methods include logic method, model checking method, theorem proving method, Petri Net methods etc. These methods all have their advantages and disadvantages. Aiming at the weakness in the analysis of cryptographic protocol using Petri Net method, the thesis mainly discusses combining Petri Net method with some results of model checking theory for the analysis of cryptographic protocol. The main results the author obtained are as follows:1. Combine running-modes method with Petri Net modeling to analyze cryptographic protocol, give the concepts of Basic Petri Net model and Attacking Petri Net model of protocols' running modes and clarify the relationship between the two models and analysis of cryptographic protocol.2. Present the method to construct a Basic Petri Net model and an Attacking Petri Net model, subsequently give detailed steps for analysis of cryptographic protocol.3. Analyze the Needham-Schroeder protocol, Helsinki protocol and TMN protocol in detail and summarize a type of attack of cryptographic protocols.The characteristics of our work are as follows:1. Construct Petri Net Model according to the protocol' s running modes, which is different from usual Petri Net method of analysis of cryptographic protocols.2. Mainly discuss a protocol' s security when many cases (take two cases as an example)are executed in parallel.