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-00099982

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.

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.

K. Cohn-gordon, C. Cremers, L. Garratt, J. Millican, and K. Milner, On ends-toends encryption: Asynchronous group messaging with strong security guarantees, Proceedings of the, 2018.

, ACM SIGSAC Conference on Computer and Communications Security, pp.1802-1819, 2018.

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

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, IJCAR 2016, vol.9706, pp.183-192, 2016.

A. K. Eeralla, S. Erbatur, A. M. Marshall, and C. Ringeissen, Rule-based unification in combined theories and the finite variant property, Language and Automata Theory and Applications -13th International Conference, vol.11417, pp.356-367, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01988419

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. Erbatur, A. M. Marshall, D. Kapur, and P. Narendran, Unification over distributive exponentiation (sub)theories, Journal of Automata, Languages and Combinatorics (JALC), vol.16, issue.2-4, pp.109-140, 2011.

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, Mathematical Structures in Computer Science, pp.1-27, 2020.
URL : https://hal.archives-ouvertes.fr/hal-02966957

S. Escobar, C. A. Meadows, and J. Meseguer, Maude-NPA: Cryptographic protocol analysis modulo equational properties, Foundations of Security Analysis and Design, 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.

D. Kim, C. Lynch, and P. Narendran, Reviving basic narrowing modulo, Frontiers of Combining Systems -12th International Symposium, vol.11715, pp.313-329, 2019.

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.

A. M. Marshall, C. A. Meadows, and P. Narendran, On unification modulo onesided distributivity: Algorithms, variants and asymmetry, Logical Methods in Computer Science, vol.11, issue.2, 2015.

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, 2013.

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

K. Nguyen, Work done under the supervision of Vincent Cheval and Véronique Cortier

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.

E. Tidén and S. Arnborg, Unification problems with one-sided distributivity, Journal of Symbolic Computation, vol.3, issue.1, pp.183-202, 1987.

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