高级搜索

留言板

尊敬的读者、作者、审稿人, 关于本刊的投稿、审稿、编辑和出版的任何问题, 您可以本页添加留言。我们将尽快给您答复。谢谢您的支持!

姓名
邮箱
手机号码
标题
留言内容
验证码

基于ATL的公平电子商务协议形式化分析

文静华 李祥 张焕国 梁敏 张梅

文静华, 李祥, 张焕国, 梁敏, 张梅. 基于ATL的公平电子商务协议形式化分析[J]. 电子与信息学报, 2007, 29(4): 901-905. doi: 10.3724/SP.J.1146.2005.01088
引用本文: 文静华, 李祥, 张焕国, 梁敏, 张梅. 基于ATL的公平电子商务协议形式化分析[J]. 电子与信息学报, 2007, 29(4): 901-905. doi: 10.3724/SP.J.1146.2005.01088
Wen Jing-Hua, Li Xiang, Zhang Huan-guo, Liang Min, Zhang Mei. Formal Analysis of Fair E-Commerce Protocols Based on ATL[J]. Journal of Electronics & Information Technology, 2007, 29(4): 901-905. doi: 10.3724/SP.J.1146.2005.01088
Citation: Wen Jing-Hua, Li Xiang, Zhang Huan-guo, Liang Min, Zhang Mei. Formal Analysis of Fair E-Commerce Protocols Based on ATL[J]. Journal of Electronics & Information Technology, 2007, 29(4): 901-905. doi: 10.3724/SP.J.1146.2005.01088

基于ATL的公平电子商务协议形式化分析

doi: 10.3724/SP.J.1146.2005.01088
基金项目: 

国家自然科学基金(40261009)和贵州省科学技术基金(20052111)资助课题

Formal Analysis of Fair E-Commerce Protocols Based on ATL

  • 摘要: 针对传统时序逻辑LTL,CTL及CTL*等把协议看成封闭系统进行分析的缺点,Kremer博士(2003)提出用一种基于博弈的ATL(Alternating-time Temporal Logic)方法分析公平电子商务协议并对几个典型的协议进行了公平性等方面的形式化分析。本文讨论了ATL逻辑及其在电子商务协议形式化分析中的应用,进一步扩展了Kremer博士的方法,使之在考虑公平性等特性的同时能够分析协议的安全性。最后本文用新方法对Zhou等人(1999)提出的 ZDB协议进行了严格的形式化分析,结果发现该协议在非保密通道下存在两个可能的攻击:保密信息泄露和重放攻击。
  • [1] Asokan N. Fairness in electronic commerce. [PhD thesis], University of Waterloo, May 1998. [2] Clarke E M and Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logic of Programs, volume 131 of Lecture Notes in Computer Science, Springer- Verlag, 1981: 52-71. [3] Schneider S A. Formal analysis of a non- repudiation protocol. In 11th IEEE Computer Security Foundations Workshop, Massachusetts, USA, 1998: 54-65. [4] Emerson E A. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol B: Formal Models and Semantics, chapter 16. Elsevier Publishers B.V, 1990: 995-1072. [5] Alur R, Henzinger T A, and Kupferman O. Alternating-time temporal logic. In 38th Annual Symposium on Foundations of Computer Science, Miami Beach, IEEE Computer Society Press, 1997: 100-109. [6] Alur R.[J].Henzinger T A, Mang F, Qadeer S, Rajamani S, and Tasiran S. MOCHA: Modularity in model checking. In Proc. CAV 98, Vancouver, BC, Canada.1998,:- [7] Kremer S and Raskin J F. A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security, 2003, 11(3): 399-429. [8] Kremer S and Raskin J F. Game analysis of abuse-free contract signing. In Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW'02), Cape Breton, Nova Scotia, Canada, June 2002, IEEE Computer Society Press, 2002: 206-220. [9] Zhou J Y, Deng R H, and Bao F. Evolution of fair non-repudiation with TTP. In ACISP: Information security and privacy: Australasian Conference, volume 1587 of Lecture Notes in Computer Science, Springer-Verlag, 1999: 258-269. [10] Henzinger T.[J].Majumdar R, Mang F, and Raskin J F. Abstract interpretation of game properties. In Proc. SAS 00, Santa Barbara, USA.2000,:- [11] Mahimkar A and Shmatikov V. Game-based analysis of denial-of-service prevention protocols. in 18th IEEE Computer Security Foundations Workshop (CSFW), Aix-en-Provence, France June 2005: 151-166. [12] Schunter M. Optimistic fair exchange.[ PhD thesis], Technische Fakultat der Universit at des Saarlandes, Saarbrucken, October 2000. [13] Zhou J and Gollmann D. An efficient non-repudiation protocol. Proceedings of 10th IEEE Computer Security Foundations Workshop[C]. Rocport , Massachusetts : IEEE Computer Society Press, June 1997: 126-132. [14] Garay J A.[J].Jakobsson M, and MacKenzie P D. Abuse-free optimistic contract signing. In Advances in Cryptology Crypto 1999, 1666 of Lecture Notes in Computer Science, Springer-Verlag.1999,:-
  • 加载中
计量
  • 文章访问数:  3484
  • HTML全文浏览量:  96
  • PDF下载量:  1171
  • 被引次数: 0
出版历程
  • 收稿日期:  2005-08-30
  • 修回日期:  2006-01-11
  • 刊出日期:  2007-04-19

目录

    /

    返回文章
    返回