A Syntactic Criterion for Injectivity of Authentication Protocols
Cas J. F. Cremers, Sjouke Mauw, E.P. de Vink · Electronic Notes in Theoretical Computer Science · 2005
Injectivity is essential when studying the correctness of authentication protocols, because noninjective 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.