A number of new cryptographic protocols are being designed to
secure applications such as video-conferencing and electronic
voting. Many of them rely upon cryptographic functions with
complex algebraic properties that must be accounted for in order
to be correctly analyzed by automated tools. Maude-NPA is a
cryptographic protocol analysis tool based on narrowing and typed
equational unification which takes into account these algebraic
properties. It has already been used to analyze protocols
involving bounded associativity, modular exponentiation, and
exclusive-or. All of the above can be handled by the same general
\emph{variant}-based equational unification technique. However,
there are important properties, in particular homomorphic
encryption, that cannot be handled by variant-based unification
in the same way. In these cases the best available approach is to
implement specialized unification algorithms and combine them
within a modular framework.  In this paper we describe how we
apply this approach within Maude-NPA, with respect to encryption
homomorphic over a free operator.  We also describe the use of
Maude-NPA to analyze several protocols using such an encryption
operation.  To the best of our knowledge, this is the first
implementation of homomorphic encryption of any sort in a tool
for verifying the security of a protocol in the presence of
active attackers.