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