Modeling and Veri cation of cryptographic protocols using coloured petri nets and design/CPN

In this paper, we present a technique to model and analyse cryptographic protocols using coloured Petri nets. A model of the protocol is constructed in a top-down manner: rst the protocol is modeled without an intruder, then a generic intruder model is added. The technique is illustrated on the TMN protocol, with several mechanisms introduced to reduce the size of the occurrence graph. A smaller occurrence graph facilitates deducing whether particular security goals are met.