Efficient general AGH-unification

General E-unification is an important tool in cryptographic protocol analysis, where the equational theory E represents properties of the cryptographic algorithm, and uninterpreted function symbols represent other functions. The property of a homomorphism over an Abelian group is common in encryption algorithms such as RSA. The general E-unification problem in this theory is NP-complete, and existing algorithms are highly nondeterministic. We give a mostly deterministic set of inference rules for solving general E-unification modulo a homomorphism over an Abelian group, and prove that it is sound, complete and terminating. These inference rules have been implemented in Maude, and will be incorporated into the Maude-NRL Protocol Analyzer (Maude-NPA).