本文關鍵詞： 電子商務協(xié)議 形式化分析 有窮自動機 邏輯分析　出處：《小型微型計算機系統(tǒng)》2013年03期 　論文類型：期刊論文

【摘要】：提出一種擴展的有窮自動機模型,并結合卿-周邏輯給出一種新的電子商務協(xié)議形式化分析方法,用于分析電子商務協(xié)議的可追究性、公平性和時限性.該方法結合了模型檢測和邏輯分析兩種形式化分析方法的優(yōu)點,可以準確形象地描述協(xié)議的具體運行過程,并且在發(fā)生重放攻擊時能夠正確分析各方的責任.利用該方法對Kim等人提出的改進版ZG協(xié)議進行了實例分析,給出了描述該協(xié)議運行過程的狀態(tài)轉換圖,結合狀態(tài)轉換圖對該協(xié)議分析得出其滿足可追究性、公平性、時限性,并且不存在被重放攻擊的可能.最后用時間自動機UPPAAL驗證了新方法中有窮自動機模型的準確性和時限性分析的有效性.
[Abstract]:In this paper, an extended finite automaton model is proposed, and a new formal analysis method of electronic commerce protocol is presented, which can be used to analyze the accountability of electronic commerce protocol. This method combines the advantages of two formal analysis methods, model checking and logic analysis, and can describe the specific running process of the protocol accurately and vividly. And when replay attack occurs, the responsibility of all parties can be correctly analyzed. By using this method, the improved ZG protocol proposed by Kim et al is analyzed as an example, and the state transition diagram describing the running process of the protocol is given. According to the analysis of the protocol based on the state transition diagram, it can be concluded that the protocol meets the requirements of accountability, fairness and time limit. Moreover, there is no possibility of being attacked by replay. Finally, the accuracy of the finite automaton model and the validity of the time-limited analysis in the new method are verified by using the timed automaton (UPPAAL).
【作者單位】： 燕山大學信息科學與工程學院;燕山大學里仁學院;
【基金】：河北省重大技術創(chuàng)新項目(09213562Z)資助 河北省自然科學基金青年科學(G2011203195)資助
【分類號】：TP393.04;F713.36

【參考文獻】

相關期刊論文 前5條

1 郭華;李舟軍;莊雷;計宏霖;;一種新的電子商務協(xié)議分析方法[J];計算機科學;2010年08期

2 劉家芬;周明天;;對安全協(xié)議重放攻擊的分類研究[J];計算機應用研究;2007年03期

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

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

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

【共引文獻】

相關期刊論文 前10條

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

2 黃曉芳;賴欣;馬兆豐;楊義先;鈕心忻;;計費公平的安全移動數(shù)字版權管理方案[J];電子科技大學學報;2009年02期

3 崔軍;劉琦;張振濤;李忠獻;楊義先;;可轉換認證加密的安全郵件協(xié)議[J];電子科技大學學報;2010年04期

4 馮春莉;;優(yōu)化網上數(shù)碼商店設計與實現(xiàn)[J];電腦編程技巧與維護;2011年08期

5 劉冬梅;卿斯?jié)h;侯玉文;李鵬飛;;一種基于適應度函數(shù)遺傳算法的公平交換協(xié)議自動生成方法[J];電子學報;2010年05期

6 周勇;朱梧i，

本文編號：1525804