基于Petri网的密码协议形式化建模

Formal Modeling of Cryptographic Protocols Using Petri Nets

密码协议是安全共享网络资源的机制和规范,是构建网络安全环境的基石,其安全性对整个网络环境的安全起着至关重要的作用。提出了采用Colored Petri Nets(CPN,着色Petri网)分析密码协议的新方法。采用新方法对TMN协议的多次并发会话通信进行形式化建模,模型依据会话配置和会话顺序进行功能单元划分,采用on-the-fly方法生成攻击路径。采用状态空间搜索技术,发现了该协议的多次并发会话不安全状态,并获得了新的攻击模式。

Cryptographic protocol is secure mechanism for sharing network resources,is the cornerstone to build securitynetwork 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-the-fly method.Using the state space search method,several attack states of multi concurrent session were found,and a new attack pattern was obtained.