【摘要】：針對現(xiàn)有顏色Petri網(wǎng)方法未能分析時限性的缺點,提出一種基于顏色Petri網(wǎng)的電子商務(wù)協(xié)議分析方法,用于分析可追究性、公平性和時限性三個重要安全屬性.針對時限性建立了表示主體是否成功接收消息的狀態(tài)顏色集和主體自定義的時間顏色集,并充分考慮時限性對公平性的影響,更加有效地分析公平性.文中以KZG協(xié)議為例,建立了KZG的分層顏色Petri網(wǎng)模型,利用CPN Tools工具對該模型仿真運行,并通過狀態(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)新項目(09213562Z)資助 河北省自然科學(xué)基金青年科學(xué)(G2011203195)資助
【分類號】：TP393.04

【參考文獻】

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

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

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

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

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

【共引文獻】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

7 陳黎潔;列車運行控制系統(tǒng)安全通信協(xié)議驗證方法的研究[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 郝天保;基于模糊時間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)的擴展α過程挖掘算法[D];哈爾濱工程大學(xué);2011年

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

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

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

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

【二級參考文獻】

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

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

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

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

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

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

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

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

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

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

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

【相似文獻】

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

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

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

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

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

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

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

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

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

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

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

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

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

2 余興超;馬爭先;王玉斌;董榮勝;;基于UPPAAL的簡單網(wǎng)絡(luò)支付協(xié)議形式化驗證[A];廣西計算機學(xué)會2010年學(xué)術(shù)年會論文集[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é)議形式化方法及模型檢測技術(shù)的研究與應(yīng)用[D];貴州大學(xué);2006年

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

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

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

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

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

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

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

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

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

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

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

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

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

5 計宏霖;基于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é)議的形式化描述與驗證[D];重慶大學(xué);2004年

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

，

本文編號：2510974