Skip to main content
SpringerLink
Log in

A Machine-Checked Formalization of the Random Oracle Model

  • Conference paper
Types for Proofs and Programs (TYPES 2004)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3839))

Included in the following conference series:

Abstract

Most approaches to the formal analysis of cryptography protocols make the perfect cryptographic assumption, which entails for example that there is no way to obtain knowledge about the plaintext pertaining to a ciphertext without knowing the key. Ideally, one would prefer to abandon the perfect cryptography hypothesis and reason about the computational cost of breaking a cryptographic scheme by achieving such goals as gaining information about the plaintext pertaining to a ciphertext without knowing the key. Such a view is permitted by non-standard computational models such as the Generic Model and the Random Oracle Model. Using the proof assistant Coq, we provide a machine-checked account of the Generic Model and the Random Oracle Model. We exploit this framework to prove the security of the ElGamal cryptosystem against adaptive chosen ciphertexts attacks.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Needham, R.M.: Prudent engineering practice for cryptographic protocols. Transactions on Software Engineering 22(1), 6–15 (1996)

    Article  Google Scholar 

  2. Barendregt, H., Geuvers, H.: Proof assistants using dependent type systems. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, ch. 18, pp. 1149–1238. Elsevier Publishing, Amsterdam (2001)

    Chapter  Google Scholar 

  3. Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. Journal of Functional Programming 13, 261–293 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. Brown, D.: Generic Groups, Collision Resistance, and ECDSA (2002), Available from: http://eprint.iacr.org/2002/026/

  7. Coq Development Team. The Coq Proof Assistant User’s Guide. Version 8.0 (January 2004)

    Google Scholar 

  8. Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Transactions on Information Theory IT-22(6), 644–654 (1976)

    Article  MathSciNet  Google Scholar 

  9. Fiat, A., Shamir, A.: How to Prove Yourself: Practical Solutions to Identification and Signature Problems. In: Odlyzko, A.M. (ed.) CRYPTO 1986. LNCS, vol. 263, pp. 186–194. Springer, Heidelberg (1987)

    Google Scholar 

  10. El Gamal, T.: A public key cryptosystem and a signature scheme based on discrete logarithms. In: Blakely, G.R., Chaum, D. (eds.) CRYPTO 1984. LNCS, vol. 196, pp. 10–18. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

  11. Nechaev, V.I.: Complexity of a determinate algorithm for the discrete logarithm. Mathematical Notes 55(2), 165–172 (1994)

    Article  MathSciNet  Google Scholar 

  12. Rackoff, C., Simon, D.R.: Non-interactive zero-knowledge proof of knowledge and chosen ciphertext attack. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 433–444. Springer, Heidelberg (1992)

    Google Scholar 

  13. Schneier, B.: Applied Cryptography, 2nd edn. John Wiley & Sons, Chichester (1996)

    Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. 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)

    Google Scholar 

  17. Smart, N.: The Exact Security of ECIES in the Generic Group Model. In: Honary, B. (ed.) Cryptography and Coding 2001. LNCS, vol. 2260, pp. 73–84. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  18. Stern, J.: Why provable security matters? In: Biham, E. (ed.) EUROCRYPT 2003. LNCS, vol. 2656, pp. 449–461. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  19. Tarento, S.: Machine-checked security proofs of cryptographic signature schemes. In: di Vimercati, S.d.C., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 140–158. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Sophia-Antipolis, France

    Gilles Barthe & Sabrina Tarento

Authors
  1. Gilles Barthe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sabrina Tarento
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LRI, Univ Paris-Sud, CNRS, Orsay F-91405, INRIA Futurs, ProVal, F-91893, Orsay

    Jean-Christophe Filliâtre

  2. INRIA Saclay - Île-de-France, ProVal - Orsay 91893 and LRI, Univ Paris-Sud, CNRS - Orsay 91405LRI, Université Paris Sud and INRIA Futurs, Bât. 490, Université Paris Sud, F-91405, Orsay Cedex, France

    Christine Paulin-Mohring

  3. INRIA-Futurs at, LIX, École Polytechnique, Palaiseau, France

    Benjamin Werner

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barthe, G., Tarento, S. (2006). A Machine-Checked Formalization of the Random Oracle Model. In: Filliâtre, JC., Paulin-Mohring, C., Werner, B. (eds) Types for Proofs and Programs. TYPES 2004. Lecture Notes in Computer Science, vol 3839. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11617990_3

Download citation

  • DOI: https://doi.org/10.1007/11617990_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-31428-8

  • Online ISBN: 978-3-540-31429-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation