@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@article{CCLZ-TOCL,
  author =        {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and
                   Z{\u{a}}linescu, Eugen},
  journal =       {ACM Transactions on Computational Logic},
  month =         jan,
  number =        {2},
  publisher =     {ACM Press},
  title =         {Deciding security properties for cryptographic
                   protocols. Application to key cycles},
  volume =        {11},
  year =          {2010},
  abstract =      {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 constraint 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 to a set of solved forms, representing all
                   solutions (within the bound on sessions).\par 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
                   (\textit{e.g.},~enc\((k, k)\)) ever occurs in the
                   execution of the protocol. Otherwise, stronger
                   security assumptions (such as KDM-security) are
                   required.\par 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.},
  doi =           {10.1145/1656242.1656244},
}