Abstract
In this paper, we extend previous results relating the Dolev-Yao model and the computational model. We add the possibility to exchange keys and consider cryptographic primitives such as signature. This work can be applied to check protocols in the computational model by using automatic verification tools in the formal model.
To obtain this result, we introduce a precise definition for security criteria which leads to a nice reduction theorem. The reduction theorem is of interest on its own as it seems to be a powerful tool for proving equivalences between security criteria. Also, the proof of this theorem uses original ideas that seem to be applicable in other situations.
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Jürgens, J.: Formal eavesdropping and its computational interpretation. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, p. 82. Springer, Heidelberg (2001)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). In: IFIP International Conference on Theoretical Computer Science (IFIP TCS 2000). Springer, Berlin (2000)
Bellare, M., Kilian, J., Rogaway, P.: The security of cipher block chaining. In: Desmedt, Y.G. (ed.) CRYPTO 1994. LNCS, vol. 839, pp. 341–358. Springer, Heidelberg (1994)
Blanchet, B.: Abstracting cryptographic protocols by prolog rules. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, p. 433. Springer, Heidelberg (2001)
Boldyreva, A., Bellare, M., Micali, S.: Public-key encryption in a multi-user setting: Security proofs and improvements. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 259–274. Springer, Heidelberg (2000)
Bozga, L., Lakhnech, Y., Périn, M.: Hermes: An automatic tool for verification of secrecy in security protocols. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 219–222. Springer, Heidelberg (2003)
Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. Research Report RR-5341, INRIA (October 2004)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences 28(2), 270–299 (1984)
Goldwasser, S., Micali, S., Rivest, R.L.: A digital signature scheme secure against adaptive chosen-message attacks. SIAM Journal on Computing 17(2), 281–308 (1988)
Goubault-Larrecq, J.: A method for automatic cryptographic protocol verification. In: Rolim, J.D.P. (ed.) IPDPS-WS 2000. LNCS, vol. 1800, p. 977. Springer, Heidelberg (2000)
Laud, P.: Symmetric encryption in automatic analyses for confidentiality against adaptive adversaries. In: Proc. of 2004 IEEE Symposium on Security and Privacy, pp. 71–85 (2004)
Lowe, G.: An attack on the Needham-Schroeder public-key authentification protocol. Information Processing Letters 56(3), 131–133 (1995)
Pfitzmann, B., Backes, M., Waidner, M.: U universally composable cryptographic library. In: ACM Press (ed.) Computer and Communication Security (October 2003)
Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Proceedings of the Theory of Cryptography Conference, pp. 133–151. Springer, Heidelberg (2004)
Lakhnech, Y., Janvier, R., Mazaré, L.: (de)compositions of cryptographic schemes and their applications to protocols. Technical report, Verimag, Centre Équation, 38610 Gières (2004) (to appear)
Lakhnech, Y., Janvier, M.R., et al.: Completing the picture: Soundness of formal encryption in the presence of active adversaries. Technical Report TR-2004-19, Verimag, Centre Équation, 38610 Gières (November 2004)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: IEEE Computer Security Foundations Workshop (2001)
Warinschi, B.: A computational analysis of the needham-schroeder(-lowe) protocol. In: Proceedings of 16th Computer Science Foundation Workshop, pp. 248–262. ACM Press, New York (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
Janvier, R., Lakhnech, Y., Mazaré, L. (2005). Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries. In: Sagiv, M. (eds) Programming Languages and Systems. ESOP 2005. Lecture Notes in Computer Science, vol 3444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31987-0_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-31987-0_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25435-5
Online ISBN: 978-3-540-31987-0
eBook Packages: Computer ScienceComputer Science (R0)