In: Lecture Notes in Computer Science, Vol. 718: Advances in Cryptology, AUSCRYPT'92. Springer-Verlag, 1993.
Abstract: In this paper, we present a Petri net based methodology for the formal modelling and analysis of cryptographic protocols. We set up modelling rules that represent the protocols in terms of Petri nets. The modelling produces formal descriptions for the protocols with good visibility and layered abstraction. In particular, the descriptions clearly visualize the causal relations and constraints among the data flows in the protocols. An intruder model is introduced to formulate intruder attacks and to generate test cases against the cryptographic protocols. A procedure that exhaustively generates the test cases and searches for states that violate specified security criteria, is also proposed. We demonstrate the value of this methodology by applying it to a number of published protocols. In this way, we are able to reveal security flaws of these protocols. This methodology is applicable to both public-key based cryptographic protocols.