1: \begin{thebibliography}{10}
2:
3: \bibitem{akvw:set}
4: A.~Aiken, D.~Kozen, M.~Vardi, and E.~Wimmers.
5: \newblock The complexity of set constraints.
6: \newblock In {\em CSL'93}, volume 832 of {\em LNCS}, pages 1--17.
7: Springer-Verlag, 1993.
8:
9: \bibitem{BG:HAR}
10: L.~Bachmair and H.~Ganzinger.
11: \newblock Resolution theorem proving.
12: \newblock In J.~A. Robinson and A.~Voronkov, editors, {\em Handbook of
13: Automated Reasoning}, volume~I, chapter~2, pages 19--99. North-Holland, 2001.
14:
15: \bibitem{Blanchet:prolog}
16: B.~Blanchet.
17: \newblock An efficient cryptographic protocol verifier based on {P}rolog rules.
18: \newblock In {\em 14th IEEE Computer Security Foundations Workshop (CSFW'01)},
19: pages 82--96. IEEE Computer Society Press, Cape Breton, Nouvelle-{\'E}cosse,
20: Canada, 2001.
21:
22: \bibitem{kozen:alternation}
23: A.~K. Chandra, D.~C. Kozen, and L.~J. Stockmeyer.
24: \newblock Alternation.
25: \newblock {\em Journal of the ACM}, 28(1), Jan. 1981.
26:
27: \bibitem{cc:tamem}
28: H.~Comon and V.~Cortier.
29: \newblock Tree automata with one memory, set constraints and cryptographic
30: protocols.
31: \newblock {\em Theoretical Computer Science}, 331(1):143--214, 2005.
32:
33: \bibitem{comon:rta03}
34: H.~Comon-Lundh and V.~Cortier.
35: \newblock New decidability results for fragments of first-order logic and
36: application to cryptographic protocols.
37: \newblock In R.~Nieuwenhuis, editor, {\em 14th International Conference on
38: Rewriting Techniques and Applications (RTA'03)}, volume 2706 of {\em LNCS},
39: pages 148--164, Valencia, Spain, June 2003. Springer-Verlag.
40:
41: \bibitem{comon:esop03}
42: H.~Comon-Lundh and V.~Cortier.
43: \newblock Security properties: Two agents are sufficient.
44: \newblock In {\em 12th European Symposium on Programming (ESOP'03)}, volume
45: 2618 of {\em LNCS}, pages 99--113, Warsaw, Poland, Apr. 2003.
46: Springer-Verlag.
47:
48: \bibitem{cortier:thesis}
49: V.~Cortier.
50: \newblock {\em V\'erification Automatique des Protocoles Cryptographiques}.
51: \newblock PhD thesis, ENS Cachan, France, 2003.
52:
53: \bibitem{durgin:fmsp99}
54: N.~A. Durgin, P.~Lincoln, J.~Mitchell, and A.~Scedrov.
55: \newblock Undecidability of bounded security protocols.
56: \newblock In {\em Workshop on Formal Methods and Security Protocols (FMSP'99)},
57: Trento, Italy, 1999.
58:
59: \bibitem{ganzinger:instantiation}
60: H.~Ganzinger and K.~Korovin.
61: \newblock New directions in instantiation-based theorem proving.
62: \newblock In P.~G. Kolaitis, editor, {\em 18th Annual IEEE Symposium on Logic
63: in Computer Science (LICS'03)}, pages 55--64, Ottawa, Canada, June 2003. IEEE
64: Computer Society Press.
65:
66: \bibitem{JGL:SOresol}
67: J.~Goubault-Larrecq.
68: \newblock R{\'e}solution ordonn{\'e}e avec s{\'e}lection et classes
69: d{\'e}cidables de la logique du premier ordre.
70: \newblock Lecture notes for the course ``d{\'e}monstration automatique et
71: v{\'e}rification de protocoles cryptographiques'' (with Hubert Comon-Lundh),
72: DEA ``programmation'', 2004.
73: \newblock 71 pages, \url{http://www.lsv.ens-cachan.fr/~goubault/SOresol.ps}.
74:
75: \bibitem{glrv:jlap04}
76: J.~Goubault-Larrecq, M.~Roger, and K.~N. Verma.
77: \newblock Abstraction and resolution modulo {AC}: How to verify
78: {D}iffie-{H}ellman-like protocols automatically.
79: \newblock {\em Journal of Logic and Algebraic Programming}, 64(2):219--251,
80: Aug. 2005.
81:
82: \bibitem{Monniaux:SAS99}
83: D.~Monniaux.
84: \newblock Abstracting cryptographic protocols with tree automata.
85: \newblock In A.~Cortesi and G.~Fil\'e, editors, {\em 6th International Static
86: Analysis Symposium (SAS'99)}, volume 1694 of {\em LNCS}, pages 149--163,
87: Venice, Italy, September 1999. Springer-Verlag.
88:
89: \bibitem{seidl:h1}
90: F.~Nielson, H.~R. Nielson, and H.~Seidl.
91: \newblock Normalizable {H}orn clauses, strongly recognizable relations and
92: {Spi}.
93: \newblock In {\em 9th Static Analysis Symposium (SAS'02)}, volume 24477 of {\em
94: LNCS}, pages 20--35. Springer-Verlag, 2002.
95:
96: \bibitem{voronkov:splitting}
97: A.~Riazanov and A.~Voronkov.
98: \newblock Splitting without backtracking.
99: \newblock In {\em IJCAI'01}, pages 611--617, 2001.
100:
101: \bibitem{Turuani:np}
102: M.~Rusinowitch and M.~Turuani.
103: \newblock Protocol insecurity with finite number of sessions is {NP}-complete.
104: \newblock In P.~Pandya and J.~Radhakrishnan, editors, {\em 14th IEEE Computer
105: Security Foundations Workshop (CSFW'01)}, Cape Breton, Nova-Scotia, Canada,
106: June 2001. IEEE Computer Society Press.
107:
108: \bibitem{Weidenbach:crypto}
109: C.~Weidenbach.
110: \newblock Towards an automatic analysis of security protocols.
111: \newblock In H.~Ganzinger, editor, {\em 16th International Conference on
112: Automated Deduction (CADE'99)}, number 1632 in LNAI, pages 378--382.
113: Springer-Verlag, 1999.
114:
115: \end{thebibliography}
116: