Deciding security properties for cryptographic protocols. Application to key cycles
| dc.creator | Comon-Lundh, Hubert | |
| dc.creator | Cortier, Véronique | |
| dc.creator | Zalinescu, Eugen | |
| dc.date | 2007-08-27 | |
| dc.date | 2009-03-20 | |
| dc.date.accessioned | 2026-07-07T12:53:57Z | |
| dc.date.available | 2026-07-07T12:53:57Z | |
| dc.description | 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. | |
| dc.description | revised version (corrected small mistakes, improved presentation); to be published in ACM Transactions on Computational Logic; 39 pages | |
| dc.identifier | https://arxiv.org/abs/0708.3564 | |
| dc.identifier | http://arxiv.org/abs/0708.3564 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/223764 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | Cryptography and Security | |
| dc.subject | F.3.1 | |
| dc.title | Deciding security properties for cryptographic protocols. Application to key cycles | |
| dc.type | text |