D. Basin, S. Mödersheim, and L. Viganò, Algebraic Intruder Deductions, Logic for Programming, Articial Intelligence, and Reasoning (LPAR), pp.549-564, 2005.
DOI : 10.1007/11591191_38

D. Basin, S. Mödersheim, and L. Viganò, OFMC: A symbolic model checker for security protocols, International Journal of Information Security, vol.7, issue.3, pp.181-208, 2005.
DOI : 10.1007/s10207-004-0055-7

M. Baudet, Deciding security of protocols against off-line guessing attacks, Proceedings of the 12th ACM conference on Computer and communications security , CCS '05, p.1625, 2005.
DOI : 10.1145/1102120.1102125

S. Bursuc, Contraintes de déductibilité dans une algèbre quotient: réduction de modèles et applications à la sécurité, Thèse de doctorat, 2009.

S. Bursuc, H. Comon-lundh, and S. Delaune, Associative-Commutative Deducibility Constraints, Proceedings of the 24th Annual Symposium on Theoretical Aspects of Computer Science (STACS'07), p.634645, 2007.
DOI : 10.1007/978-3-540-70918-3_54

Y. Chevalier, R. Küsters, M. Rusinowitch, and M. Turuani, Deciding the security of protocols with die-hellman exponentiation and products in exponents

Y. Chevalier, R. Küsters, 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., pp.247-274, 2005.
DOI : 10.1109/LICS.2003.1210066
URL : https://hal.archives-ouvertes.fr/inria-00103954

Y. Chevalier, D. Lugiez, and M. Rusinowitch, Towards an Automatic Analysis of Web Service Security, FroCoS, p.133147, 2007.
DOI : 10.1007/978-3-540-74621-8_9
URL : https://hal.archives-ouvertes.fr/inria-00557707

Y. Chevalier and M. Rusinowitch, Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures, ICALP 2005 -Track C: Security and Cryptography Foundations, pp.4111261-1282, 2010.
DOI : 10.1016/j.tcs.2009.10.022
URL : https://hal.archives-ouvertes.fr/inria-00455290

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., p.271280, 2003.
DOI : 10.1109/LICS.2003.1210067

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

C. J. Cremers, The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols, Computer Aided Verication, 20th International Conference, p.414418, 2008.
DOI : 10.1007/978-3-540-70545-1_38

S. Delaune, P. Lafourcade, D. Lugiez, and R. Treinen, Symbolic protocol analysis for monoidal equational theories, Information and Computation, vol.206, issue.2-4, p.312351, 2008.
DOI : 10.1016/j.ic.2007.07.005
URL : https://hal.archives-ouvertes.fr/hal-00496352

L. Mazaré, Satisability of Dolev-Yao Constraints, Electronic Notes in Theoretical Computer Science, vol.125, issue.1, p.109124, 2005.

L. Mazaré, Computational Soundness of Symbolic Models for Cryptographic Protocols, 2006.

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, p.166175, 2001.
DOI : 10.1145/501983.502007

M. Rusinowitch and M. Turuani, Protocol insecurity with a nite number of sessions, composed keys is np-complete, Theor. Comput. Sci, issue.299, pp.1-3451475, 2003.

V. Shmatikov, Decidable Analysis of Cryptographic Protocols with Products and Modular Exponentiation
DOI : 10.1007/978-3-540-24725-8_25

P. Syverson, C. Meadows, and I. Cervesato, Dolev-Yao is no better than Machiavelli, First Workshop on Issues in the Theory of Security WITS'00, p.8792, 2000.

M. Turuani, The CL-Atse Protocol Analyser, Term Rewriting and Applications (RTA), p.277286, 2006.
DOI : 10.1007/11805618_21
URL : https://hal.archives-ouvertes.fr/inria-00103573

I. Unité-de-recherche-inria-lorraine and L. , 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