There is a growing interest in formal methods and tools to
analyze cryptographic protocols \emph{modulo} algebraic
properties of their underlying cryptographic functions. It is
well-known that an intruder who uses algebraic equivalences of
such functions can mount attacks that would be impossible if the
cryptographic functions did not satisfy such equivalences. In
practice, however, protocols use a collection of well-known
functions, whose algebraic properties can naturally be grouped
together as a union of theories $E_{1} \cup \ldots \cup E_{n}$.
Reasoning symbolically modulo the algebraic properties $E_{1}
\cup \ldots \cup E_{n}$ requires performing $(E_{1} \cup \ldots
\cup E_{n})$-unification. However, even if a unification
algorithm for each individual $E_{i}$ is available, this requires
combining the existing algorithms by methods that are highly
non-deterministic and have high computational cost. In this work
we present an alternative method to obtain unification algorithms
for combined theories based on \emph{variant narrowing}.
Although variant narrowing is less efficient at the level of a
single theory $E_{i}$, it does not use any costly combination
method. Furthermore, it does not require that each $E_{i}$ has a
dedicated unification algorithm in a tool implementation. We
illustrate the use of this method in the Maude-NPA tool by means
of a well-known protocol requiring the combination of three
distinct equational theories.
\begin{keywords}
Cryptographic protocol verification,
equational unification,
variants,
exclusive or,
narrowing
\end{keywords}