Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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). In: IFIP International Conference on Theoretical Computer Science (IFIP TCS2000), Sendai, Japan. Springer, Berlin (2000)
Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library (2003)
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)
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)
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)
Brown, D.: Generic Groups, Collision Resistance, and ECDSA (2002) Available from, http://eprint.iacr.org/2002/026/
Coq Development Team. The Coq Proof Assistant User’s Guide. Version 8.0 (January 2004)
Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Transactions on Information Theory IT-22(6), 644–654 (1976)
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)
formalization of probability, http://www-sop.inria.fr/everest/personnel/Sabrina.Tarento/useful_files.html
Impagliazzo, R., Kapron, B.: Logics for reasoning about cryptographic constructions (2003)
Lang, S.: Algebra. Addison Wesley, Reading (1983)
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)
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)
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)
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)
Nechaev, V.I.: Complexity of a determinate algorithm for the discrete logarithm. Mathematical Notes 55(2), 165–172 (1994)
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)
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
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tarento, S. (2005). Machine-Checked Security Proofs of Cryptographic Signature Schemes. In: di Vimercati, S.d.C., Syverson, P., Gollmann, D. (eds) Computer Security – ESORICS 2005. ESORICS 2005. Lecture Notes in Computer Science, vol 3679. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11555827_9
Download citation
DOI: https://doi.org/10.1007/11555827_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28963-0
Online ISBN: 978-3-540-31981-8
eBook Packages: Computer ScienceComputer Science (R0)