Narrowing is a well-known complete procedure for equational
$E$-unification when $E$ can be decomposed as a union $E = \Delta
\uplus B$ with $B$ a set of axioms for which a finitary unification
algorithm exists, and $\Delta$ a set of confluent, terminating, and
$B$-coherent rewrite rules. However, when $B\not= \emptyset$,
effective narrowing strategies such as basic narrowing easily fail to
be complete and cannot be used. This poses two challenges to
narrowing-based equational unification: (i) finding effective
narrowing strategies that are complete modulo $B$ under mild
assumptions on $B$, and (ii) finding sufficient conditions under which
such narrowing strategies yield \emph{finitary} $E$-unification
algorithms. Inspired by Comon and Delaune's notion of $E$-variant for
a term, we propose a new narrowing strategy called \emph{variant
narrowing} that has a search space potentially much smaller than full
narrowing, is complete, and yields a finitary $E$-unification
algorithm when $E$ has the finite variant property. We also discuss
applications to symbolic reachability analysis of concurrent systems
specified as rewrite theories, and in particular to the formal
analysis of cryptographic protocols modulo the algebraic properties of
the underlying cryptographic functions.