基于著色Petri網(wǎng)的安全協(xié)議形式化分析理論與技術(shù)研究

《基于著色Petri網(wǎng)的安全協(xié)議形式化分析理論與技術(shù)研究》由會員上傳分享，免費在線閱讀，更多相關(guān)內(nèi)容在學術(shù)論文-天天文庫。

1、碩士學位論文Ｉ基于著色Ｐｅｔｒｉ網(wǎng)的安全協(xié)議形式化分析理論與技術(shù)研究作者姓名馬瑞潔指導教師姓名、職稱馬卓副教授？申請學位類別工學碩士基于著色Petri網(wǎng)的安全協(xié)議形式化分析理論與技術(shù)研究作者姓名馬瑞潔指導教師姓名、職稱馬卓副教授申請學位類別工學碩士學校代碼10701學號1503121520分類號TP39密級公開西安電子科技大學碩士學位論文基于著色Petri網(wǎng)的安全協(xié)議形式化分析理論與技術(shù)研究作者姓名：馬瑞潔一級學科：計算機科學與技術(shù)二級學科：計算機系統(tǒng)結(jié)構(gòu)學位類別：工學碩士指導教師

2、姓名、職稱：馬卓副教授學院：計算機學院提交日期：2018年4月OntheFormalDescriptionandAnalysisofSecurityProtocolsUsingColoredPetriNetsA?thesissubmitted?toXIDIAN?UNIVERSITYin?partial?fulfillment?of?the?requirementsfor?the?degreeof?Masterin?Computer?System?ArchitectureByMa?RuijieSupervi

3、sor:?Ma?ZhuoTitle:Associate?ProfessorApril?2018西安電子科技大學學位論文獨創(chuàng)性（或創(chuàng)新性）聲明秉承學校嚴謹?shù)膶W風和優(yōu)良的科學道德，本人聲明所呈交的論文是我個人在導師指導下進行的研究工作及取得的研究成果。盡我所知，除了文中特別加以標注和致謝中所羅列的內(nèi)容以外，論文中不包含其他人已經(jīng)發(fā)表或撰寫過的研究成果也不包含；為獲得西安電子科技大學或其它教育機構(gòu)的學位或證書而使用過的材料一。與我同工作的同事對本研宄所做的任何貢獻均已在論文中作了明確的說

4、明并表示了謝意。一學位論文若有不實之處，本人承擔切法律責任。本人簽名？＾秦主：日期：西安電子科技大學關(guān)于論文使用授權(quán)的說明？本人完全了解西安電子科技大學＾：關(guān)保留和使用學位論文的規(guī)定，即研宄生在一校攻讀學位期間論文工作的知識產(chǎn)權(quán)屬于西安電子科技大學。學校有權(quán)保留送交論文的復印件，允許查閱、借閱論文；學?？梢怨颊撐牡娜炕虿糠謨?nèi)容，允許采用影印、縮印或其它復制手段保存論文。同時本人保證，結(jié)合學位論文研宄成果完成的論文、發(fā)明專利等成果，署名單位為西安電子科技大學。

5、■＾傘客導師簽名本人簽名：：日期：ｇ日期：專ｑ認曰摘要摘要隨著無線傳感網(wǎng)領(lǐng)域和工業(yè)控制領(lǐng)域的不斷發(fā)展，網(wǎng)絡(luò)空間中的新興領(lǐng)域不斷產(chǎn)生，網(wǎng)絡(luò)通信機制也日益復雜。安全協(xié)議作為保障各類新興領(lǐng)域數(shù)據(jù)與服務(wù)資源的關(guān)鍵技術(shù)之一，近年來得到普遍關(guān)注。安全協(xié)議數(shù)量的激增，協(xié)議運行環(huán)境的差異，協(xié)議復雜度的提高，與設(shè)計分析人員主觀聯(lián)系密切等特點，導致安全協(xié)議的設(shè)計與分析成為極具挑戰(zhàn)性的課題。安全協(xié)議的形式化分析方法近年來取得了巨大進步，在模態(tài)邏輯、定理證明以及模型檢測等幾大分支都具有頗具影響力的代表方法。與

6、之相對應，基于計算模型的計算復雜性方法也在同步發(fā)展。該方法具有嚴謹?shù)臄?shù)學理論作為支撐，使用結(jié)構(gòu)復雜，對研究人員要求極高；此外，由于研究人員對協(xié)議的不同理解，在分析同種協(xié)議時，可能得到不同結(jié)果。與計算復雜性方法相比，基于符號模型的形式化分析方法由于自身的符號性和離散性，具有更簡單清晰的結(jié)構(gòu)，在與分布式計算機工程領(lǐng)域相結(jié)合方面，具備天生優(yōu)勢。并且，隨著業(yè)界安全協(xié)議數(shù)量的規(guī)模化，協(xié)議的自動化分析勢必成為協(xié)議安全性分析領(lǐng)域的重要趨勢。著色Petri網(wǎng)作為分布式異步并發(fā)系統(tǒng)分析中的最重要工具之一，具有二元性、圖形化

7、以及代數(shù)表示性的特點，既有清晰的結(jié)構(gòu)又有嚴謹?shù)臄?shù)學基礎(chǔ)；著色Petri網(wǎng)的輔助建模工具同時集成了自動化狀態(tài)空間分析的功能，通過補充修改，即可用于分析安全協(xié)議。本文正是利用其在分布式系統(tǒng)建模領(lǐng)域的優(yōu)勢，結(jié)合時態(tài)邏輯語句的狀態(tài)空間判決以及Dolev-Yao模型下的協(xié)議運行環(huán)境，提出一種基于著色Petri網(wǎng)的安全協(xié)議分析方法。該方法從攻擊者模型構(gòu)造出發(fā)，引入消息推理規(guī)則，形成了Dolev-Yao模型下使用著色Petri網(wǎng)建模分析協(xié)議安全性的理論。最后，本文以CPN?Tools形式化建模工具為基礎(chǔ)，結(jié)合上述理論方

8、法，實現(xiàn)了一套基于著色Petri網(wǎng)的安全協(xié)議分析原型系統(tǒng)。通過與業(yè)界主流安全協(xié)議自動化分析工具AVISPA的對比，結(jié)果表明，本文所提方法具有較強的可行性；并且攻擊者能力模型擴展后，能夠用于分析多數(shù)安全協(xié)議。關(guān)鍵詞：安全協(xié)議，著色Petri網(wǎng)，CPN?Tools，模型檢測，自動化IABSTRACTABSTRACTWith?the?continuous?development?of?wireless?sensor?network?