  There is a large amount of work dedicated to the formal verification of
security protocols. In this paper, we revisit and extend the NP-complete
decision procedure for a bounded number of sessions. We use a, now standard,
deducibility constraints formalism for modeling security protocols. Our first
contribution is to give a simple set of constraint simplification rules, that
allows to reduce any deducibility constraint system to a set of solved forms,
representing all solutions (within the bound on sessions).
  As a consequence, we prove that deciding the existence of key cycles is
NP-complete for a bounded number of sessions. The problem of key-cycles has
been put forward by recent works relating computational and symbolic models.
The so-called soundness of the symbolic model requires indeed that no key cycle
(e.g., enc(k,k)) ever occurs in the execution of the protocol. Otherwise,
stronger security assumptions (such as KDM-security) are required.
  We show that our decision procedure can also be applied to prove again the
decidability of authentication-like properties and the decidability of a
significant fragment of protocols with timestamps.
