【摘要】：針對(duì)現(xiàn)有顏色Petri網(wǎng)方法未能分析時(shí)限性的缺點(diǎn),提出一種基于顏色Petri網(wǎng)的電子商務(wù)協(xié)議分析方法,用于分析可追究性、公平性和時(shí)限性三個(gè)重要安全屬性.針對(duì)時(shí)限性建立了表示主體是否成功接收消息的狀態(tài)顏色集和主體自定義的時(shí)間顏色集,并充分考慮時(shí)限性對(duì)公平性的影響,更加有效地分析公平性.文中以KZG協(xié)議為例,建立了KZG的分層顏色Petri網(wǎng)模型,利用CPN Tools工具對(duì)該模型仿真運(yùn)行,并通過狀態(tài)空間和查詢函數(shù)分析了協(xié)議的性質(zhì),證明了本方法的有效性.
[Abstract]:In view of the fact that the existing color Petri net methods fail to analyze the time limit, an e-commerce protocol analysis method based on color Petri net is proposed, which is used to analyze three important security attributes: traceability, fairness and time limit. Aiming at the time limit, the state color set which represents whether the agent successfully receives the message or not and the time color set defined by the agent are established, and the fairness is analyzed more effectively by fully considering the influence of time limit on fairness. In this paper, taking KZG protocol as an example, the hierarchical color Petri net model of KZG is established, and the model is simulated by CPN Tools tool. The properties of the protocol are analyzed by state space and query function, and the effectiveness of the method is proved.
【作者單位】： 燕山大學(xué)信息科學(xué)與工程學(xué)院;燕山大學(xué)里仁學(xué)院;
【基金】：河北省重大技術(shù)創(chuàng)新項(xiàng)目(09213562Z)資助 河北省自然科學(xué)基金青年科學(xué)(G2011203195)資助
【分類號(hào)】：TP393.04

【參考文獻(xiàn)】

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

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

2 黎波濤,羅軍舟;不可否認(rèn)協(xié)議的Petri網(wǎng)建模與分析[J];計(jì)算機(jī)研究與發(fā)展;2005年09期

3 于楓;羅軍舟;李偉;王鵬;;一種基于進(jìn)程驗(yàn)證的Petri網(wǎng)可達(dá)性判定方法[J];計(jì)算機(jī)學(xué)報(bào);2010年02期

4 劉文琦;顧宏;;電子支付協(xié)議可追究性的Petri網(wǎng)建模與分析[J];系統(tǒng)仿真學(xué)報(bào);2008年20期

【共引文獻(xiàn)】

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

1 唐明偉;宋文;葉劍虹;;發(fā)送-接收問題的Petri網(wǎng)建模與驗(yàn)證[J];電子科技大學(xué)學(xué)報(bào);2007年S3期

2 魏星;隋新;;SIP協(xié)議的形式化分析與驗(yàn)證[J];桂林航天工業(yè)高等�？茖W(xué)校學(xué)報(bào);2009年01期

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

4 李鑫;李仲學(xué);李翠平;;基于Agent技術(shù)的井下運(yùn)輸仿真模型研究[J];金屬礦山;2011年12期

5 劉云;鄭紅;;基于Petri網(wǎng)的數(shù)字家庭無線射頻協(xié)議研究[J];計(jì)算機(jī)應(yīng)用與軟件;2011年10期

6 楊鵬;包廣斌;魯江;;基于廣義隨機(jī)Petri網(wǎng)的SIP的吞吐量性能研究[J];甘肅廣播電視大學(xué)學(xué)報(bào);2010年03期

7 白云莉;葉新銘;;基于Petri網(wǎng)的密碼協(xié)議形式化建模[J];計(jì)算機(jī)科學(xué);2012年08期

8 范玉濤;蘇桂平;;一種含時(shí)間因素的安全協(xié)議形式化分析方法[J];計(jì)算機(jī)應(yīng)用與軟件;2013年01期

9 楊夏妮;龍法寧;張遠(yuǎn)夏;;基于約束優(yōu)化的Petri網(wǎng)可達(dá)性分析[J];計(jì)算機(jī)應(yīng)用;2013年04期

10 楊夏妮;;Petri網(wǎng)可達(dá)性的偽標(biāo)識(shí)判定法[J];計(jì)算機(jī)應(yīng)用與軟件;2013年04期

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

1 楊鵬;袁占亭;王繼曾;;基于廣義隨機(jī)Petri網(wǎng)的SIP的性能分析[A];第六屆全國信息獲取與處理學(xué)術(shù)會(huì)議論文集（3）[C];2008年

2 楊鵬;袁占亭;王繼曾;;基于廣義隨機(jī)Petri網(wǎng)的SIP的時(shí)延分析[A];第三屆全國虛擬儀器大會(huì)論文集[C];2008年

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

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

2 張立臣;面向普適計(jì)算的主動(dòng)訪問控制模型研究[D];陜西師范大學(xué);2011年

3 劉文琦;移動(dòng)支付系統(tǒng)安全的若干關(guān)鍵問題研究[D];大連理工大學(xué);2008年

4 李艷平;若干安全協(xié)議的研究與設(shè)計(jì)[D];西安電子科技大學(xué);2009年

5 李良;中國電子銀行風(fēng)險(xiǎn)評(píng)估研究[D];大連理工大學(xué);2010年

6 董學(xué)文;基于串空間模型安全協(xié)議形式化方法的分析與擴(kuò)展[D];西安電子科技大學(xué);2011年

7 陳黎潔;列車運(yùn)行控制系統(tǒng)安全通信協(xié)議驗(yàn)證方法的研究[D];北京交通大學(xué);2013年

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

1 劉云;數(shù)字家庭無線射頻協(xié)議的形式化分析與研究[D];華東理工大學(xué);2011年

2 蘇曼;基于Petri網(wǎng)的數(shù)字家庭無線抄表建模與分析[D];華東理工大學(xué);2011年

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

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

5 劉玉磊;基于Petri網(wǎng)模型的數(shù)據(jù)批處理系統(tǒng)研究與應(yīng)用[D];哈爾濱工程大學(xué);2011年

6 吳蘇;一種可發(fā)現(xiàn)復(fù)雜循環(huán)結(jié)構(gòu)的擴(kuò)展α過程挖掘算法[D];哈爾濱工程大學(xué);2011年

7 劉波;基于Petri網(wǎng)的網(wǎng)絡(luò)入侵檢測(cè)系統(tǒng)研究與實(shí)現(xiàn)[D];南京郵電大學(xué);2012年

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

9 范鈺丹;密碼協(xié)議非否認(rèn)性和公平性驗(yàn)證技術(shù)研究[D];解放軍信息工程大學(xué);2007年

10 唐明偉;Petri網(wǎng)在網(wǎng)絡(luò)性能評(píng)價(jià)中的研究與應(yīng)用[D];西華大學(xué);2008年

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

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

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

2 于楓;羅軍舟;李偉;;基于T-不變量消除的Petri網(wǎng)合法變遷引發(fā)序列判定算法[J];解放軍理工大學(xué)學(xué)報(bào)(自然科學(xué)版);2008年05期

3 吳哲輝,王培良,趙茂先;無界公平Petri網(wǎng)的進(jìn)程表達(dá)式[J];計(jì)算機(jī)學(xué)報(bào);2000年04期

4 曾慶田,吳哲輝;Petri網(wǎng)的進(jìn)程網(wǎng)系統(tǒng)[J];計(jì)算機(jī)學(xué)報(bào);2002年12期

5 曾慶田,吳哲輝;無界Petri網(wǎng)的進(jìn)程表達(dá)式[J];計(jì)算機(jī)學(xué)報(bào);2003年12期

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

7 曾慶田;;一種基于同步合成構(gòu)造Petri網(wǎng)進(jìn)程表達(dá)式的方法[J];計(jì)算機(jī)學(xué)報(bào);2008年03期

8 卿斯?jié)h;一種新型的非否認(rèn)協(xié)議[J];軟件學(xué)報(bào);2000年10期

9 李先賢,懷進(jìn)鵬;公平的非否認(rèn)密碼協(xié)議及其形式分析與應(yīng)用[J];軟件學(xué)報(bào);2000年12期

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

【相似文獻(xiàn)】

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

1 王兵;肖美華;劉曉清;朱宜炳;;電子商務(wù)協(xié)議原子性的SPIN分析[J];南昌大學(xué)學(xué)報(bào)(工科版);2007年02期

2 董榮勝;郭云川;古天龍;;一種電子商務(wù)協(xié)議原子性的模型檢驗(yàn)分析方法[J];計(jì)算機(jī)科學(xué);2005年04期

3 張梅,文靜華,楊滋榮,李祥;CMP1協(xié)議的符號(hào)模型檢驗(yàn)分析[J];海軍工程大學(xué)學(xué)報(bào);2005年03期

4 郭云川;丁麗;周淵;郭莉;;基于ProVerif的電子商務(wù)協(xié)議分析[J];通信學(xué)報(bào);2009年03期

5 ;電子技術(shù)應(yīng)用[J];電子科技文摘;2001年08期

6 郭云川;古天龍;董榮勝;蔡國永;;電子商務(wù)協(xié)議形式化分析的一種新方法[J];計(jì)算機(jī)科學(xué);2004年08期

7 文靜華;張梅;李祥;;ISI協(xié)議的符號(hào)模型檢驗(yàn)分析[J];電訊技術(shù);2005年06期

8 譚新蓮;李磊;;安全電子商務(wù)協(xié)議的形式化分析[J];數(shù)學(xué)愛好者(教育學(xué)術(shù));2008年02期

9 劉文遠(yuǎn),邸鶴;帶有公平電子合同的交易協(xié)議[J];微機(jī)發(fā)展;2005年11期

10 文靜華;張梅;李祥;;基于博弈的電子商務(wù)協(xié)議分析[J];通信學(xué)報(bào);2006年03期

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

1 崔楠;汪學(xué)明;;基于SVO邏輯的電子商務(wù)協(xié)議非否認(rèn)性形式化分析[A];邏輯學(xué)及其應(yīng)用研究——第四屆全國邏輯系統(tǒng)、智能科學(xué)與信息科學(xué)學(xué)術(shù)會(huì)議論文集[C];2008年

2 余興超;馬爭先;王玉斌;董榮勝;;基于UPPAAL的簡單網(wǎng)絡(luò)支付協(xié)議形式化驗(yàn)證[A];廣西計(jì)算機(jī)學(xué)會(huì)2010年學(xué)術(shù)年會(huì)論文集[C];2010年

3 侯紅霞;;信息安全專業(yè)“安全協(xié)議”課程的教改探討[A];Proceedings of 2011 National Teaching Seminar on Cryptography and Information Security(NTS-CIS 2011) Vol.1[C];2011年

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

1 李云峰;電子商務(wù)協(xié)議安全性的形式化分析方法研究[D];西南交通大學(xué);2009年

2 文靜華;電子商務(wù)協(xié)議形式化方法及模型檢測(cè)技術(shù)的研究與應(yīng)用[D];貴州大學(xué);2006年

3 龍士工;串空間理論及其在安全協(xié)議分析中的應(yīng)用研究[D];貴州大學(xué);2007年

4 石曙東;網(wǎng)絡(luò)協(xié)議安全性分析中的邏輯化方法研究[D];華中科技大學(xué);2009年

5 李鋒;移動(dòng)支付安全研究[D];山東大學(xué);2008年

6 劉文琦;移動(dòng)支付系統(tǒng)安全的若干關(guān)鍵問題研究[D];大連理工大學(xué);2008年

7 孟博;電子商務(wù)環(huán)境中在線支付協(xié)議和抗抵賴協(xié)議的研究[D];武漢理工大學(xué);2003年

8 陳莉;電子商務(wù)安全協(xié)議的設(shè)計(jì)與分析[D];解放軍信息工程大學(xué);2009年

9 邢育紅;公平交換協(xié)議分析方法研究[D];山東大學(xué);2005年

10 李向東;公平交換協(xié)議的形式化分析與設(shè)計(jì)[D];解放軍信息工程大學(xué);2009年

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

1 魏剛;基于知識(shí)和信念模型的電子商務(wù)協(xié)議分析[D];燕山大學(xué);2012年

2 馬生;有窮機(jī)和邏輯結(jié)合的電子商務(wù)協(xié)議分析方法[D];燕山大學(xué);2012年

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

4 胡磊;安全協(xié)議形式化分析方法的融合性研究[D];南昌大學(xué);2007年

5 計(jì)宏霖;基于UPPAAL的電子商務(wù)協(xié)議安全性分析[D];解放軍信息工程大學(xué);2008年

6 何加亮;形式化邏輯方法在分析認(rèn)證協(xié)議以及電子商務(wù)協(xié)議中的應(yīng)用[D];吉林大學(xué);2004年

7 王兵;電子商務(wù)協(xié)議的形式化分析[D];南昌大學(xué);2007年

8 吳建耀;電子商務(wù)安全協(xié)議的形式化分析技術(shù)研究[D];西安電子科技大學(xué);2005年

9 代新敏;網(wǎng)絡(luò)安全協(xié)議的形式化描述與驗(yàn)證[D];重慶大學(xué);2004年

10 黨繼勝;基于SVO邏輯的電子商務(wù)協(xié)議形式化分析與研究[D];貴州大學(xué);2007年

，

本文編號(hào)：2510974