M. Abadi, B. Blanchet, and C. Fournet, Just Fast Keying in the Pi Calculus, Proceedings of ESOP'04, pp.340-354, 2004.
DOI : 10.1007/978-3-540-24725-8_24

M. Abadi and C. Fournet, Mobile values, new names, and secure communication, POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp.104-115, 2001.
DOI : 10.1145/360204.360213
URL : https://hal.archives-ouvertes.fr/hal-01423924

R. Amadio, D. Lugiez, and V. Vanackère, On the symbolic reduction of processes with cryptographic functions, Theoretical Computer Science, vol.290, issue.1, pp.695-740, 2003.
DOI : 10.1016/S0304-3975(02)00090-7
URL : https://hal.archives-ouvertes.fr/inria-00072478

F. Baader and K. U. Schulz, Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures, Journal of Symbolic Computation, vol.21, issue.2, pp.211-243, 1996.
DOI : 10.1006/jsco.1996.0009

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

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

M. Boreale and M. Buscemi, Symbolic Analysis of Crypto-Protocols Based on Modular Exponentiation, Proceedings of MFCS 2003, 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. 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 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

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

H. Comon-lundh, Intruder Theories (Ongoing Work), 7th International Conference, pp.1-4, 2004.
DOI : 10.1007/978-3-540-24727-2_1

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

H. Comon-lundh and R. Treinen, Easy Intruder Deductions, Lecture Notes in Computer Science, vol.2772, pp.225-242, 2003.
DOI : 10.1007/978-3-540-39910-0_10

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

V. Cortier, S. Delaune, and P. Lafourcade, A survey of algebraic properties used in cryptographic protocols, Journal of Computer Security, vol.14, issue.1, 2004.
DOI : 10.3233/JCS-2006-14101
URL : https://hal.archives-ouvertes.fr/inria-00000552

S. Delaune and F. Jacquemard, A decision procedure for the verification of security protocols with explicit destructors, Proceedings of the 11th ACM conference on Computer and communications security , CCS '04, pp.278-287, 2004.
DOI : 10.1145/1030083.1030121
URL : https://hal.archives-ouvertes.fr/inria-00579012

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

D. Dolev and A. Yao, On the Security of Public-Key Protocols, IEEE Transactions on Information Theory, vol.2, issue.29, 1983.

G. Guo, P. Narendran, and D. A. Wolfram, Unification and matching modulo nilpotence, Information and Computation, issue.12, pp.1623-1646, 2000.
DOI : 10.1007/3-540-61511-3_90

R. Küsters and T. Wilke, Automata-Based Analysis of Recursive Cryptographic Protocols, 21st Symposium on Theoretical Aspects of Computer Science Lecture Notes in Computer Science, pp.382-393, 2004.
DOI : 10.1007/978-3-540-24749-4_34

C. Meadows and P. Narendran, A unification algorithm for the group Diffie-Hellman protocol, Workshop on Issues in the Theory of Security (in conjunction with POPL'02), 2002.

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
URL : http://doi.org/10.1016/0743-1066(95)00095-x

J. Millen, On the freedom of decryption, Information Processing Letters, vol.86, issue.6, pp.329-333, 2003.
DOI : 10.1016/S0020-0190(03)00211-4

J. 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. Millen and V. Shmatikov, Symbolic protocol analysis with an abelian group operator or Diffie-Hellman exponentiation, Journal of Computer Security, 2005.

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

M. Schmidt-schauß, Unification in a combination of arbitrary disjoint equational theories, Journal of Symbolic Computation, vol.8, issue.1-2, pp.51-99, 1989.
DOI : 10.1016/S0747-7171(89)80022-7

V. Shmatikov, Decidable Analysis of Cryptographic Protocols with Products and Modular Exponentiation, Proceedings of 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.