Application of colored petri nets in security protocol analysis

Colored Petri Nets (CPN) used in this paper is an automatic modeling tool based on model detection, which introduces the concept of "color set" and expands the expression capability of Petri nets. In addition, CPN Tools, a mature CPN modeling tool, is different from the commonly used method of establishing reverse state analysis equation before, which makes the model establishment graphical and hierarchical, and its own state space analysis tool and CPN ML language can efficiently help analysts get the desired data. In this paper, the principle and advantages of formal analysis of security protocols using CPN are introduced in detail. Dolev-Yao attacker model and CPN Tools are used to demonstrate the effectiveness and intuitiveness of modeling analysis using CPN by taking TMN as an example. Finally, this method is compared with mainstream formal analysis tools. The characteristics and limitations of each tool are discussed.