Analysis And Evaluation Of Cryptographic Protocols Based On Timed Petri Nets

It is a hard problem to analyze cryptographic protocol in the area of computer network security. Using formal methods to analyze cryptographic protocol remains the key issue in this field. Because of its compactness, fineness and unambiguity, formal analysis of cryptographic protocol has been an efficient and correct method step by step. The dissertation mainly discusses using formal methods for analysis and evaluation of cryptographic protocols based on timed Petri nets(TPN). The main results that the author obtained are as follows:(1) The thesis reviews four kinds of formal methods for the analysis of cryptographic protocol and sets forth the merits and disadvantages of each.(2) The author introduces a new way to describe cryptographic protocol based on timed Petri net, meanwhile, the concrete steps using TPN is expounded. This method not only specifies the structure and dynamic properties but also evaluates the performance of cryptographic protocol (mainly time delay and software complexity).(3) Firing rules of timed Petri nets and the definition and algorithm of timed reachable graph are given. A fundamental applied methods (mainly timed reachable graph and state equation ) are discussed.(4) Applying this method to the MSR, Aziz-Diffle and TMN wireless protocol, this thesis verifies the known attacks on them and points out several executive scenarios and attacking scenarios. An improvement on Aziz-Diffle is proposed.(5) The thesis also objectively evaluates the performance of time delay, structure properties and software complexity of the above three cryptographic protocols.(6) At last this thesis builds the structure of the automatic tool based on timed Petri nets to analyze cryptographic protocol.