Stéphanie Delaune. An Undecidability Result for AGh. Theoretical Computer Science, 368(1-2):161–167, Elsevier Science Publishers, December 2006.
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 satisfaisability of symbolic deducibility 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].
@article{delaune-tcs06,
abstract = {We present an undecidability result for the
verification of security protocols. Since the
\emph{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 \emph{Abelian
groups} theory in combination with the homomorphism
axiom. We show that satisfaisability of symbolic
deducibility 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{\"{o}}bner
bases, J.~ACM~40(3) (1993)~477-503].},
author = {Delaune, St{\'e}phanie},
OPTDOI = {10.1016/j.tcs.2006.08.018},
journal = {Theoretical Computer Science},
month = dec,
number = {1-2},
pages = {161-167},
publisher = {Elsevier Science Publishers},
title = {An Undecidability Result
for~{AG}h},
volume = {368},
year = {2006},
nmonth = {12},
lsv-category = {jour},
wwwpublic = {public and ccsb},
}