Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
From MaRDI portal
Publication:1874404
DOI10.1016/S0304-3975(02)00490-5zbMath1042.68009MaRDI QIDQ1874404
Michaël Rusinowitch, Mathieu Turuani
Publication date: 25 May 2003
Published in: Theoretical Computer Science (Search for Journal in Brave)
Related Items
From Security Protocols to Pushdown Automata, The Complexity of Disjunction in Intuitionistic Logic, Model Checking Security Protocols, Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols, An undecidability result for AGh, A (restricted) quantifier elimination for security protocols, Decidability issues for extended ping-pong protocols, Decision procedures for the security of protocols with probabilistic encryption against offline dictionary attacks, Modular verification of protocol equivalence in the presence of randomness, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, Emerging Issues and Trends in Formal Methods in Cryptographic Protocol Analysis: Twelve Years Later, Active Linking Attacks, Verifying Cryptographic Protocols with Subterms Constraints, Deciding Knowledge in Security Protocols for Monoidal Equational Theories, Decidability of equivalence of symbolic derivations, Computing knowledge in security protocols under convergent equational theories, Decidability and combination results for two notions of knowledge in security protocols, Deducibility constraints and blind signatures, Bounded memory Dolev-Yao adversaries in collaborative systems, Challenges in the Automated Verification of Security Protocols, Protocol insecurity with a finite number of sessions and a cost-sensitive guessing intruder is NP-complete, Bounding messages for free in security protocols -- extension to various security properties, Efficient representation of the attacker's knowledge in cryptographic protocols analysis, Transducer-based analysis of cryptographic protocols, Intruder deducibility constraints with negation. Decidability and application to secured service compositions, Satisfiability of general intruder constraints with and without a set constructor, Symbolic protocol analysis for monoidal equational theories, Hierarchical combination of intruder theories, Multi-attacker protocol validation, An NP decision procedure for protocol insecurity with XOR, A method for symbolic analysis of security protocols, Automating Security Analysis: Symbolic Equivalence of Constraint Systems, Computing Knowledge in Security Protocols under Convergent Equational Theories, A decidable class of security protocols for both reachability and equivalence properties, Deciding Security for Protocols with Recursive Tests, Safely Composing Security Protocols, Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables, Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case, Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions, Deciding knowledge in security protocols under some e-voting theories, Safely composing security protocols, Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model, Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif, Bounded memory protocols, On the symbolic reduction of processes with cryptographic functions., Explicit Randomness is not Necessary when Modeling Probabilistic Encryption, Computational Soundness of Symbolic Analysis for Protocols Using Hash Functions
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Secure networking - CQRE [Secure '99. International exhibition and congress. Düsseldorf, Germany, November 30--December 2, 1999. Proceedings]
- The NRL Protocol Analyzer: An Overview
- On the security of public key protocols
