Deciding security properties for cryptographic protocols. application to key cycles

DOI10.1145/1656242.1656244MaRDI QIDQ2946596zbMATH OpenOpenAlexWikidataFDO

Authors Hubert Comon-Lundh, Véronique Cortier, Eugen Zălinescu

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0708.3564

zbMATH Keywords

verificationsecurity protocolsformal proofssymbolic constraints

Mathematics Subject Classification ID

Cryptography (94A60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60) Network protocols (68M12)

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

Recommendations

• Deciding Key Cycles for Security Protocols
• Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions
• CONCUR 2004 - Concurrency Theory
• Deciding security for protocols with recursive tests
• scientific article; zbMATH DE number 1759624

Cited in

(13)

• Deciding security for protocols with recursive tests
• A symbolic decision procedure for cryptographic protocols with time stamps
• Deducibility constraints and blind signatures
• Modeling and verifying ad hoc routing protocols
• A procedure for deciding symbolic equivalence between sets of constraint systems
• scientific article; zbMATH DE number 2202020 (Why is no real title available?)
• Automating security analysis: symbolic equivalence of constraint systems
• Deciding Key Cycles for Security Protocols
• CONCUR 2004 - Concurrency Theory
• Deciding the security of protocols with commuting public key encryption
• Intruder deducibility constraints with negation. Decidability and application to secured service compositions
• Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables
• SPEC: an equivalence checker for security protocols

This page was built for publication: Deciding security properties for cryptographic protocols. application to key cycles

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946596)