基于ATL的公平交换协议的形式化验证

发布时间：2018-08-26 06:49

【摘要】：如何对电子商务协议进行分析与验证一直是研究的热点,基于ATL(交替时态逻辑)对电子商务协议中的公平交换协议(Fair Exchange Protocols)进行形式化分析与验证,并选取了其中的一个电子合同签署协议进行形式化验证。用ATL语言来形式化描述公平交换协议,并使用ATS(Alternating Transition Systems,交替转移系统)来为公平交换协议进行形式化建模,再用形式化验证工具MOCHA对公平交换协议的公平性(Fairness)、及时性(Timeliness)和不可滥用性(Abuse-Freeness)进行有效的验证;对验证结果进行分析与讨论,发现了该协议不满足公平性和不可滥用性,不符合设计的要求。
[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.
【作者单位】： 暨南大学计算机科学系;
【基金】：国家自然科学基金(No.61003056,No.61272415) 国家重点基础研究发展规划(973)(No.2010CB328103)
【分类号】：TP393.04;TP301

【参考文献】

相关期刊论文 前1条

1 王芷玲;张玉清;杨波;;一个公平电子合同签署协议的设计[J];计算机工程;2006年19期

相关博士学位论文 前1条

1 李云峰;电子商务协议安全性的形式化分析方法研究[D];西南交通大学;2009年

相关硕士学位论文 前1条

1 李桦;公平交换协议研究[D];电子科技大学;2012年

【共引文献】

相关期刊论文 前4条

1 刘海;彭长根;任祉静;;一种理性安全协议形式化分析方法及应用[J];贵州大学学报(自然科学版);2014年06期

2 刘海;彭长根;张弘;任祉静;;一种理性安全协议的博弈逻辑描述模型[J];计算机科学;2015年09期

3 翁立晨;汪学明;;公平的电子合同签署协议的博弈分析与改进[J];计算机工程与设计;2010年24期

4 宋俊辉;谢华;;基于两方的电子合同签名协议模型研究[J];信息系统工程;2011年05期

相关博士学位论文 前3条

1 赵铭伟;电子商务系统中信息资源安全管理的若干技术问题研究[D];大连理工大学;2010年

2 范伟;移动商务安全性研究[D];北京邮电大学;2010年

3 徐伟峰;多主体模型定量验证方法研究[D];吉林大学;2014年

相关硕士学位论文 前1条

1 丁广泓;集成电路形式化验证的FPGA加速技术研究[D];广西民族大学;2015年

【二级参考文献】

相关期刊论文 前10条

1 仲红;黄刘生;罗永龙;;安全电子选举研究[J];安徽大学学报(自然科学版);2007年03期

2 秦志光;罗绪成;;P2P共享系统中无需专用TTP的公平交换协议[J];电子科技大学学报;2006年S1期

3 刘道斌,郭莉,白硕;基于Petri网的安全协议形式化分析[J];电子学报;2004年11期

4 王彩芬,贾爱库,刘军龙,于成尊;基于签密的多方认证邮件协议[J];电子学报;2005年11期

5 王彩芬;俞惠芳;王会歌;易玮;;一种新的多方多合同签署协议[J];电子学报;2007年10期

6 文静华;李祥;张焕国;梁敏;张梅;;基于ATL的公平电子商务协议形式化分析[J];电子与信息学报;2007年04期

7 周勇;朱梧i，

本文编号：2204061