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-5zbMATH Open1042.68009MaRDI QIDQ1874404FDOQ1874404
Authors: Michaël Rusinowitch, Mathieu Turuani 
Publication date: 25 May 2003
Published in: Theoretical Computer Science (Search for Journal in Brave)
Recommendations
- Protocol insecurity with a finite number of sessions and a cost-sensitive guessing intruder is NP-complete
- Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption
- Automated Deduction – CADE-20
- An NP decision procedure for protocol insecurity with XOR
- The practice of cryptographic protocol verification
Cites Work
- The NRL Protocol Analyzer: An Overview
- Title not available (Why is that?)
- On the security of public key protocols
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Secure networking - CQRE [Secure] '99. International exhibition and congress. Düsseldorf, Germany, November 30--December 2, 1999. Proceedings
Cited In (55)
- DeepSec: deciding equivalence properties for security protocols -- improved theory and practice
- Decidability of equivalence of symbolic derivations
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- The complexity of disjunction in intuitionistic logic
- Title not available (Why is that?)
- Deciding security for protocols with recursive tests
- Multi-attacker protocol validation
- Active linking attacks
- From security protocols to pushdown automata
- Automatic verification of security protocols in the symbolic model: the verifier ProVerif
- Bounded memory protocols
- Protocol insecurity with a finite number of sessions and a cost-sensitive guessing intruder is NP-complete
- Emerging issues and trends in formal methods in cryptographic protocol analysis: twelve years later
- Computing Knowledge in Security Protocols under Convergent Equational Theories
- A method for symbolic analysis of security protocols
- Computer Science Logic
- A (restricted) quantifier elimination for security protocols
- Computing knowledge in security protocols under convergent equational theories
- Decidability and combination results for two notions of knowledge in security protocols
- Safely composing security protocols
- An undecidability result for AGh
- Decidability issues for extended ping-pong protocols
- Decision procedures for the security of protocols with probabilistic encryption against offline dictionary attacks
- On the symbolic reduction of processes with cryptographic functions.
- An NP decision procedure for protocol insecurity with XOR
- Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
- Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions
- Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption
- Bounded memory Dolev-Yao adversaries in collaborative systems
- Deducibility constraints and blind signatures
- Hierarchical combination of intruder theories
- Formalization in PVS of balancing properties necessary for proving security of the Dolev-Yao cascade protocol model
- Automating security analysis: symbolic equivalence of constraint systems
- Challenges in the Automated Verification of Security Protocols
- Deciding Key Cycles for Security Protocols
- Transducer-based analysis of cryptographic protocols
- Safely Composing Security Protocols
- Bounding messages for free in security protocols -- extension to various security properties
- Modular verification of protocol equivalence in the presence of randomness
- A decidable class of security protocols for both reachability and equivalence properties
- Computational soundness of symbolic analysis for protocols using hash functions
- Explicit randomness is not necessary when modeling probabilistic encryption
- Model Checking Security Protocols
- The practice of cryptographic protocol verification
- Symbolic protocol analysis for monoidal equational theories
- Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case
- Automated Deduction – CADE-20
- Efficient representation of the attacker's knowledge in cryptographic protocols analysis
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Verifying Cryptographic Protocols with Subterms Constraints
- 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
- Satisfiability of general intruder constraints with and without a set constructor
- Deciding knowledge in security protocols under some e-voting theories
- Deciding Knowledge in Security Protocols for Monoidal Equational Theories
Uses Software
This page was built for publication: Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1874404)
