Deciding security properties for cryptographic protocols. Application to key cycles. - Archive ouverte HAL Access content directly
Journal Articles ACM Transactions on Computational Logic Year : 2010

Deciding security properties for cryptographic protocols. Application to key cycles.

(1) , (2) , (3)
1
2
3

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.

Dates and versions

inria-00525775 , version 1 (12-10-2010)

Identifiers

Cite

Hubert Comon-Lundh, Véronique Cortier, Eugen Zalinescu. Deciding security properties for cryptographic protocols. Application to key cycles.. ACM Transactions on Computational Logic, 2010, 11 (2), pp.Article 9. ⟨10.1145/1656242.1656244⟩. ⟨inria-00525775⟩
153 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More