Machine-Checked Security Proofs of Cryptographic Signature Schemes

  • Sabrina Tarento
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3679)


Formal methods have been extensively applied to the certification of cryptographic protocols. However, most of these works make the perfect cryptography assumption, i.e. the hypothesis that there is no way to obtain knowledge about the plaintext pertaining to a ciphertext without knowing the key. A model that does not require the perfect cryptography assumption is the generic model and the random oracle model. These models provide non-standard computational models in which one may reason about the computational cost of breaking a cryptographic scheme. Using the machine-checked account of the Generic Model and the Random Oracle Model formalized in Coq, we prove the safety of cryptosystems that depend on a cyclic group (like ElGamal cryptosystem), against interactive generic attacks and we prove the security of blind signatures against interactive attacks. To prove the last step, we use a generic parallel attack to create a forgery signature.


Hash Function Blind Signature Cryptographic Protocol Valid Signature Proof Assistant 
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. 1.
    Abadi, M., Needham, R.M.: Prudent engineering practice for cryptographic protocols. Transactions on Software Engineering 22(1), 6–15 (1996)CrossRefGoogle Scholar
  2. 2.
    Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). In: IFIP International Conference on Theoretical Computer Science (IFIP TCS2000), Sendai, Japan. Springer, Berlin (2000)Google Scholar
  3. 3.
    Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library (2003)Google Scholar
  4. 4.
    Barendregt, H., Geuvers, H.: Proof assistants using dependent type systems. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 18, vol. II, pp. 1149–1238. Elsevier Publishing, Amsterdam (2001)CrossRefGoogle Scholar
  5. 5.
    Barthe, G., Cederquist, J., Tarento, S.: A machine-checked formalization of the generic model and the random oracle model. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 385–399. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    Bellare, M., Rogaway, P.: Random oracles are practical: A paradigm for designing efficient protocols. In: Proceedings of the 1st ACM Conference on Computer and Communications Security, pp. 62–73. ACM Press, New York (1993)CrossRefGoogle Scholar
  7. 7.
    Brown, D.: Generic Groups, Collision Resistance, and ECDSA (2002) Available from,
  8. 8.
    Coq Development Team. The Coq Proof Assistant User’s Guide. Version 8.0 (January 2004)Google Scholar
  9. 9.
    Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Transactions on Information Theory IT-22(6), 644–654 (1976)Google Scholar
  10. 10.
    Fiat, A., Shamir, A.: How to Prove Yourself: Practical Solutions to Identification and Signature Problems. In: Proc. CRYPTO 1986. LNCS, vol. 286, pp. 186–194. Springer, Heidelberg (1986)Google Scholar
  11. 11.
  12. 12.
    Impagliazzo, R., Kapron, B.: Logics for reasoning about cryptographic constructions (2003)Google Scholar
  13. 13.
    Lang, S.: Algebra. Addison Wesley, Reading (1983)Google Scholar
  14. 14.
    Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: Probabilistic polynomial-time equivalence and security analysis. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 776–793. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  15. 15.
    Meadows, C.: Open issues in formal methods for cryptographic protocol analysis. In: Gorodetski, V.I., Skormin, V.A., Popyack, L.J. (eds.) MMM-ACNS 2001. LNCS, vol. 2052, p. 21. Springer, Heidelberg (2001)Google Scholar
  16. 16.
    Mitchell, J., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time calculus for analysis of cryptographic protocols (preliminary report). In: Brookes, S., Mislove, M. (eds.) 17-th Annual Conference on the Mathematical Foundations of Programming Semantics, Aarhus, Denmark, vol. 45 (2001)Google Scholar
  17. 17.
    Mitchell, J.C., Mitchell, M., Scedrov, A.: A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In: IEEE Symposium on Foundations of Computer Science, pp. 725–733 (1998)Google Scholar
  18. 18.
    Nechaev, V.I.: Complexity of a determinate algorithm for the discrete logarithm. Mathematical Notes 55(2), 165–172 (1994)CrossRefMathSciNetGoogle Scholar
  19. 19.
    Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: Proceedings of SOSP 2001, pp. 184–201. IEEE Press, Los Alamitos (2001)Google Scholar
  20. 20.
    Schnorr, C.-P.: Security of blind discrete log signatures against interactive attacks. In: Qing, S., Okamoto, T., Zhou, J. (eds.) ICICS 2001. LNCS, vol. 2229, pp. 1–12. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  21. 21.
    Schnorr, C.-P., Jakobsson, M.: Security of signed elGamal encryption. In: Okamoto, T. (ed.) ASIACRYPT 2000. LNCS, vol. 1976, pp. 73–89. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  22. 22.
    Shoup, V.: Lower bounds for discrete logarithms and related problems. In: Fumy, W. (ed.) EUROCRYPT 1997. LNCS, vol. 1233, pp. 256–266. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  23. 23.
    Smart, N.: The Exact Security of ECIES in the Generic Group Model. In: Honary, B. (ed.) Cryptography and Coding, pp. 73–84. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  24. 24.
    Stern, J.: Why provable security matters? In: Biham, E. (ed.) EUROCRYPT 2003. LNCS, vol. 2656, pp. 449–461. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Sabrina Tarento
    • 1
  1. 1.INRIA Sophia-AntipolisFrance

Personalised recommendations