Abstract
Most approaches to the formal analyses of cryptographic protocols make the perfect cryptography assumption, i.e. the hypothese that there is no way to obtain knowledge about the plaintext pertaining to a ciphertext without knowing the key. Ideally, one would prefer to rely on a weaker hypothesis on the computational cost of gaining information about the plaintext pertaining to a ciphertext without knowing the key. Such a view is permitted by the Generic Model and the Random Oracle Model which provide non-standard computational models in which one may reason about the computational cost of breaking a cryptographic scheme. Using the proof assistant Coq, we provide a machine-checked account of the Generic Model and the Random Oracle Model.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Blanchet, B.: Secrecy types for asymmetric communication. Theoretical Computer Science 298(3), 387–415 (2003)
Abadi, M., Needham, R.M.: Prudent engineering practice for cryptographic protocols. Transactions on Software Engineering 22(1), 6–15 (1996)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology 15(2), 103–127 (2002)
Bailey, A.: Representing Algebra in LEGO. Master’s thesis, University of Edinburgh (1993)
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)
Bella, G., Massacci, F., Paulson, L.C.: Verifying the set registration protocols. IEEE Journal on Selected Areas in Communications 21, 77–87 (2003)
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, November 1993, pp. 62–73. ACM Press, New York (1993)
Bolignano, D.: Towards a mechanization of cryptographic protocol verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 131–142. Springer, Heidelberg (1997)
Brown, D.: Generic groups, collision resistance, and ecdsa (2002), Available from http://eprint.iacr.org/2002/026/
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Transactions on Computer Systems 8(1), 18–36 (1990)
Canetti, R., Goldreich, O., Halevi, S.: The random oracle methodology, revisited. In: Proceedings of STOC 1998, pp. 209–218. ACM Press, New York (1998)
Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: An NP Decision Procedure for Protocol Insecurity with XOR. In: Proceedings of LICS 2003, pp. 261–270. IEEE Computer Society Press, Los Alamitos (2003)
Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Proceedings of LICS 2003, pp. 271–280. IEEE Computer Society Press, Los Alamitos (2003)
Coq Development Team. The Coq Proof Assistant User’s Guide. Version 7.4 (February 2003)
Dent, A.W.: Adapting theWeaknesses of the Random Oracle Model to the Generic Group Model. In: Zheng, Y. (ed.) ASIACRYPT 2002. LNCS, vol. 2501, pp. 100–109. Springer, Heidelberg (2002)
Fiat, A., Shamir, A.: How to Prove Yourself: Practical Solutions to Identification and Signature Problems. In: Bouchon, B., Yager, R.R. (eds.) Uncertainty in Knowledge-Based Systems. LNCS, vol. 286, pp. 186–194. Springer, Heidelberg (1987)
Gordon, A., Jeffrey, A.: Authenticity by typing for security protocols. In: Proceedings of CSFW 2001, pp. 145–159. IEEE Computer Society Press, Los Alamitos (2001)
Harrison, J.: Theorem Proving with the Real Numbers. Distinguished Dissertations. Springer, Heidelberg (1998)
Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge (2002)
Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, Springer, Heidelberg (1996)
Meadows, C.: The nrl protocol analyzer: An overview. Journal of Logic Programming 26(2), 113–131 (1996)
Meadows, C.: Analysis of the internet key exchange protocol using the NRL protocol analyzer. In: Proceedings of SOSP 1999, pp. 216–233. IEEE Computer Society Press, Los Alamitos (1999)
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)
Nechaev, V.I.: Complexity of a determinate algorithm for the discrete logarithm. Mathematical Notes 55(2), 165–172 (1994)
Nedzusiak, A.: σ-fields and probability. Journal of Formalized Mathematics 1 (1989)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1/2), 85–128 (1998)
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)
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)
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)
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)
Stern, J.: Why provable security matters? In: Biham, E. (ed.) EUROCRYPT 2003. LNCS, vol. 2656, pp. 449–461. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barthe, G., Cederquist, J., Tarento, S. (2004). A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. In: Basin, D., Rusinowitch, M. (eds) Automated Reasoning. IJCAR 2004. Lecture Notes in Computer Science(), vol 3097. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25984-8_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-25984-8_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22345-0
Online ISBN: 978-3-540-25984-8
eBook Packages: Springer Book Archive