基于ATL的公平电子商务协议形式化分析
doi: 10.3724/SP.J.1146.2005.01088
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协议进行了严格的形式化分析,结果发现该协议在非保密通道下存在两个可能的攻击:保密信息泄露和重放攻击。Abstract: Aiming at the shortcoming that traditional temporal logic such as LTL,CTL and CTL* regards protocols as close system to analyze, Dr Kremer(2003) proposes an ATL(Alternating-time Temporal Logic) logical method based on game to analyze fair E-commerce protocols, and analyses formally several typical protocols on their fairness and other properties. In this paper, ATL logical and its applications in formal analysis of E-commerce protocols are discussed, and Dr Kremer approach is ulteriorly extended to analyze security of protocols besides fairness. Finally, the strict formal analysis is made for ZDB protocol(1999) proposed by Zhou et al. With this new method, as a result there exists 2 possible attacks in the ZDB protocol under non-secrecy channels: leakiness of secret information and reply attacks.
-
[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