Inductive methods and contract-signing protocols

ABSTRACT

Garay, Jakobsson and MacKenzie introduced the notion of abuse-free distributed contract-signing: at any stage of the protocol, no participant Ahas the ability to prove to an outside party, that A has the power to choose between completing the contract and aborting it. We study a version of this property, which is naturally formulated in terms of game strategies, and which we formally state and prove for a two-party, optimistic contract-signing protocol. We extend to this setting the formal inductive proof methods previously used in the formal analysis of simpler, trace-based properties of authentication protocols.

REFERENCES

• 1: N.Asokan,V.Shoup,and M.Waidner.Asynchronous protocols for optimistic fair exchange.In IEEE Symposium on Security and Privacy ,pages 86 -99, 1998.
• 2: I.Cervesato.Typed MSR:Syntax and examples.In WITS '00.Workshop on Issues in the Theory of Security,2000.,2000.
• 3: I. Cervesato , N. A. Durgin , P. D. Lincoln , J. C. Mitchell , A. Scedrov, A Meta-Notation for Protocol Analysis, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.55, June 28-30, 1999
• 4: Véronique Cortier , Jon Millen , Harald Rueβ, Proving Secrecy is Easy Enough, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, p.97, June 11-13, 2001
• 5: Satyaki Das , David L. Dill, Successive Approximation of Abstract Transition Relations, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.51, June 16-19, 2001
• 6: D.Dolev and A.Yao.On the security of public-key protocols.In Proc.22nd Annual IEEE Symp. Foundations of Computer Science ,pages 350 -357, 1981.
• 7: S.Even.Protocol for signing contracts.In CRYPTO , pages 148 -153,1981.
• 8: S.Even and Y.Yacobi.Tr 175.pages 148 -153, Computer Science Dept,Technion,Israel,March, 1980.
• 9: Michael J. Fischer , Nancy A. Lynch , Michael S. Paterson, Impossibility of distributed consensus with one faulty process, Journal of the ACM (JACM), v.32 n.2, p.374-382, April 1985 [doi>10.1145/3149.214121]
• 10: Juan A. Garay , Markus Jakobsson , Philip D. MacKenzie, Abuse-Free Optimistic Contract Signing, Proceedings of the 19th Annual International Cryptology Conference on Advances in Cryptology, p.449-466, August 15-19, 1999
• 11: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 12: M.Kanovich.Linear logic as a logic f computations. Annals of Pure and Applied Logic ,67:183 -212,1994.
• 13: Max I. Kanovich, The direct simulation of Minsky machines in linear logic, Proceedings of the workshop on Advances in linear logic, p.123-145, June 1995
• 14: S.Kremer and J.-F.Raskin.Formal veri .cation of non-repudiation protocols -a game approach.In Formal Methods for Computer Security (FMCS 2000), Chicago,USA,July 2000.
• 15: Vitaly Shmatikov , John C. Mitchell, Analysis of Abuse-Free Contract Signing, Proceedings of the 4th International Conference on Financial Cryptography, p.174-191, February 20-24, 2000
• 16: Roger M. Needham , Michael D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, v.21 n.12, p.993-999, Dec. 1978 [doi>10.1145/359657.359659]
• 17: Lawrence C Paulson, Proving Properties of Security Protocols by Induction, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.70, June 10-12, 1997
• 18: V.Shmatik v and J.C.Mitchell.Analysis of a fair exchange protocol.In FLoC Workshop on Formal Methods and Security Protocols ,1999.
• 19: P.Syverson,C.Meadows,and I.Cervesato.Dolev-ya is no better than machiavelli.In WITS '00.Workshop on Issues in the Theory of Security,2000.,2000.
• 20: V.Shmatik v and J.C.Mitchell.Finite-state analysis of tw contract signing protocols.In To appear in special issue of TCS on computer security ,2001.
• 21: Thomas Y. C. Woo , Simon S. Lam, A Semantic Model for Authentication Protocols, Proceedings of the 1993 IEEE Symposium on Security and Privacy, p.178, May 24-26, 1993

INDEX TERMS

Primary Classification:
  K. Computing Milieux
  K.4 COMPUTERS AND SOCIETY
      K.4.4 Electronic Commerce
          Subjects: Security

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Authentication

  K. Computing Milieux
  K.4 COMPUTERS AND SOCIETY
      K.4.4 Electronic Commerce
          Subjects: Electronic data interchange (EDI)

General Terms:
Algorithms, Performance, Security