Deciding security properties for cryptographic protocols. application to key cycles

DOI10.1145/1656242.1656244zbMATH Open1351.94035arXiv0708.3564OpenAlexW2155993098WikidataQ130960630 ScholiaQ130960630MaRDI QIDQ2946596FDOQ2946596

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)

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.

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

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

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)

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
• Title not available (Why is that?)
• 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
• Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables
• Intruder deducibility constraints with negation. Decidability and application to secured service compositions
• 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)