Deciding security properties for cryptographic protocols. Application to key cycles

There has been a growing interest in applying formal methods for validating cryptographic protocols and many results have been obtained. In this paper, we re-investigate and extend the NP-complete decision procedure for a bounded number of sessions of Rusinowitch and Turuani. In this setting, constraint systems are now a standard for modeling security protocols. We provide a generic approach to decide general security properties by showing that any constraint system can be transformed in (possibly several) much simpler constraint systems that are called \emph{solved forms}. As a consequence, we prove that deciding the existence of key cycles is NP-complete for a bounded number of sessions. Indeed, many recent results are concerned with interpreting proofs of security done in symbolic models in the more detailed models of computational cryptography. In the case of symmetric encryption, these results stringently demand that no key cycle (e.g. $\{k\}_k$) can be produced during the execution of protocols. We show that our decision procedure can also be applied to reprove decidability of authentication-like properties and decidability of a significant existing fragment of protocols with timestamps.