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

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

Y. Chevalier, A Simple Constraint Solving Procedure for Protocols with Exclusive Or, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00099889

Y. Chevalier, R. Küsters, M. Rusinowitch, and M. Turuani, An NP decision procedure for protocol insecurity with XOR, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.261-270, 2003.
DOI : 10.1109/LICS.2003.1210066
URL : https://hal.archives-ouvertes.fr/inria-00071889

Y. Chevalier, R. Küsters, M. Rusinowitch, and M. Turuani, Deciding the Security of Protocols with Diffie-Hellman Exponentiation and Products in Exponents, FSTTCS 2003, pp.124-135, 2003.
DOI : 10.1007/978-3-540-24597-1_11
URL : https://hal.archives-ouvertes.fr/inria-00103935

Y. Chevalier, R. Küsters, M. Rusinowitch, and M. Turuani, Deciding the Security of Protocols with Commuting Public Key Encryption, Electronic Notes in Theoretical Computer Science, vol.125, issue.1, pp.55-66, 2005.
DOI : 10.1016/j.entcs.2004.05.019
URL : https://hal.archives-ouvertes.fr/inria-00100013

Y. Chevalier and L. Vigneron, A tool for lazy verification of security protocols, Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), pp.373-376, 2001.
DOI : 10.1109/ASE.2001.989832
URL : https://hal.archives-ouvertes.fr/inria-00107545

H. Comon-lundh and V. Shmatikov, Intruder deductions, constraint solving and insecurity decision in presence of exclusive or, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.271-280, 2003.
DOI : 10.1109/LICS.2003.1210067

Q. Guo, P. Narendran, and D. A. Wolfram, Unification and matching modulo nilpotence, CADE 1996, pp.261-274, 1996.
DOI : 10.1007/3-540-61511-3_90

S. Kepser and J. Richts, Optimisation techniques for combining constraint solvers, Frontiers of Combining Systems 2, Papers presented at FroCoS'98, pp.193-210, 1999.

J. K. 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.
DOI : 10.1145/501983.502007

P. Y. Ryan and S. A. Schneider, An attack on a recursive authentication protocol A cautionary tale, Information Processing Letters, vol.65, issue.1, pp.7-10, 1998.
DOI : 10.1016/S0020-0190(97)00180-4

M. Tuengerthal and C. Kiel, Implementing a unification algorithm for protocol analysis with XOR Available from http, 2006.