M. Abadi and R. M. Needham, Prudent engineering practice for cryptographic protocols, IEEE Transactions on Software Engineering, vol.22, issue.1, pp.6-15, 1996.
DOI : 10.1109/32.481513

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.225.1311

R. Amadio and W. Charatonik, On Name Generation and Set-Based Analysis in the Dolev-Yao Model, Proc. Inter. Conference on Concurrency Theory, pp.499-514, 2002.
DOI : 10.1007/3-540-45694-5_33

B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., pp.82-96, 2001.
DOI : 10.1109/CSFW.2001.930138

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.5150

B. Blanchet and A. Podelski, Verification of cryptographic protocols: Tagging enforces termination, Foundations of Software Science and Computation Structures (FoS- SaCS'03), 2003.
DOI : 10.1016/j.tcs.2004.10.018

URL : http://doi.org/10.1016/j.tcs.2004.10.018

R. Canetti, C. Meadows, and P. F. Syverson, Environmental Requirements for Authentication Protocols, Proc. Symposium on Software Security ? Theories and Systems, pp.339-355, 2002.
DOI : 10.1007/3-540-36532-X_21

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.148.8214

H. Comon-lundh and V. Cortier, Security properties: two agents are sufficient, Science of Computer Programming, vol.50, issue.1-3, pp.51-71, 2004.
DOI : 10.1016/j.scico.2003.12.002

URL : https://hal.archives-ouvertes.fr/inria-00099981

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

V. Cortier and E. Zalinescu, Deciding Key Cycles for Security Protocols, Proc. 13th Inter. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), pp.317-331, 2006.
DOI : 10.1007/11916277_22

URL : https://hal.archives-ouvertes.fr/inria-00181625

A. Datta, A. Derek, J. Mitchell, and D. Pavlovic, A derivation system and compositional logic for security protocols, Journal of Computer Security, vol.13, issue.3, 2005.
DOI : 10.3233/JCS-2005-13304

URL : http://doi.org/10.3233/jcs-2005-13304

L. Gong and P. Syverson, Fail-stop protocols: An approach to designing secure protocols, Proc. 5th Inter. Working Conference on Dependable Computing for Critical Applications, pp.44-55, 1995.

J. D. Guttman and F. J. Thayer, Protocol independence through disjoint encryption, Proceedings 13th IEEE Computer Security Foundations Workshop. CSFW-13, pp.24-34, 2000.
DOI : 10.1109/CSFW.2000.856923

J. Kelsey, B. Schneier, and D. Wagner, Protocol interactions and the chosen protocol attack, Proc. 5th Inter. Workshop on Security Protocols, pp.91-104, 1997.
DOI : 10.1007/BFb0028162

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

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.3643

R. Needham and M. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, vol.21, issue.12, pp.993-999, 1978.
DOI : 10.1145/359657.359659

M. Rusinowitch and M. Turuani, Protocol insecurity with a finite number of sessions and composed keys is NP-complete, Theoretical Computer Science, vol.299, issue.1-3, pp.451-475, 2003.
DOI : 10.1016/S0304-3975(02)00490-5

H. Seidl and K. N. Verma, Flat and one-variable clauses, Proc. 11th Inter. Conference on Logic for Programming, 2005.
DOI : 10.1145/1380572.1380577

?. Let-w, Moreover, thanks to (?), we have that n(T ? ?) ? n(T ? ) ? {init}. Hence, we deduce that n(w?) ? n(T ? ) ? {init}, Thus, n(w?) ? Names = ?

. Hence-?, v i j ?} ? u i j ? by relying on the fact that T 0 , v 1 ?, v 2 ?, . . . , v i j ?1 ? ? u i j ?. INRIA Unité de recherche INRIA Lorraine LORIA, 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, rue Jacques Monod -91893 ORSAY Cedex

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.