Computationally Sound Analysis of a Probabilistic Contract Signing Protocol

  • Mihhail Aizatulin
  • Henning Schnoor
  • Thomas Wilke
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5789)


We propose a probabilistic contract signing protocol that achieves balance even in the presence of an adversary that may delay messages sent over secure channels. To show that this property holds in a computational setting, we first propose a probabilistic framework for protocol analysis, then prove that in a symbolic setting the protocol satisfies a probabilistic alternating-time temporal formula expressing balance, and finally establish a general result stating that the validity of formulas such as our balance formula is preserved when passing from the symbolic to a computational setting. The key idea of the protocol is to take a “gradual commitment” approach.


Successor State Security Property Trusted Third Party Propositional Variable State Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [AHK02]
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49(5), 672–713 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  2. [AR02]
    Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology 15(2), 103–127 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  3. [ASW98]
    Asokan, N., Shoup, V., Waidner, M.: Asynchronous protocols for optimistic fair exchange. In: Proceedings of the IEEE Symposium on Research in Security and Privacy, pp. 86–99. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  4. [ASW09]
    Aizatulin, M., Schnoor, H., Wilke, T.: Computationally sound analysis of a probabilistic contract signing protocol. Technical Report 0911, Institut für Informatik, Christian-Albrechts-Universität zu Kiel (2009)Google Scholar
  5. [BDD+06]
    Backes, M., Datta, A., Derek, A., Mitchell, J.C., Turuani, M.: Compositional analysis of contract-signing protocols. Theoretical Computer Science 367(1-2), 33–56 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  6. [BL69]
    Buchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society 138, 295–311 (1969)MathSciNetCrossRefzbMATHGoogle Scholar
  7. [BOGMR90]
    Ben-Or, M., Goldreich, O., Micali, S., Rivest, R.L.: Fair protocol for signing contracts. IEEE Transactions on Information Theory 36(1), 40–46 (1990)MathSciNetCrossRefGoogle Scholar
  8. [BR93]
    Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 232–249. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  9. [CH06]
    Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key-exchange protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 380–403. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. [CKKW06]
    Cortier, V., Kremer, S., Küsters, R., Warinschi, B.: Computationally sound symbolic secrecy in the presence of hash functions. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 176–187. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. [CKS01]
    Chadha, R., Kanovich, M.I., Scedrov, A.: Inductive methods and contract-signing protocols. In: ACM Conference on Computer and Communications Security, pp. 176–185 (2001)Google Scholar
  12. [CKW07]
    Cortier, V., Küsters, R., Warinschi, B.: A cryptographic model for branching time security properties - the case of contract signing protocols. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 422–437. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. [CL07]
    Chen, T., Lu, J.: Probabilistic alternating-time temporal logic and model checking algorithm. In: Lei, J. (ed.) FSKD (2), pp. 35–39. IEEE Computer Society Press, Los Alamitos (2007)Google Scholar
  14. [CMSS05]
    Chadha, R., Mitchell, J.C., Scedrov, A., Shmatikov, V.: Contract signing, optimism, and advantage. Journal of Logic and Algebraic Programming 64(2), 189–218 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  15. [DY83]
    Dolev, D., Yao, A.C.-C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–207 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  16. [GJM99]
    Garay, J.A., Jakobsson, M., MacKenzie, P.D.: Abuse-free optimistic contract signing. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 449–466. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  17. [KKT07]
    Kähler, D., Küsters, R., Truderung, T.: Infinite state AMC-model checking for cryptographic protocols. In: LICS, pp. 181–192. IEEE Computer Society Press, Los Alamitos (2007)Google Scholar
  18. [KKW05]
    Kähler, D., Küsters, R., Wilke, T.: Deciding properties of contract-signing protocols. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, pp. 158–169. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  19. [KR02]
    Kremer, S., Raskin, J.-F.: Game analysis of abuse-free contract signing. In: CSFW. IEEE Computer Society Press, Los Alamitos (2002)Google Scholar
  20. [KR03]
    Kremer, S., Raskin, J.-F.: A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security 11(3), 399–430 (2003)CrossRefGoogle Scholar
  21. [Kuh53]
    Kuhn, H.W.: Extensive games and the problem of information. Annals of Mathematics Studies 28, 193–216 (1953)MathSciNetzbMATHGoogle Scholar
  22. [LM05]
    Lakhnech, Y., Mazaré, L.: Computationally sound verification of security protocols using Diffie-Hellman exponentiation. Technical report, Verimag (2005)Google Scholar
  23. [PG99]
    Pagnia, H., Gartner, F.C.: On the impossibility of fair exchange without a trusted third party. Technical report, Darmstadt University of Technology (1999)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Mihhail Aizatulin
    • 1
  • Henning Schnoor
    • 1
  • Thomas Wilke
    • 1
  1. 1.Institut für InformatikChristian-Albrechts-Universität zu KielKielGermany

Personalised recommendations