An undecidability result for AGh

We present an undecidability result for the verification of security protocols. Since the perfect cryptography assumption is unrealistic for cryptographic primitives with visible algebraic properties, several recent works relax this assumption, allowing the intruder to exploit these properties. We are interested in the Abelian groups theory in combination with the homomorphism axiom. We show that the security problem for a bounded number of sessions (expressed by satisfiability of symbolic deductibility constraints) is undecidable, obtaining in this way the first undecidability result concerning a theory for which unification is known to be decidable [F. Baader, Unification in commutative theories, Hilbert's basis theorem, and Gröbner bases, J. ACM 40(3) (1993) 477–503].