An undecidability result for AGh

Citations of this article
Mendeley users who have this article in their library.


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]. © 2006 Elsevier B.V. All rights reserved.




Delaune, S. (2006). An undecidability result for AGh. Theoretical Computer Science, 368(1–2), 161–167.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free