The Verification of Cryptographic Protocols Using Coloured Petri Nets
Issam Al-Azzoni · MacSphere (McMaster University) · 2004
1977) is an example of a public key cryptographic algorithm [HeI78, Sch96].Given a ciphertext C, crypt analysts attempt to find the plaintext M such that C = E(M, K), where K, unknown to the cryptanalyst, is the key used to encrypt M.Cryptanalysts break a cryptographic algorithm by observing ciphertext messages generated by the algorithm, or having access to a collection of plaintext-ciphertext pairs.Many of the currently used cryptographic algorithms are very difficult to break.An • use the technique to model and verify the TMN key exchange protocol and the Needham-Schroeder public key authentication protocols. Thesis OutlineThe remainder of this thesis is organized as follows.Chapter 2 introduces Petri nets and coloured Petri nets.First, Petri nets are introduced.This is followed by a detailed introduction to Jensen's form of coloured Petri nets and Design/CPN.Chapter 3 serves as a literature review on the verification of cryptographic protocols using Petri nets. Chapter 4 describes our new technique. We demonstrate the technique by using it in the modeling and analysis of the TMN protocol.Chapter 5 is the conclusion chapter.It includes a discussion on the technique, as well as suggestions for possible future work.Appendix A summarizes the functional notation we use to describe the protocols. Appendix B presents the application of our technique in the verification of theNeedham-Schroeder authentication protocol.