【摘要】：如何對(duì)電子商務(wù)協(xié)議進(jìn)行分析與驗(yàn)證一直是研究的熱點(diǎn),基于ATL(交替時(shí)態(tài)邏輯)對(duì)電子商務(wù)協(xié)議中的公平交換協(xié)議(Fair Exchange Protocols)進(jìn)行形式化分析與驗(yàn)證,并選取了其中的一個(gè)電子合同簽署協(xié)議進(jìn)行形式化驗(yàn)證。用ATL語(yǔ)言來形式化描述公平交換協(xié)議,并使用ATS(Alternating Transition Systems,交替轉(zhuǎn)移系統(tǒng))來為公平交換協(xié)議進(jìn)行形式化建模,再用形式化驗(yàn)證工具M(jìn)OCHA對(duì)公平交換協(xié)議的公平性(Fairness)、及時(shí)性(Timeliness)和不可濫用性(Abuse-Freeness)進(jìn)行有效的驗(yàn)證;對(duì)驗(yàn)證結(jié)果進(jìn)行分析與討論,發(fā)現(xiàn)了該協(xié)議不滿足公平性和不可濫用性,不符合設(shè)計(jì)的要求。
[Abstract]:How to analyze and verify the electronic commerce protocol has been a hot topic. Based on ATL (alternating temporal Logic), the fair exchange protocol (Fair Exchange Protocols) in the electronic commerce protocol is analyzed and verified formally. One of the electronic contract signing protocols is selected for formal verification. ATL language is used to formalize the fair exchange protocol, and ATS (Alternating Transition Systems, alternate transition system is used to model the fair exchange protocol. Then we use formal verification tool MOCHA to verify fairness (Fairness), timeliness (Timeliness) and non-abusing (Abuse-Freeness) of fair exchange protocol, analyze and discuss the verification results, and find that the protocol is not fair and non-abusing. Does not meet the design requirements.
【作者單位】： 暨南大學(xué)計(jì)算機(jī)科學(xué)系;
【基金】：國(guó)家自然科學(xué)基金(No.61003056,No.61272415) 國(guó)家重點(diǎn)基礎(chǔ)研究發(fā)展規(guī)劃(973)(No.2010CB328103)
【分類號(hào)】：TP393.04;TP301

【參考文獻(xiàn)】

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

1 王芷玲;張玉清;楊波;;一個(gè)公平電子合同簽署協(xié)議的設(shè)計(jì)[J];計(jì)算機(jī)工程;2006年19期

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

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

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

1 李樺;公平交換協(xié)議研究[D];電子科技大學(xué);2012年

【共引文獻(xiàn)】

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

1 劉海;彭長(zhǎng)根;任祉靜;;一種理性安全協(xié)議形式化分析方法及應(yīng)用[J];貴州大學(xué)學(xué)報(bào)(自然科學(xué)版);2014年06期

2 劉海;彭長(zhǎng)根;張弘;任祉靜;;一種理性安全協(xié)議的博弈邏輯描述模型[J];計(jì)算機(jī)科學(xué);2015年09期

3 翁立晨;汪學(xué)明;;公平的電子合同簽署協(xié)議的博弈分析與改進(jìn)[J];計(jì)算機(jī)工程與設(shè)計(jì);2010年24期

4 宋俊輝;謝華;;基于兩方的電子合同簽名協(xié)議模型研究[J];信息系統(tǒng)工程;2011年05期

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

1 趙銘偉;電子商務(wù)系統(tǒng)中信息資源安全管理的若干技術(shù)問題研究[D];大連理工大學(xué);2010年

2 范偉;移動(dòng)商務(wù)安全性研究[D];北京郵電大學(xué);2010年

3 徐偉峰;多主體模型定量驗(yàn)證方法研究[D];吉林大學(xué);2014年

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

1 丁廣泓;集成電路形式化驗(yàn)證的FPGA加速技術(shù)研究[D];廣西民族大學(xué);2015年

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

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

1 仲紅;黃劉生;羅永龍;;安全電子選舉研究[J];安徽大學(xué)學(xué)報(bào)(自然科學(xué)版);2007年03期

2 秦志光;羅緒成;;P2P共享系統(tǒng)中無需專用TTP的公平交換協(xié)議[J];電子科技大學(xué)學(xué)報(bào);2006年S1期

3 劉道斌,郭莉,白碩;基于Petri網(wǎng)的安全協(xié)議形式化分析[J];電子學(xué)報(bào);2004年11期

4 王彩芬,賈愛庫(kù),劉軍龍,于成尊;基于簽密的多方認(rèn)證郵件協(xié)議[J];電子學(xué)報(bào);2005年11期

5 王彩芬;俞惠芳;王會(huì)歌;易瑋;;一種新的多方多合同簽署協(xié)議[J];電子學(xué)報(bào);2007年10期

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

7 周勇;朱梧i，

本文編號(hào)：2204061