M. Abadi, Taming the Adversary, Proc. of Crypto'00, 2000.
DOI : 10.1007/3-540-44598-6_22

M. Abadi and A. Gordon, A calculus for cryptographic protocols, Proceedings of the 4th ACM conference on Computer and communications security , CCS '97, pp.36-47, 1997.
DOI : 10.1145/266420.266432

M. Abadi and P. Rogaway, Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)*, Journal of Cryptology, vol.15, issue.2, pp.103-127, 2002.
DOI : 10.1007/s00145-001-0014-7

M. Backes, B. Pfitzmann, and M. Waidner, A universally composable cryptographic library, Cryptology ePrint Archive Report, vol.015, 2003.

M. Bellare, A. Boldyreva, and S. Micali, Public-Key Encryption in a Multi-user Setting: Security Proofs and Improvements, Proc. of Eurocrypt'00, pp.259-274, 2000.
DOI : 10.1007/3-540-45539-6_18

L. Bozga, Y. Lakhnech, and M. Perin, HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols, 15th Int. Conference on Computer Aided Verification, pp.219-222, 2003.
DOI : 10.1007/978-3-540-45069-6_23

Y. Chevalier and L. Vigneron, A tool for lazy verification of security protocols, Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), 2001.
DOI : 10.1109/ASE.2001.989832
URL : https://hal.archives-ouvertes.fr/inria-00107545

V. Cortier, A guide for Securify, 2003.

S. Goldwasser, S. Micali, and R. Rivest, A Digital Signature Scheme Secure Against Adaptive Chosen-Message Attacks, SIAM Journal on Computing, vol.17, issue.2, pp.281-308, 1988.
DOI : 10.1137/0217017

P. Laud, Symmetric encryption in automatic analyses for confidentiality against active adversaries, Proc. of 2004 IEEE Symposium on Security and Privacy, pp.71-85, 2004.

G. Lowe, Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), pp.147-166, 1996.
DOI : 10.1007/3-540-61042-1_43

G. Lowe, Casper: A compiler for the analysis of security protocols, Proc. of 10th Computer Security Foundations Workshop (CSFW'97, 1997.

D. Micciancio and B. Warinschi, Soundness of Formal Encryption in the Presence of Active Adversaries, Theory of Cryptography Conference, pp.133-151, 2004.
DOI : 10.1007/978-3-540-24638-1_8

J. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague, A Probabilistic Polynomial-time Calculus For Analysis of Cryptographic Protocols, Electronic Notes in Theoretical Computer Science, vol.45, 2001.
DOI : 10.1016/S1571-0661(04)80968-X

L. Paulson, Mechanized proofs for a recursive authentication protocol, Proceedings 10th Computer Security Foundations Workshop, pp.84-95, 1997.
DOI : 10.1109/CSFW.1997.596790

C. Rackoff and D. Simon, Non-Interactive Zero-Knowledge Proof of Knowledge and Chosen Ciphertext Attack, CRYPTO'91, pp.433-444, 1992.
DOI : 10.1007/3-540-46766-1_35

M. Rusinowitch and M. Turuani, Protocol insecurity with finite number of sessions is NP-complete, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., pp.174-190, 2001.
DOI : 10.1109/CSFW.2001.930145
URL : https://hal.archives-ouvertes.fr/inria-00100411

S. Yamaguchi, K. Okayama, and H. Miyahara, The design and implementation of an authentication system for the wide area distributed environment, IEICE Transactions on Information and Systems, 1991.

L. Unité-de-recherche-inria-lorraine, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès-Nancy Cedex (France) Unité de recherche INRIA Futurs : Parc Club Orsay Université -ZAC des Vignes 4

I. Unité-de-recherche and . Rennes, IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l'Europe -38334 Montbonnot Saint-Ismier (France) Unité de recherche INRIA Rocquencourt : Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Unité de recherche, 2004.

I. De-voluceau-rocquencourt, BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399