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