A Syntactic Criterion for Injectivity of Authentication Protocols
C.J.F. Cremers, S. Mauw and E.P. de Vink

Injectivity is essential when studying the correctness of
authentication protocols, because non-injective protocols may suffer
from replay attacks. The standard ways of verifying injectivity either
make use of a counting argument, which only seems to be applicable in
a verification methodology based on model-checking, or draw
conclusions on the basis of the details of the data-model used.  We
propose and study a property, the loop property, that can be
syntactically verified and is sufficient to guarantee injectivity. Our
result is generic in the sense that it holds for a wide range of
security protocol models, and does not depend on the details of
message contents or nonce freshness.