M. Abadi and V. Cortier, Deciding knowledge in security protocols under equational theories, INRIA, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00000554

M. Abadi and V. Cortier, Deciding knowledge in security protocols under equational theories, Theor. Comput. Sci, vol.367, issue.1-2, pp.2-32, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000554

M. Abadi and C. Fournet, Mobile values, new names, and secure communication, Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'01, pp.104-115, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01423924

P. Siva-anantharaman, M. Narendran, and . Rusinowitch, Intruders with caps, Term Rewriting and Applications, 18th International Conference, vol.4533, pp.20-35, 2007.

F. Baader and T. Nipkow, Term rewriting and all that, 1998.

M. Baudet, V. Cortier, and S. Delaune, YAPA: A generic tool for computing intruder knowledge, ACM Trans. Comput. Log, vol.14, issue.1, p.4, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00732901

H. Comon, M. Haberstrau, and J. Jouannaud, Syntacticness, cyclesyntacticness, and shallow theories, Inf. Comput, vol.111, issue.1, pp.154-191, 1994.

B. Conchinha, D. A. Basin, and C. Caleiro, FAST: an efficient decision procedure for deduction and static equivalence, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, vol.10, pp.11-20, 2011.

V. Cortier and S. Delaune, Decidability and combination results for two notions of knowledge in security protocols, Journal of Automated Reasoning, vol.48, issue.4, pp.441-487, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00525778

S. ¸tefan-ciobâc?-a, S. Delaune, and S. Kremer, Computing knowledge in security protocols under convergent equational theories, J. Autom. Reasoning, vol.48, issue.2, pp.219-262, 2012.

S. Erbatur, D. Kapur, and A. M. Marshall, Paliath Narendran, and Christophe Ringeissen. Unification and matching in hierarchical combinations of syntactic theories, Frontiers of Combining Systems-10th International Symposium, FroCoS 2015, Wroclaw, Poland. Proceedings, vol.9322, pp.291-306, 2015.

S. Erbatur, A. M. Marshall, and C. Ringeissen, Notions of knowledge in combinations of theories sharing constructors, Automated Deduction-CADE 26-26th International Conference on Automated Deduction, vol.10395, pp.60-76, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01587181

S. Erbatur, A. M. Marshall, and C. Ringeissen, Computing knowledge in equational extensions of subterm convergent theories, 2018.

K. A. Gero, Deciding Static Inclusion for Delta-strong and Omega Delta-strong Intruder Theories: Applications to Cryptographic Protocol Analysis, 2015.

J. Kirchner, Completion of a set of rules modulo a set of equations, SIAM J. Comput, vol.15, issue.4, pp.1155-1194, 1986.

C. Kirchner and F. Klay, Syntactic theories and unification, Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on Logic in Computer Science, pp.270-277, 1990.

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, pp.166-175, 2001.

C. Lawrence and . Paulson, The inductive approach to verifying cryptographic protocols, Computer Security, vol.6, p.85128, 1998.

M. Schmidt-schauß, Unification in permutative equational theories is undecidable, J. Symb. Comput, vol.8, issue.4, pp.415-421, 1989.

F. Yang, S. Escobar, C. Meadows, J. Meseguer, and P. Narendran, Theories of homomorphic encryption, unification, and the finite variant property, Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, PPDP '14, pp.123-133, 2014.
DOI : 10.1145/2643135.2643154