Deciding security properties for cryptographic protocols. Application to key cycles

Deciding security properties for cryptographic protocols. Application to key cycles. Hubert Comon-Lundh, Véronique Cortier, and Eugen Zălinescu. ACM Transactions on Computational Logic, 11(2), ACM Press, January 2010.

Download

[PDF] [HTML]

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).
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.

BibTeX

@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},
}