Security protocol analysis based on run modes and Petri net

The analysis of security protocols is of great significance to ensure the safe communication of computer networks. Using formal methods to analyze security protocols has been a research hotspot in this field. Based on the run modes method and Petri net, this paper presents a specific method for analyzing security protocols. Firstly, the concepts of basic Petri net model (BPN) and attack Petri net model (APN) of protocol run modes are given, then the algorithm for constructing APN through BPN is proposed. Finally, the effectiveness of this method is illustrated by analyzing Helsinki protocol.