A. [. Abdulla, A. Annichini, and . Bouajjani, Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol, Tools and Algorithms for the Construction and Analysis of Systems , TACAS'99, pp.208-222, 1999.
DOI : 10.1007/3-540-49059-0_15

B. [. Abadi and . Blanchet, Computer-assisted verification of a protocol for certified email, Science of Computer Programming, vol.58, issue.1-2, pp.3-27, 2005.
DOI : 10.1016/j.scico.2005.02.002

D. Armando, Y. Basin, Y. Boichut, L. Chevalier, J. Compagna et al., The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, Computer Aided Verification, CAV'05, pp.281-285, 2005.
DOI : 10.1007/11513988_27
URL : https://hal.archives-ouvertes.fr/inria-00000408

A. [. Abdulla, B. Bouajjani, and . Jonsson, On-the-fly analysis of systems with unbounded, lossy FIFO channels, Computer Aided Verification , CAV'98, pp.305-322, 1998.
DOI : 10.1007/BFb0028754

L. [. Armando and . Compagna, An Optimized Intruder Model for SAT-based Model-Checking of Security Protocols, Electronic Notes in Theoretical Computer Science, vol.125, issue.1, pp.91-108, 2005.
DOI : 10.1016/j.entcs.2004.05.021

R. [. Aldini and . Gorrieri, Security Analysis of a Probabilistic Non-repudiation Protocol, Process Algebra and Probabilistic Methods : Performance Modeling and Verification, pp.17-36, 2002.
DOI : 10.1007/3-540-45605-8_3

]. P. Aldr06, A. Abdulla, J. Legay, A. Orso, and . Rezine, Tree regular model checking: A simulation-based approach, Journal of Logic and Algebraic Programming, vol.69, issue.12, pp.93-121, 2006.

M. [. Blanchet, C. Abadi, and . Fournet, Automated Verification of Selected Equivalences for Security Protocols, 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), pp.3-51, 2008.
DOI : 10.1109/LICS.2005.8

C. [. Bozga, Y. Ene, and . Lakhnech, A symbolic decision procedure for cryptographic protocols with time stamps, The Journal of Logic and Algebraic Programming, vol.65, issue.1, pp.1-35, 2005.
DOI : 10.1016/j.jlap.2004.09.007

A. Bouajjani, X. Esparza, and T. Touili, A Generic Approach to the Static Analysis of Concurrent Programs with Procedures, International Journal of Foundations of Computer Science, vol.14, issue.04, pp.551-582, 2003.
DOI : 10.1142/S0129054103001893
URL : https://hal.archives-ouvertes.fr/hal-00161114

J. [. Bouajjani, T. Esparza, and . Touili, Reachability Analysis of Synchronized PA Systems, Electronic Notes in Theoretical Computer Science, vol.138, issue.3, pp.153-178, 2005.
DOI : 10.1016/j.entcs.2005.02.063
URL : https://hal.archives-ouvertes.fr/hal-00161111

A. [. Bardin, J. Finkel, and . Leroux, FASTer Acceleration of Counter Automata in Practice, Lecture Notes in Computer Science, vol.2988, pp.576-590, 2004.
DOI : 10.1007/978-3-540-24730-2_42

P. [. Boigelot and . Godefroid, Symbolic verification of communication protocols with infinite state spaces using QDDs, Computer Aided Verification , CAV'96, pp.1-12, 1996.
DOI : 10.1007/3-540-61474-5_53

. [. Boichut, . Th, and . Genet, Feasible Trace Reconstruction for Rewriting Approximations, Rewriting Techniques and Applications, RTA'06, pp.123-135
DOI : 10.1007/11805618_10
URL : https://hal.archives-ouvertes.fr/hal-00463426

. [. Boichut, . Th, T. P. Genet, L. Jensen, and . Le-roux, Rewriting Approximations for Fast Prototyping of Static Analyzers, Rewriting Techniques and Applications, RTA'07 Proceedings, pp.48-62, 2007.
DOI : 10.1007/978-3-540-73449-9_6
URL : https://hal.archives-ouvertes.fr/hal-00463418

P. [. Boichut, O. Héam, and . Kouchnarenko, Automatic Verification of Security Protocols Using Approximations, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00070291

P. [. Boichut, O. Héam, and . Kouchnarenko, Handling Algebraic Properties in Automatic Analysis of Security Protocols, International Colloquium on Theorical Aspects of Computing, ICTAC'06, pp.153-167, 2006.
DOI : 10.1007/11921240_11
URL : https://hal.archives-ouvertes.fr/hal-00463424

P. [. Boichut, O. Héam, and . Kouchnarenko, Tree Automata for Detecting Attacks on Protocols with Algebraic Cryptographic Primitives, Verification of Infinite-State Systems, INFINITY'07 The final version will be published in EN in Theoretical Computer Science, pp.44-53, 2007.
DOI : 10.1016/j.entcs.2009.05.030
URL : https://hal.archives-ouvertes.fr/hal-00561374

P. [. Bouajjani, A. Habermehl, T. Rogalewicz, and . Vojnar, Abstract Regular Tree Model Checking, Electronic Notes in Theoretical Computer Science, vol.149, issue.1, pp.37-48, 2006.
DOI : 10.1016/j.entcs.2005.11.015
URL : https://hal.archives-ouvertes.fr/hal-00156828

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

Y. [. Bozga, M. Lakhnech, and . Perin, HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols, Computer Aided Verification , CAV'03, pp.219-222, 2003.
DOI : 10.1007/978-3-540-45069-6_23

A. [. Bouajjani, T. Muscholl, and . Touili, Permutation rewriting and algorithmic verification, Information and Computation, vol.205, issue.2, pp.199-224, 2007.
DOI : 10.1016/j.ic.2005.11.007
URL : https://hal.archives-ouvertes.fr/hal-00161120

M. Basin and V. , An On-the-Fly Model-Checker for Security Protocol Analysis, European Symposium on Research in Computer Security, ESORICS'03, pp.253-270, 2003.
DOI : 10.1007/978-3-540-39650-5_15

T. [. Bouajjani and . Touili, Extrapolating Tree Transformations, Computer Aided Verification, CAV'02 Copenhagen (Denmark), pp.539-554, 2002.
DOI : 10.1007/3-540-45657-0_46
URL : https://hal.archives-ouvertes.fr/hal-00161115

P. [. Boigelot and . Wolper, Verifying systems with infinite but regular state spaces, Computer Aided Verification, CAV'98, pp.88-97, 1998.

R. Dauchet, F. Gilleron, D. Jacquemard, S. Lugiez, M. Tison et al., Tree Automata Techniques and Applications, 2002.

[. Coquidé, M. Dauchet, R. Gilleron, and S. Vágvölgyi, Bottom-up tree pushdown automata and rewrite systems, Rewriting Techniques and Applications, RTA'91, pp.287-298, 1991.
DOI : 10.1007/3-540-53904-2_104

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

A. [. Cece and . Finkel, Verification of programs with half-duplex communication . Information and Computation, pp.166-190, 2005.

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

[. Chevalier, R. Kusters, 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

C. J. Cremers and P. Lafourcade, Comparing state spaces in security protocol analysis In Automated Verification of Critical Systems, AVoCS'07, Electronic Notes in Theoretical Computer Science Comon-Lundh and V. Cortier. Security properties: two agents are sufficient, European Symposium on Programming, ESOP'03, pp.49-63, 2007.

V. [. Comon-lundh and . Cortier, Tree automata with one memory set constraints and cryptographic protocols, Theoretical Computer Science, vol.331, issue.1, pp.143-214, 2005.
DOI : 10.1016/j.tcs.2004.09.036
URL : https://hal.archives-ouvertes.fr/inria-00000553

V. [. Comon-lundh and . 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

[. Chevalier and M. Rusinowitch, Combining Intruder Theories, International Colloquium on Automata, Languages and Programming, ICAPL'05, pp.639-651, 2005.
DOI : 10.1007/11523468_52
URL : https://hal.archives-ouvertes.fr/inria-00070512

]. C. Cre06 and . Cremers, Scyther -Semantics and Verification of Security Protocols Comon-Lundh and R. Treinen. Easy intruder deductions Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, Lecture Notes in Computer Science, vol.2772, pp.225-242, 2003.

S. Delaune, Easy intruder deduction problems with homomorphisms, Information Processing Letters, vol.97, issue.6, pp.213-218, 2006.
DOI : 10.1016/j.ipl.2005.11.008
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.96.2785

F. [. Delaune and . Jacquemard, Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks, Journal of Automated Reasoning, vol.40, issue.2, pp.85-124, 2006.
DOI : 10.1007/s10817-005-9017-7
URL : https://hal.archives-ouvertes.fr/inria-00578855

P. [. Durgin, J. C. Lincoln, A. Mitchell, and . Scedrov, Undecidability of Bounded Security Protocols, Formal Methods and Security Protocols , FMSP'99, 1999.

P. [. Durgin, J. C. Lincoln, A. Mitchell, and . Scedrov, Multiset rewriting and the complexity of bounded security protocols, Proc. FloC'99, pp.247-311, 2004.
DOI : 10.3233/JCS-2004-12203

Y. [. Dams, M. Lakhnech, and . Steffen, Iterating transducers, Journal of Logic and Algebraic Programming, pp.52-53109, 2002.
DOI : 10.1007/3-540-44585-4_27

T. Dauchet, The theory of ground rewrite systems is decidable, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, 1990.
DOI : 10.1109/LICS.1990.113750

C. [. Escobar, J. Meadows, and . Meseguer, Equational Cryptographic Reasoning in the Maude-NRL Protocol Analyzer, Electronic Notes in Theoretical Computer Science, vol.171, issue.4, pp.23-36, 2007.
DOI : 10.1016/j.entcs.2007.02.053

. [. Feuillade, . Th, V. Genet, and . Viet-triem-tong, Reachability Analysis over Term Rewriting Systems, Journal of Automated Reasoning, vol.37, issue.1?2, pp.3-4341, 2004.
DOI : 10.1007/s10817-004-6246-0
URL : https://hal.archives-ouvertes.fr/inria-00071609

J. [. Finkel and . Leroux, How to Compose Presburger-Accelerations: Applications to Broadcast Protocols, Fundations of Software Technology and Theoretical Computer Science FSTTCS'02, pp.145-156, 2002.
DOI : 10.1007/3-540-36206-1_14

A. Finkel, B. Willems, and P. Wolper, A Direct Symbolic Approach to Model Checking Pushdown Systems (extended abstract), Verification of Infinite State Systems, INFINITY'97, pp.27-39, 1997.
DOI : 10.1016/S1571-0661(05)80426-8

. Th, F. Genet, and . Klay, Rewriting for Cryptographic Protocol Verification, Conference on Automated Deduction, CADE'00, pp.271-290, 2000.

M. [. Goubault-larrecq, K. N. Roger, and . Verma, Abstraction and resolution modulo AC: How to verify Diffie???Hellman-like protocols automatically, The Journal of Logic and Algebraic Programming, vol.64, issue.2, pp.219-251, 2005.
DOI : 10.1016/j.jlap.2004.09.004
URL : http://doi.org/10.1016/j.jlap.2004.09.004

S. [. Gilleron and . Tison, Regular tree languages and rewrite systems, Fundamenta Informatica, vol.24, issue.12, pp.157-174, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00538882

]. F. Jac96 and . Jacquemard, Decidable approximations of term rewriting systems, Rewriting Techniques and Applications, RTA'96, volume 1103 of Lecture Notes in Computer Sciences, pp.362-376, 1996.

M. [. Jonsson and . Nilsson, Transitive Closures of Regular Relations for Verifying Infinite-State Systems, Tools and Algorithms for Construction and Analysis of Systems, TACAS'00, pp.220-234, 2000.
DOI : 10.1007/3-540-46419-0_16

M. [. Kremer and . Ryan, Analysis of an Electronic Voting Protocol in the Applied Pi Calculus, European Symposium on Programming, ESOP'05, pp.186-200, 2005.
DOI : 10.1007/978-3-540-31987-0_14

R. Küsters, . Th, and . Wilke, Automata-Based Analysis of Recursive Cryptographic Protocols, Symposium on Theoretical Aspects of Computer Science, STACS'04, pp.382-393, 2004.
DOI : 10.1007/978-3-540-24749-4_34

B. [. Legall and . Jeannet, Lattice Automata: A Representation for Languages on Infinite Alphabets, and Some Applications to Verification, Static Analysis Symposium, SAS'07, pp.52-68, 2007.
DOI : 10.1007/978-3-540-74061-2_4

[. Lafourcade, D. Lugiez, and R. Treinen, Intruder deduction for the equational theory of Abelian groups with distributive encryption, Information and Computation, vol.205, issue.4, pp.581-623, 2007.
DOI : 10.1016/j.ic.2006.10.008
URL : https://hal.archives-ouvertes.fr/hal-00496353

J. C. Mitchell, M. Mitchell, and U. Stern, Automated analysis of cryptographic protocols using mur, Proceedings of the 1997 Conference on Security and Privacy (S&P-97), pp.141-153, 1997.

]. S. Möd07, E. Mödersheim, and . Zürich, Models and Methods for the Automated Analysis of Security Protocols, 2007.

]. D. Mon99 and . Monniaux, Abstracting cryptographic protocols with tree automata, Static Analysis Symposium, SAS'99, pp.149-163, 1999.

E. [. Nielsen, H. R. Andersen, and . Nielson, Static Validation of a Voting Protocol, Automated Reasoning for Security Protocol Analysis, pp.115-134, 2005.
DOI : 10.1016/j.entcs.2005.06.001

. [. Nanz, . Ch, and . Hankin, A framework for security analysis of mobile wireless networks, Theoretical Computer Science, vol.367, issue.1-2, pp.203-227, 2006.
DOI : 10.1016/j.tcs.2006.08.036

T. [. Ohsaki and . Takai, ACTAS : A System Design for Associative and Commutative Tree Automata Theory, Electronic Notes in Theoretical Computer Science, vol.124, issue.1, pp.97-111, 2005.
DOI : 10.1016/j.entcs.2004.07.017

E. [. Pnueli, M. Shahar, and . Turuani, Liveness and acceleration in parameterized verification Protocol insecurity with finite number of sessions is NP-complete, Computer Aided Verification, CAV'00 Computer Security Foundations Workshop CSFW '01, pp.328-343, 2000.

J. [. Réty and . Vuotto, Regular Sets of Descendants by Some Rewrite Strategies, Rewriting Techniques and Applications, RTA'02, pp.129-143, 2002.
DOI : 10.1007/3-540-45610-4_10

K. Salomaa, Deterministic tree pushdown automata and monadic tree rewriting systems, Journal of Computer and System Sciences, vol.37, issue.3, pp.367-394, 1988.
DOI : 10.1016/0022-0000(88)90014-1
URL : http://doi.org/10.1016/0022-0000(88)90014-1

[. Song, Athena: A new efficient automatic checker for security protocol analysis, Computer Security Fondations Workshop, CSFW'99, pp.192-202, 1999.

]. T. Tru05 and . Truderung, Regular protocols and attacks with regular knowledge, Conference on Automated Deduction, CADE'05, pp.377-391, 2005.

P. [. Zunino and . Degano, Handling exp,?? (and Timestamps) in Protocol Analysis, Foundations of Software Science and Computation Structures , FoSSaCS'06, pp.413-427, 2006.
DOI : 10.1007/11690634_28