微信服务号

微信订阅号

2025-4-6- 3
Home > Archive>Volume 22, Issue 3, 2011 >509-521. DOI:10.3724/SP.J.1001.2011.03945
PDF HTML XML Export Cite reminder
Formal Logic for Fair Exchange Protocols
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [26]
    • |
  • Related
    • |
  • Cited by [1]
    • | |
  • Comments
    Abstract:

    The fairness and punctuality of optimistic fair exchange protocols are difficult to analyze by using belief logic. Based on the studies of existing formal models and security attributes in fair exchange, a formal model for logic reasoning and fair exchange protocols is proposed. In the model, the channel errors are transferred to the attacker’s behaviors, the participants are divided into honest and dishonest ones, and the threats are attributed to two types of intruders. Based on the idea of model checking, the protocols are defined as an evolved system that has the Kripke structure, and the parties are considered as processes in an asynchronous environment. The new logic stimulates the time operators to control the transfers among the participants’ behaviors and is simple and easy to use. Through typical optimistic fair exchange protocols, the article demonstrates the course of protocol analysis. Two flaws of the protocol are discovered and improved. The case study shows that the new logic can be used to analyze the fairness and timeliness of fair exchange protocols.

    Reference
    [1] Asokan N. Fairness in electronic commerce [Ph.D. Thesis]. Waterloo: University of Waterloo, 1998.
    [2] Asokan N, Shoup V, Waidner M. Asynchronous protocols for optimistic fair exchange. In: Proc. of the IEEE Symp. on Research in Security and Privacy. Oakland: IEEE Computer Society Press, 1998. 86?99.
    [3] Bao F, Deng RH, Mao W. Efficient and practical fair exchange protocols with off-line TTP. In: Proc. of the IEEE Symp. on Security and Privacy. Oakland: IEEE Computer Society, 1998. 77?85. [doi: 10.1109/SECPRI.1998.674825]
    [4] Ray I, Ray I, Natarajan N. An anonymous and failure resilient fair-exchange e-commerce protocol. Decision Support Systems, 2005, 39(3):267?292. [doi: 10.1016/j.dss.2003.10.011]
    [5] Pagnia H, Vogt H, G?rtner FC. Fair exchange. The Computer Journal, 2003,46(1):55?76. [doi: 10.1093/comjnl/46.1.55]
    [6] Wang H, Guo H, Lin M, Yin J, He Q, Zhang J. A new dependable exchange protocol. Computer Communications, 2006,29(10): 2770?2780. [doi: 10.1016/j.comcom.2005.10.028]
    [7] Hernandez-Ardieta JL, Gonzalez-Tablas AI, Alvarez BR. An optimistic fair exchange protocol based on signature policies. Computers & Security, 2008,27(10):309?322. [doi: 10.1016/j.cose.2008.07.005]
    [8] Kremer S, Markowitch O. Optimistic non-repudiable information exchange. In: Biemond J, ed. Proc. of the 21st Symp. on Information Theory in the Benelux. Wassenaar: Werkgemeenschap Informatie-en Communicatietheorie, 2000. 139?146.
    [9] Zhou J, Gollmann D. An efficient non-repudiation protocol. In: Proc. of the 10th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, 1997. 126?132. [doi: 10.1109/CSFW.1997.596801].
    [10] Kailar R. Accountability in electronic commerce protocols. IEEE Trans. on Software Engineering, 1996,22(5):313?328. [doi: 10.1109/32.502224]
    [11] Burrows M, Abadi M, Needham R. A logic of authentication. ACM Trans. on Computer Systems, 1990,8(1):18?36. [doi: 10.1145/77648.77649]
    [12] Zhou J, Gollmann D. Towards verification of non-repudiation protocols. In: Proc. of the Int’l Refinement Workshop and Formal Methods Pacific. Canberra: Springer-Verlag, 1998. 370?380.
    [13] Syverson PF, Van Oorschot PC. A unified cryptographic protocol logic. NRL Publication 5540-227. Washington: Naval Research Laboratory, 1996.
    [14] Schneider S. Formal analysis of a non-repudiation protocol. In: Proc. of the 11th IEEE Computer Security Foundations Workshop. Washington-Brussels-Tokyo: IEEE Computer Security Press, 1998. 54?65. [doi: 10.1109/CSFW.1998.683155]
    [15] Bella G, Paulson LC. Accountability protocols: Formalized and verified. ACM Trans. on Information System Security, 2006,9(2): 138?161. [doi: 10.1145/1151414.1151416]
    [16] Zhou J, Gollmann D. A fair non-repudiation protocol. In: Proc. of the IEEE Symp. on Research in Security and Privacy, Research in Security and Privacy. IEEE Computer Security Press, 1996. 55?61. [doi: 10.1109/SECPRI.1996.502669]
    [17] Shmatikov V, Mitchell JC. Finite-State analysis of two contract signing protocols. Theoretical Computer Science, 2002,283(2): 419?450. [doi: 10.1016/S0304-3975(01)00141-4]
    [18] Garay JA, Jakobsson M, MacKenzie P. Abuse-Free optimistic contract signing. In: Proc. of the Advance in Cryptology-Crypto’99. LNCS 1666, Berlin, Heidelberg: Springer-Verlag, 1999. 449?466.
    [19] Kremer S, Raskin J. A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security, 2003, 11(3):399?429.
    [20] Dashti MT. Keeping fairness alive [Ph.D. Thesis]. Geboren te Kordkoy: Vrije Universiteit Amsterdam, 2008.
    [21] Qing SH, Li GC. A formal model of fair exchange protocols. Science in China Ser. F: Information Sciences, 2005,48(4):499?512.
    [22] Dolev D, Yao AC. On the security of public key protocols. IEEE Trans. on Information Theory, 1983,29(2):198?208. [doi: 10.1109/TIT.1983.1056650]
    [23] Li BT, Luo JZ. Formal analysis of timeliness in non-repudiation protocols. Journal of Software, 2006,17(7):1510?1516 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/17/1510.htm [doi: 10.1360/jos171510]
    [24] Qing SH. TTP roles in electronic commerce protocols. Journal of Software, 2003,14(11):1936?1943 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/14/1936.htm
    [25] Pagnia H, G?rtner F. On the impossibility of fair exchange without a trusted third party. Technical Report, TUD-BS-1999-02, Darmstadt: Darmstadt University of Technology, 1999.
    [26] Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Proving security protocols correct. Journal of Computer Security, 1999,7(2-3): 191?230.
    Related
    Comments
    Comments
    分享到微博
    Submit
Get Citation

陈明,吴开贵,吴长泽,徐洁,吴中福.公平交换协议形式逻辑.软件学报,2011,22(3):509-521

Copy
Share
Article Metrics
  • Abstract:5225
  • PDF: 7336
  • HTML: 0
  • Cited by: 0
History
  • Received:November 05,2009
  • Revised:September 06,2010
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2033284Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063