【摘要】：提出一種針對包含時間因素的安全協(xié)議的有色Petri(CPN)形式化分析方法,利用CPN Tools中的內(nèi)置全局自動時鐘標記,時間相關性質(zhì)可通過仿真和生成狀態(tài)圖進行分析驗證�；谶@一方法,對著名的NS協(xié)議(簡化版)建模,來分析驗證與時間相關的安全屬性。然后利用CPN Tools,采用CPN ML語言編寫查詢函數(shù)驗證協(xié)議的AUT性質(zhì),從而發(fā)現(xiàn)協(xié)議的漏洞。應用分析結(jié)果表明方法有效,且操作簡單容易理解。
[Abstract]:This paper presents a formal analysis method of colored Petri (CPN) for security protocols with time factors. By using the built-in global automatic clock tag in CPN Tools, the property of time correlation can be analyzed and verified by simulation and generation of state diagrams. Based on this method, the famous NS protocol (simplified version) is modeled to analyze the security properties related to time. Then, using CPN tools, we use CPN ML language to write query function to verify the AUT nature of the protocol, so as to discover the protocol vulnerabilities. The application results show that the method is effective and easy to understand.
【作者單位】： 華北科技學院計算機學院;中國科學院研究生院信息科學與工程學院;
【基金】：中國科學院研究生院院長基金項目(Y15102HN00)
【分類號】：TP393.08

【參考文獻】

相關期刊論文 前3條

1 劉文琦;顧宏;;基于分層時間有色Petri網(wǎng)的支付協(xié)議公平性分析[J];電子與信息學報;2009年06期

2 蘇桂平;孫莎;;一種基于有色Petri網(wǎng)的安全協(xié)議分析方法研究[J];微型機與應用;2011年15期

3 吳瑞龍;李陶深;;基于有色Petri網(wǎng)模型的安全協(xié)議檢測方法[J];微電子學與計算機;2006年03期

【共引文獻】

相關期刊論文 前3條

1 葉紅;袁志祥;;SET協(xié)議的持卡人匿名性分析[J];安徽工業(yè)大學學報(自然科學版);2010年02期

2 陳家偉;王知衍;張艷青;;基于Petri網(wǎng)的流程挖掘算法設計與應用[J];計算機工程與設計;2010年10期

3 林宏剛;胡勇;;WAP環(huán)境下移動支付協(xié)議公平性分析[J];四川大學學報(工程科學版);2013年03期

相關博士學位論文 前1條

1 楊鵬;基于廣義隨機Petri網(wǎng)理論的SIP的研究[D];蘭州理工大學;2009年

相關碩士學位論文 前7條

1 晁媛媛;基于分層思想的基本通信系統(tǒng)CPN建模[D];山東大學;2011年

2 郝天保;基于模糊時間Petri網(wǎng)的并行工作流模型研究[D];燕山大學;2011年

3 折建峰;WAP事務層協(xié)議的有色PETRI網(wǎng)建模與分析[D];武漢科技大學;2007年

4 呂波;IPv6環(huán)境下IKEv2的形式化分析及應用研究[D];貴州大學;2007年

5 劉煩;基于著色Petri網(wǎng)的發(fā)布/訂閱系統(tǒng)的建模與分析[D];中國石油大學;2008年

6 張生財;SCTP關聯(lián)管理的有色Petri網(wǎng)建模與分析[D];蘭州理工大學;2009年

7 盧貝;顏色Petri網(wǎng)的電子商務協(xié)議形式化分析方法研究[D];燕山大學;2012年

【二級參考文獻】

相關期刊論文 前8條

1 文靜華;李祥;張煥國;梁敏;張梅;;基于ATL的公平電子商務協(xié)議形式化分析[J];電子與信息學報;2007年04期

2 懷進鵬,李先賢;密碼協(xié)議的代數(shù)模型及其安全性[J];中國科學E輯:技術科學;2003年12期

3 劉道斌,郭莉,白碩;一種新的安全協(xié)議驗證方法[J];計算機研究與發(fā)展;2003年10期

4 王彩芬,葛建華;一種分析電子商務協(xié)議的新方法[J];計算機學報;2004年04期

5 李夢君;李舟軍;陳火旺;;安全協(xié)議的擴展Horn邏輯模型及其驗證方法[J];計算機學報;2006年09期

6 周典萃 ,卿斯?jié)h ,周展飛;一種分析電子商務協(xié)議的新工具[J];軟件學報;2001年09期

7 杜玉越,蔣昌俊;網(wǎng)上證券交易系統(tǒng)的時序Petri網(wǎng)描述及驗證[J];軟件學報;2002年08期

8 卿斯?jié)h;一種電子商務協(xié)議形式化分析方法[J];軟件學報;2005年10期

【相似文獻】

相關期刊論文 前10條

1 劉晶;伏飛;肖軍模;;Ad Hoc網(wǎng)絡安全路由協(xié)議形式化分析模型[J];解放軍理工大學學報(自然科學版);2008年03期

2 趙華偉,李大興,秦靜;一種時間相關的分析安全協(xié)議的擴展邏輯[J];計算機應用;2005年10期

3 吳建耀;張玉清;楊波;;SET支付協(xié)議的形式化分析與改進[J];計算機工程;2006年03期

4 劉晶;伏飛;肖軍模;;擴展Meadows模型分析Ad Hoc網(wǎng)絡路由協(xié)議安全性[J];應用科學學報;2008年03期

5 馮登國,范紅;安全協(xié)議形式化分析理論與方法研究綜述[J];中國科學院研究生院學報;2003年04期

6 李韶光,張險峰,秦志光;一個基于活體指紋的用戶身份認證協(xié)議及其形式化分析[J];重慶郵電學院學報(自然科學版);2004年06期

7 范紅,馮登國;一個非否認協(xié)議ZG的形式化分析[J];電子學報;2005年01期

8 羅志宏;朱思銘;;有色Petri網(wǎng)的一種密碼協(xié)議建模分析[J];現(xiàn)代計算機;2006年02期

9 文靜華;張梅;李祥;;一種新的密碼協(xié)議分析方法及其應用[J];計算機應用;2006年05期

10 王惠斌;常青美;祝躍飛;;基于PDS的IKE安全協(xié)議形式化分析[J];河南師范大學學報(自然科學版);2007年03期

相關會議論文 前10條

1 劉家芬;周明天;;對安全協(xié)議重放攻擊的分類研究(英文)[A];計算機技術與應用進展——全國第17屆計算機科學與技術應用（CACIS）學術會議論文集（下冊）[C];2006年

2 范銳;劉小輝;;企業(yè)實體構件動態(tài)演化模型[A];2009中國控制與決策會議論文集（3）[C];2009年

3 王焱;夏夢芹;曾家智;;CPN在可靠數(shù)據(jù)傳輸機制中的建模研究[A];系統(tǒng)仿真技術及其應用（第7卷）——'2005系統(tǒng)仿真技術及其應用學術交流會論文選編[C];2005年

4 周家浩;王建民;聞立杰;;基于CPN的工作流管理系統(tǒng)訪問控制技術研究與實現(xiàn)[A];第二十二屆中國數(shù)據(jù)庫學術會議論文集（技術報告篇）[C];2005年

5 文靜華;張梅;張煥國;;電子支付協(xié)議的博弈邏輯模型與形式化分析[A];2007年全國開放式分布與并行計算機學術會議論文集(上冊)[C];2007年

6 林國璋;;博物館的時間因素[A];2004年科技館學術年會論文選編[C];2004年

7 李秋山;胡游君;;低成本RFID系統(tǒng)安全協(xié)議設計及其形式化分析[A];2006北京地區(qū)高校研究生學術交流會——通信與信息技術會議論文集（上）[C];2006年

8 柳芳;;淺談《內(nèi)經(jīng)》中有關針灸時間因素的論述[A];第十三屆針灸對機體功能的調(diào)節(jié)機制及針灸臨床獨特經(jīng)驗學術研討會暨第三屆經(jīng)絡分會委員會會議論文集[C];2008年

9 徐銳;;設計安全協(xié)議[A];第十八次全國計算機安全學術交流會論文集[C];2003年

10 張梅;文靜華;張煥國;;基于ATL的電子商務協(xié)議建模與形式化分析[A];2009年全國開放式分布與并行計算機學術會議論文集(上冊)[C];2009年

相關重要報紙文章 前10條

1 萬春萍　何Z，

本文編號：2168564