資源描述：
《基于Petri網(wǎng)的密碼協(xié)議形式化建模.doc》由會員上傳分享，免費在線閱讀，更多相關內(nèi)容在行業(yè)資料-天天文庫。
1、基于Petri網(wǎng)的密碼協(xié)議形式化建?；痦椖浚簢易匀豢茖W基金項目(No.61163011);國家重點基礎研究發(fā)展規(guī)劃(973)項目(No.2007CB310702);內(nèi)蒙古自然科學基金重點項目(No.20080404ZD20)作者簡介:白云莉(1977-)，副教授，博士研究生，主要研究領域為計算機網(wǎng)絡與網(wǎng)絡安全。葉新銘（1943-），教授，博士生導師，中國計算機學會高級會員，主要研究領域為計算機網(wǎng)絡與分布式系統(tǒng)白云莉1,2葉新銘1(1內(nèi)蒙古大學計算機學院，呼和浩特010021；2內(nèi)蒙古農(nóng)業(yè)大學計算機與信息工程學院，呼和浩特010018)(bai
2、yunli@vip.imau.edu.cn，xmy@imu.edu.cn)摘要密碼協(xié)議是安全共享網(wǎng)絡資源的機制和規(guī)范，是構建網(wǎng)絡安全環(huán)境的基石，其安全性對整個網(wǎng)絡環(huán)境的安全起著至關重要的作用。本文提出了采用ColoredPetriNets（CPN，著色Petri網(wǎng)）分析密碼協(xié)議的新方法。采用新方法對TMN協(xié)議進行多次并發(fā)會話通信的形式化建模，模型依據(jù)會話配置和會話順序進行功能單元劃分，采用on-the-fly方法生成攻擊路徑。采用狀態(tài)空間搜索技術，發(fā)現(xiàn)了該協(xié)議的多次并發(fā)會話不安全狀態(tài)，并獲得了新的攻擊模式。關鍵詞密碼協(xié)議，TMN，CPN，多次并發(fā)
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引言密碼協(xié)議是以密碼學為基礎的消息交換協(xié)議，其目的是在網(wǎng)絡環(huán)境中避免惡意方攻擊，從而達到預定安全目標。有很多種密碼協(xié)議的應用：包括認證協(xié)議、密鑰交換協(xié)議、電子商務協(xié)議、電子銀行協(xié)議、電子投票協(xié)議等。由于與日俱增的攻擊能力和應用需求的復雜化，使得設計與分析
7、密碼協(xié)議越來越困難。很多密碼協(xié)議的攻擊是在使用很多年之后才發(fā)現(xiàn)的。因此對密碼協(xié)議進行形式化建模，對其所存在的攻擊進行分析是非常有價值的。常用的形式化分析方法有：BAN邏輯法、進程代數(shù)法、串空間、π演算和Petri網(wǎng)。其中Petri網(wǎng)具有異步并發(fā)特性,與物理系統(tǒng)極其接近,適合于描述網(wǎng)絡體系結構、服務和協(xié)議,此外它采用直觀的圖形表示,具有嚴密的數(shù)學理論和豐富的分析技術便于進行協(xié)議的驗證工作。以往基于Petri網(wǎng)的密碼協(xié)議分析與驗證工作主要針對單會話過程進行的。本文提出了一種新的基于ColoredPetriNets（CPN，著色Petri網(wǎng)）的密碼協(xié)議
8、多并發(fā)會話的形式化建模方法，并以密鑰交互協(xié)議—TMN協(xié)議為例說明了新方法有效性。我們在模型檢測工具CPNTools中實現(xiàn)了新方法，有效地
