Formal Modeling of Cryptographic Protocols Using Petri Nets
基于Petri网的密码协议形式化建模

Cryptographic protocol is secure mechanism for sharing network resources,is the cornerstone to build security network environment The security of the cryptographic protocol plays a vital role to entire network environment. A new colored Petri nets (CPN) methodology for security analysis of cryptographic protocol was proposed. We applied the new approach to model TMN protocol with multi concurrent session, and the model was categorized based on session configuration and session schedule. And the attack traces were obtained using on-th}fly method. Using the state space search method, several attack states of multi concurrent session were found, and a new attack pattern was obtained.