Decomposition techniques for cryptographic protocol analysis

In this paper, decomposition techniques are used to simplify the analysis of cryptographic protocols using coloured Petri nets to locate security flaws and weaknesses. These techniques exploit the inherent modularity of the Petri net model which is composed of distinct protocol entities, distinct protocol stages, and an explicit intruder model. The intruder model may embody a suite of threat characteristics, which can be used to formulate simple or complex attacks. The methodology is described in this paper and is applied to a one-way authentication protocol with two stages