L. [. Armando and . 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

P. [. Asokan and . Ginzboorg, Key agreement in ad hoc networks, Computer Communications, vol.23, issue.17, pp.1627-1637, 2000.
DOI : 10.1016/S0140-3664(00)00249-8

S. [. Basin, L. Mödersheim, and . 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

B. Blanchet and A. Podelski, Verification of cryptographic protocols: Tagging enforces termination, Foundations of Software Science and Computational Structures FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003 Proceedings, volume 2620 of Lecture Notes in Computer Science, pp.136-152, 2003.

D. Dolev and A. Yao, On the security of public key protocols, IEEE Transactions on Information Theory, vol.29, issue.2, pp.198-208, 1981.
DOI : 10.1109/TIT.1983.1056650

D. [. Bull and . Otway, The authentication protocol, Defence Research Agency, 1997.

A. [. Kremer, R. Mercier, and . Treinen, Proving Group Protocols Secure Against Eavesdroppers, Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR'08), 2008.
DOI : 10.1007/978-3-540-71070-7_9
URL : https://hal.archives-ouvertes.fr/hal-00496351

K. O. Kürtz, R. Küsters, and T. Wilke, Selecting theories and nonce generation for recursive protocols, FMSE '07: Proceedings of the 2007 ACM workshop on Formal methods in security engineering, pp.61-70, 2007.

T. [. Küsters, E. Truderung, and . Zurich, On the automatic analysis of recursive security protocols with xor An abridged version appears in STACS, 2007.

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

]. C. Mea00 and . Meadows, Extending formal cryptographic protocol analysis techniques for group protocols and low-level cryptographic primitives, the First Workshop on Issues in the Theory of Security, pp.87-92, 2000.

]. S. Mit97 and . Mittra, Iolus: A framework for scalable secure multicasting, SIGCOMM, pp.277-288, 1997.

C. Meadows and P. Syverson, Formalizing GDOI group key management requirements in NPATRL, Proceedings of the 8th ACM conference on Computer and Communications Security , CCS '01, pp.235-244, 2001.
DOI : 10.1145/501983.502016
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.914

J. Meseguer and P. Thati, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, Higher-Order and Symbolic Computation, pp.123-160, 2007.

L. C. Paulson, Isabelle: A generic theorem prover, Lecture Notes in Computer Science, vol.828, pp.283-298, 1996.
DOI : 10.1007/BFb0030541

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

O. Pereira and J. Quisquater, Some attacks upon authenticated group key agreement protocols, Journal of Computer Security, vol.11, issue.4, pp.555-580, 2003.
DOI : 10.3233/JCS-2003-11404
URL : http://doi.org/10.3233/jcs-2003-11404

O. Pereira and J. Quisquater, Generic insecurity of cliques-type authenticated group key agreement protocols, Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004., pp.16-19, 2004.
DOI : 10.1109/CSFW.2004.1310729

I. Ramanujam and S. P. Suresh, Tagging Makes Secrecy Decidable with Unbounded Nonces as Well, FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, 23rd Conference Proceedings, volume 2914 of Lecture Notes in Computer Science, pp.363-374, 2003.
DOI : 10.1007/978-3-540-24597-1_31

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

A. [. Steel and . Bundy, Attacking Group Multicast Key Management Protocols Using Coral, Proceedings of the ARSPA Workshop, pp.125-144, 2004.
DOI : 10.1016/j.entcs.2004.05.023

M. Steiner, M. Waidner, and G. Tsudik, CLIQUES: a new approach to group key agreement, Proceedings. 18th International Conference on Distributed Computing Systems (Cat. No.98CB36183), 1998.
DOI : 10.1109/ICDCS.1998.679745

D. [. Taghdiri and . Jackson, A Lightweight Formal Analysis of a Multicast Key Management Scheme, pp.240-256, 2003.
DOI : 10.1016/0743-1066(95)00095-X

T. Truderung, Selecting Theories and Recursive Protocols, pp.217-232, 2005.
DOI : 10.1007/11539452_19

M. Turuani, The CL-Atse Protocol Analyser, Term Rewriting and Applications -Proc. of RTA, pp.277-286, 2006.
DOI : 10.1007/11805618_21
URL : https://hal.archives-ouvertes.fr/inria-00103573

C. Weidenbach, Towards an Automatic Analysis of Security Protocols in First-Order Logic, 16th International Conference on Automated Deduction, pp.314-328, 1999.
DOI : 10.1007/3-540-48660-7_29

I. Centre-de-recherche, ?. Nancy, and L. Est, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès