發(fā)布時(shí)間：2018-08-06 18:10

【摘要】：提出一種針對(duì)包含時(shí)間因素的安全協(xié)議的有色Petri(CPN)形式化分析方法,利用CPN Tools中的內(nèi)置全局自動(dòng)時(shí)鐘標(biāo)記,時(shí)間相關(guān)性質(zhì)可通過(guò)仿真和生成狀態(tài)圖進(jìn)行分析驗(yàn)證�；谶@一方法,對(duì)著名的NS協(xié)議(簡(jiǎn)化版)建模,來(lái)分析驗(yàn)證與時(shí)間相關(guān)的安全屬性。然后利用CPN Tools,采用CPN ML語(yǔ)言編寫(xiě)查詢函數(shù)驗(yàn)證協(xié)議的AUT性質(zhì),從而發(fā)現(xiàn)協(xié)議的漏洞。應(yīng)用分析結(jié)果表明方法有效,且操作簡(jiǎn)單容易理解。
[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.
【作者單位】： 華北科技學(xué)院計(jì)算機(jī)學(xué)院;中國(guó)科學(xué)院研究生院信息科學(xué)與工程學(xué)院;
【基金】：中國(guó)科學(xué)院研究生院院長(zhǎng)基金項(xiàng)目(Y15102HN00)
【分類(lèi)號(hào)】：TP393.08

【參考文獻(xiàn)】

相關(guān)期刊論文 前3條

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

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

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

【共引文獻(xiàn)】

相關(guān)期刊論文 前3條

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

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

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

相關(guān)博士學(xué)位論文 前1條

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

相關(guān)碩士學(xué)位論文 前7條

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

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

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

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

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

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

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

【二級(jí)參考文獻(xiàn)】

相關(guān)期刊論文 前8條

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

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

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

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

5 李夢(mèng)君;李舟軍;陳火旺;;安全協(xié)議的擴(kuò)展Horn邏輯模型及其驗(yàn)證方法[J];計(jì)算機(jī)學(xué)報(bào);2006年09期

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

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

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

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

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

2 趙華偉,李大興,秦靜;一種時(shí)間相關(guān)的分析安全協(xié)議的擴(kuò)展邏輯[J];計(jì)算機(jī)應(yīng)用;2005年10期

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

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

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

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

7 范紅,馮登國(guó);一個(gè)非否認(rèn)協(xié)議ZG的形式化分析[J];電子學(xué)報(bào);2005年01期

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

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

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

相關(guān)會(huì)議論文 前10條

1 劉家芬;周明天;;對(duì)安全協(xié)議重放攻擊的分類(lèi)研究(英文)[A];計(jì)算機(jī)技術(shù)與應(yīng)用進(jìn)展——全國(guó)第17屆計(jì)算機(jī)科學(xué)與技術(shù)應(yīng)用（CACIS）學(xué)術(shù)會(huì)議論文集（下冊(cè)）[C];2006年

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

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

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

5 文靜華;張梅;張煥國(guó);;電子支付協(xié)議的博弈邏輯模型與形式化分析[A];2007年全國(guó)開(kāi)放式分布與并行計(jì)算機(jī)學(xué)術(shù)會(huì)議論文集(上冊(cè))[C];2007年

6 林國(guó)璋;;博物館的時(shí)間因素[A];2004年科技館學(xué)術(shù)年會(huì)論文選編[C];2004年

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

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

9 徐銳;;設(shè)計(jì)安全協(xié)議[A];第十八次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集[C];2003年

10 張梅;文靜華;張煥國(guó);;基于ATL的電子商務(wù)協(xié)議建模與形式化分析[A];2009年全國(guó)開(kāi)放式分布與并行計(jì)算機(jī)學(xué)術(shù)會(huì)議論文集(上冊(cè))[C];2009年

相關(guān)重要報(bào)紙文章 前10條

1 萬(wàn)春萍　何Z，

本文編號(hào)：2168564