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

Formal Modeling of Cryptographic Protocols Using Petri Nets

作　　者：白云莉[1,2] 叶新铭[1] 

机构地区：[1]内蒙古大学计算机学院,呼和浩特010021 [2]内蒙古农业大学计算机与信息工程学院,呼和浩特010018

出　　处：《计算机科学》2012年第8期70-74,共5页Computer Science

基　　金：国家自然科学基金项目(61163011);国家重点基础研究发展规划(973)项目(2007CB310702);内蒙古自然科学基金重点项目(20080404ZD20)资助

摘　　要：密码协议是安全共享网络资源的机制和规范,是构建网络安全环境的基石,其安全性对整个网络环境的安全起着至关重要的作用。提出了采用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.

关 键 词：密码协议 TMN CPN 多次并发会话 

分 类 号：TP393.06[自动化与计算机技术—计算机应用技术]