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

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

F. Baader and K. U. Schulz, Unification in the union of disjoint equational theories: Combining decision procedures, Journal of Symbolic Computation, vol.21, issue.2, pp.211-243, 1996.

F. Baader and W. Snyder, Unification theory, Handbook of Automated Reasoning, pp.445-532, 2001.

D. A. Basin, S. Mödersheim, and L. Viganò, An on-the-fly model-checker for security protocol analysis, Computer Security-ESORICS 2003, 8th European Symposium on Research in Computer Security, vol.2808, pp.253-270, 2003.

. Springer, , 2003.

B. Blanchet, Modeling and verifying security protocols with the Applied Pi calculus and proverif, Foundations and Trends in Privacy and Security, vol.1, issue.1-2, pp.1-135, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01423760

C. Bouchard, K. A. Gero, C. Lynch, and P. Narendran, On forward closure and the finite variant property, Frontiers of Combining Systems-9th International Symposium, vol.8152, pp.327-342, 2013.

S. Ciobâc?, 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.

H. Comon-lundh and S. Delaune, The finite variant property: How to get rid of some algebraic properties, Rewriting Techniques and Applications, vol.3467, pp.294-307, 2005.

F. Durán, S. Eker, S. Escobar, N. Martí-oliet, J. Meseguer et al., Built-in variant generation and unification, and their applications in Maude 2.7, Automated Reasoning-8th International Joint Conference, vol.9706, pp.183-192, 2016.

A. K. Eeralla and C. Lynch, Bounded ACh Unification. CoRR, 2018.

S. Erbatur, D. Kapur, A. M. Marshall, P. Narendran, and C. Ringeissen, Hierarchical combination, 24-24th International Conference on Automated Deduction, vol.7898, pp.249-266, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00878649

S. Escobar, C. A. Meadows, and J. Meseguer, Maude-NPA: Cryptographic protocol analysis modulo equational properties, Lecture Notes in Computer Science, vol.5705, pp.1-50, 2007.

S. Escobar, R. Sasse, and J. Meseguer, Folding variant narrowing and optimal variant termination, J. Log. Algebr. Program, vol.81, issue.7-8, pp.898-928, 2012.

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

J. Jouannaud and C. Kirchner, Solving equations in abstract algebras: A rule-based survey of unification, Computational Logic-Essays in Honor of Alan Robinson, pp.257-321, 1991.

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.

C. Lynch and B. Morawska, Automated Deduction-CADE-18, 18th International Conference on Automated Deduction, vol.2392, pp.471-485, 2002.

S. Meier, B. Schmidt, C. Cremers, and D. A. Basin, The TAMARIN prover for the symbolic analysis of security protocols, Computer Aided Verification-25th International Conference, CAV 2013, vol.8044, pp.696-701, 1319.

J. Meseguer, Variant-based satisfiability in initial algebras, Sci. Comput. Program, vol.154, pp.3-41, 2018.

P. Narendran, F. Pfenning, and R. Statman, On the unification problem for cartesian closed categories, Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pp.57-63, 1993.

T. Nipkow, Proof transformations for equational theories, Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on Logic in Computer Science, pp.278-288, 1990.

M. Schmidt-schauß, Unification in a combination of arbitrary disjoint equational theories, Journal of Symbolic Computation, vol.8, pp.51-99, 1989.

F. Yang, S. Escobar, C. A. 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, pp.123-133, 2014.

K. A. Yelick, Unification in combinations of collapse-free regular theories, Journal of Symbolic Computation, vol.3, issue.1-2, pp.153-181, 1987.

S. Let and . Rhs-(r), If (G, ?) is R-normalized, S |= G? and G is not in dag solved form, then there exist some G and a substitution ?