Study on a CPN-Based Auto-Analysis Tool for Security Protocols

This paper proposed an auto-analysis tool for security protocols. The tool is a formal analysis method based on Colored Petri Net (CPN for short) model. It analyses the semantics of security protocols based on CPN model and creates the relations between elements of security protocols and objects of CPN. And then the query functions of CPN ML from CPN Tools are used to describe security attributes and a self-defined inquiry functions library and state query function from CPN Tools are used to analyze and verify security protocols. Advantages of this tool are strong generality, high timeliness and good interactivity.