R. Amadio and D. Lugiez, On the Reachability Problem in Cryptographic Protocols, Proceedings of CONCUR'00, 2000.
DOI : 10.1007/3-540-44618-4_28
URL : https://hal.archives-ouvertes.fr/inria-00072738

A. Armando and L. Compagna, Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning, Foundation of Computer Security & Verification Workshops, 2002.
DOI : 10.1007/3-540-36135-9_14

F. Baader and K. Schulz, Unification in the union of disjoint equational theories: Combining decision procedures, Proceedings of the 11th International Conference on Automated Deduction, pp.50-65, 1992.

D. Basin, S. Mödersheim, and L. Viganò, An On-the-Fly Model-Checker for Security Protocol Analysis, Proceedings of ESORICS'03, p.253, 2003.
DOI : 10.1007/978-3-540-39650-5_15

M. Boreale, Symbolic Trace Analysis of Cryptographic Protocols, Proceedings of the 28th International Conference on Automata, Language and Programming: ICALP'01, pp.667-681, 2001.
DOI : 10.1007/3-540-48224-5_55

M. Boreale and M. G. Buscemi, Symbolic Analysis of Crypto-Protocols Based on Modular Exponentiation, Proceedings of the Mathematical Foundations of Computer Science 2003, 28th International Symposium, 2003.
DOI : 10.1007/978-3-540-45138-9_21

N. Borisov, I. Goldberg, and D. Wagner, Intercepting mobile communications, Proceedings of the 7th annual international conference on Mobile computing and networking , MobiCom '01, pp.180-189, 2001.
DOI : 10.1145/381677.381695

Y. Chevalier, Résolution deprobì emes d'accessibilité pour la compilation et la validation de protocoles cryptographiques, 2003.

Y. Chevalier, R. Kuesters, M. Rusinowitch, and M. Turuani, An NP decision procedure for protocol insecurity with XOR, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., 2003.
DOI : 10.1109/LICS.2003.1210066
URL : https://hal.archives-ouvertes.fr/inria-00071889

Y. Chevalier, R. Küsters, M. Rusinowitch, and M. Turuani, Deciding the Security of Protocols with Diffie-Hellman Exponentiation and Products in Exponents, Proceedings of the Foundations of Software Technology and Theoretical Computer Science, FSTTCS'03 Long version available as Christian-Albrecht Universität IFI-Report 0305, 2003.
DOI : 10.1007/978-3-540-24597-1_11
URL : https://hal.archives-ouvertes.fr/inria-00103935

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

Y. Chevalier and L. Vigneron, Automated Unbounded Verification of Security Protocols, 14th International Conference on Computer Aided Verification, pp.324-337, 2002.
DOI : 10.1007/3-540-45657-0_24
URL : https://hal.archives-ouvertes.fr/inria-00100916

J. Clark and J. Jacob, A survey of authentication protocol literature: Version 1.0. Available via http, 1997.

H. Comon-lundh and V. Shmatikov, Intruder deductions, constraint solving and insecurity decision in presence of exclusive or, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.271-280, 2003.
DOI : 10.1109/LICS.2003.1210067

G. Denker, J. Millen, and H. Rueß, CAPSL integrated protocol environment, Proceedings DARPA Information Survivability Conference and Exposition. DISCEX'00, 2000.
DOI : 10.1109/DISCEX.2000.824980
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.1442

N. Dershowitz and J. Jouannaud, Rewrite Systems, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), pp.243-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

M. Fiore and M. Abadi, Computing symbolic models for verifying cryptographic protocols, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., 2001.
DOI : 10.1109/CSFW.2001.930144

P. Narendran, G. Guo, and D. A. Wolfram, Unification and matching modulo nilpotence, Information and Computation, issue.12, pp.1623-1646, 2000.

P. Ganty and G. Delzanno, Automatic verification of time sensitive cryptographic protocols, TACAS, pp.342-356, 2004.

J. Goubault-larrecq, A method for automatic cryptographic protocol verification Fifth International Workshop on Formal Methods for Parallel Programming: Theory and Applications, number 1800 in Lecture Notes in Computer Science, 2000.

Y. Lakhnech, L. Bozga, and M. Perin, Hermes: An automatic tool for the verification of secrecy in security protocols, Proceedings of the Computer-Aided Verification Conference CAV'03, pp.219-222, 2003.

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

C. Meadows, The NRL Protocol Analyzer: An Overview, The Journal of Logic Programming, vol.26, issue.2, pp.113-131, 1996.
DOI : 10.1016/0743-1066(95)00095-X

J. K. Millen and V. Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, Proceedings of the 8th ACM conference on Computer and Communications Security , CCS '01, pp.166-175, 2001.
DOI : 10.1145/501983.502007

J. C. Mitchell, V. Shmatikov, and U. Stern, Finite-state analysis of ssl 3.0, Seventh USENIX Security Symposium, pp.201-216, 1998.

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

S. E. and R. Corin, An Improved Constraint-Based System for the Verification of Security Protocols, SAS, pp.326-341, 2002.
DOI : 10.1007/3-540-45789-5_24

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

P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe, The Modelling and Analysis of Security Protocols, 2000.

P. Y. Ryan and S. A. Schneider, An attack on a recursive authentication protocol, Information Processing Letters, vol.65, 1998.

V. Shmatikov, Decidable Analysis of Cryptographic Protocols with Products and Modular Exponentiation, Proceedings of thirteenth European Symposium on Programming ESOP'04, pp.355-369, 2004.
DOI : 10.1007/978-3-540-24725-8_25

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.