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.
DOI : 10.1006/jsco.1996.0009

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

B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., p.82, 2001.
DOI : 10.1109/CSFW.2001.930138

C. Bouchard, K. A. Gero, C. Lynch, and P. Narendran, On Forward Closure and the Finite Variant Property, Frontiers of Combining Systems, pp.327-342, 2013.
DOI : 10.1007/978-3-642-40885-4_23

A. Boudet, Combining Unification Algorithms, Journal of Symbolic Computation, vol.16, issue.6, pp.597-626, 1993.
DOI : 10.1006/jsco.1993.1066

H. Comon-lundh and S. Delaune, The Finite Variant Property: How to Get Rid of Some Algebraic Properties, Rewriting Techniques and Applications, pp.294-307, 2005.
DOI : 10.1007/978-3-540-32033-3_22

S. Erbatur, S. Escobar, D. Kapur, Z. Liu, C. Lynch et al., Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions, Computer Security, ESORICS 2012, pp.73-90, 2012.
DOI : 10.1007/978-3-642-33167-1_5

S. Escobar, C. Meadows, and J. Meseguer, Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, Tutorial Lectures Lecture Notes in Computer Science, vol.20, issue.1-2, pp.1-50, 2007.
DOI : 10.1007/s10990-007-9000-6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.226.3197

S. Escobar, J. Meseguer, and R. Sasse, Variant Narrowing and Equational Unification, Electronic Notes in Theoretical Computer Science, vol.238, issue.3, pp.103-119, 2009.
DOI : 10.1016/j.entcs.2009.05.015

S. Escobar, R. Sasse, and J. Meseguer, Folding variant narrowing and optimal variant termination, The Journal of Logic and Algebraic Programming, vol.81, issue.7-8, pp.898-928, 2012.
DOI : 10.1016/j.jlap.2012.01.002

J. and Y. Toyama, Modular Church-Rosser Modulo: The Complete Picture, Int. J. Software and Informatics, vol.2, issue.1, pp.61-75, 2008.

Z. Liu, Dealing Efficiently with Exclusive OR, Abelian Groups and Homomorphism in Cryptographic Protocol Analysis, 2012.

S. Meier, B. Schmidt, C. Cremers, and D. Basin, The TAMARIN Prover for the Symbolic Analysis of Security Protocols, Computer Aided Verification, pp.696-701, 2013.
DOI : 10.1007/978-3-642-39799-8_48

S. Mödersheim, Models and Methods for the Automated Analysis of Security Protocols, 2007.

M. Rusinowitch, On termination of the direct sum of term-rewriting systems, Information Processing Letters, vol.26, issue.2, pp.65-70, 1987.
DOI : 10.1016/0020-0190(87)90039-1
URL : https://hal.archives-ouvertes.fr/inria-00075874