Analysis Cryptographic Protocol Using Timed Petri Net
Pang Yu-ye · Acta Simulata Systematica Sinica · 2003
The paper analysis four kinds of formal methods for the analysis of cryptographic protocol and set forth the merits and disadvantages of each. In order to develop a unified theory to verify cryptographic protocol, this paper provides a way to describe cryptographic protocol based on timed Petri net. This methods not only specifies the static and dynamic properties but also evaluates the performance of cryptographic protocol (mainly time delay and software complexity). Applying this method to the wireless protocol proposed by Aziz and Diffie, this paper verifies the known attacks on it and points out several attacking scenarios. Finally, An improvement on Aziz-Diffle protocol is proposed.