  We consider the problem of the unification modulo an equational theory ACh,
which consists of a function symbol $h$ that is homomorphic over an
associative-commutative operator $+$. Since the unification modulo ACh theory
is undecidable, we define a variant of the problem called \textit{bounded ACh
unification}. In this bounded version of ACh unification, we essentially bound
the number of times $h$ can be applied to a term recursively, and only allow
solutions that satisfy this bound. There is no bound on the number of
occurrences of $h$ in a term, and the $+$ symbol can be applied an unlimited
number of times. We give inference rules for solving the bounded version of the
problem and prove that the rules are sound, complete, and terminating. We have
implemented the algorithm in Maude and give experimental results. We argue that
this algorithm is useful in cryptographic protocol analysis.

Logic in Computer Science