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

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