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

《基于Petri网的密码协议形式化建模.doc》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、基于Petri网的密码协议形式化建模基金项目：国家自然科学基金项目(No.61163011);国家重点基础研究发展规划(973)项目(No.2007CB310702);内蒙古自然科学基金重点项目(No.20080404ZD20)作者简介:白云莉(1977-)，副教授，博士研究生，主要研究领域为计算机网络与网络安全。叶新铭（1943-），教授，博士生导师，中国计算机学会高级会员，主要研究领域为计算机网络与分布式系统白云莉1,2叶新铭1(1内蒙古大学计算机学院，呼和浩特010021；2内蒙古农业大学计算机与信息工程学院，呼和浩特010018)(bai

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

3、会话中图分类号:TP393.06　　文献标识码:AFormalModelingofCryptographicProtocolsUsingPetriNetsBAIYunli1,2YEXinming1(baiyunli@vip.imau.edu.cn，xmy@imu.edu.cn)1(CollegeofComputerScience,InnerMongoliaUniversity，Hohhot010021,China)2(CollegeofComputerandInformationEngineering,InnerMongoliaAgricultu

4、ralUniversity，Hohhot010018,China)AbstractCryptographicprotocolissecuremechanismforsharingnetworkresources,isthecornerstonetobuildsecuritynetworkenvironment.Thesecurityofthecryptographicprotocolplaysavitalroletoentirenetworkenvironment.Inthispaper,anewColoredPetriNets(CPN)meth

5、odologyforsecurityanalysisofcryptographicprotocolisproposed.WeapplythenewapproachtomodelingTMNprotocolwithmulticoncurrentsession,andthemodeliscategorizedbasedonsessionconfigurationandsessionschedule.Andtheattacktracesareobtainedusingon–the-flymethod.Usingthestatespacesearchme

6、thod,severalattackstatesofmulticoncurrentsessionarefound,andanewattackpatternisobtained.KeywordsCryptographicprotocol;TMN;CPN;Multiconcurrentsession1引言密码协议是以密码学为基础的消息交换协议，其目的是在网络环境中避免恶意方攻击，从而达到预定安全目标。有很多种密码协议的应用：包括认证协议、密钥交换协议、电子商务协议、电子银行协议、电子投票协议等。由于与日俱增的攻击能力和应用需求的复杂化，使得设计与分析

7、密码协议越来越困难。很多密码协议的攻击是在使用很多年之后才发现的。因此对密码协议进行形式化建模，对其所存在的攻击进行分析是非常有价值的。常用的形式化分析方法有：BAN逻辑法、进程代数法、串空间、π演算和Petri网。其中Petri网具有异步并发特性,与物理系统极其接近,适合于描述网络体系结构、服务和协议,此外它采用直观的图形表示,具有严密的数学理论和丰富的分析技术便于进行协议的验证工作。以往基于Petri网的密码协议分析与验证工作主要针对单会话过程进行的。本文提出了一种新的基于ColoredPetriNets（CPN，着色Petri网）的密码协议

8、多并发会话的形式化建模方法，并以密钥交互协议—TMN协议为例说明了新方法有效性。我们在模型检测工具CPNTools中实现了新方法，有效地