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

【摘要】：提出一種擴(kuò)展的有窮自動(dòng)機(jī)模型,并結(jié)合卿-周邏輯給出一種新的電子商務(wù)協(xié)議形式化分析方法,用于分析電子商務(wù)協(xié)議的可追究性、公平性和時(shí)限性.該方法結(jié)合了模型檢測(cè)和邏輯分析兩種形式化分析方法的優(yōu)點(diǎn),可以準(zhǔn)確形象地描述協(xié)議的具體運(yùn)行過程,并且在發(fā)生重放攻擊時(shí)能夠正確分析各方的責(zé)任.利用該方法對(duì)Kim等人提出的改進(jìn)版ZG協(xié)議進(jìn)行了實(shí)例分析,給出了描述該協(xié)議運(yùn)行過程的狀態(tài)轉(zhuǎn)換圖,結(jié)合狀態(tài)轉(zhuǎn)換圖對(duì)該協(xié)議分析得出其滿足可追究性、公平性、時(shí)限性,并且不存在被重放攻擊的可能.最后用時(shí)間自動(dòng)機(jī)UPPAAL驗(yàn)證了新方法中有窮自動(dòng)機(jī)模型的準(zhǔn)確性和時(shí)限性分析的有效性.
[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).
【作者單位】： 燕山大學(xué)信息科學(xué)與工程學(xué)院;燕山大學(xué)里仁學(xué)院;
【基金】：河北省重大技術(shù)創(chuàng)新項(xiàng)目(09213562Z)資助 河北省自然科學(xué)基金青年科學(xué)(G2011203195)資助
【分類號(hào)】：TP393.04;F713.36

【參考文獻(xiàn)】

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

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

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

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

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

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

【共引文獻(xiàn)】

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

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

2 黃曉芳;賴欣;馬兆豐;楊義先;鈕心忻;;計(jì)費(fèi)公平的安全移動(dòng)數(shù)字版權(quán)管理方案[J];電子科技大學(xué)學(xué)報(bào);2009年02期

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

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

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

6 周勇;朱梧i，

本文編號(hào)：1525804