An NP decision procedure for protocol insecurity with XOR
From MaRDI portal
Publication:557799
DOI10.1016/J.TCS.2005.01.015zbMATH Open1068.68057OpenAlexW2013689938MaRDI QIDQ557799FDOQ557799
Authors: Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani 
Publication date: 30 June 2005
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00071889
Recommendations
- Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
- On the Automatic Analysis of Recursive Security Protocols with XOR
- Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach
- Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive Or
- Automatic Analysis of the Security of XOR-Based Key Management Schemes
Cites Work
- An attack on a recursive authentication protocol. A cautionary tale
- Using encryption for authentication in large networks of computers
- Title not available (Why is that?)
- Title not available (Why is that?)
- On the security of public key protocols
- Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
- FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
- An NP decision procedure for protocol insecurity with XOR
- An attack on the Needham-Schroeder public-key authentication protocol
- Title not available (Why is that?)
- Title not available (Why is that?)
- Deciding the security of protocols with commuting public key encryption
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (37)
- Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
- Intruder deduction problem for locally stable theories with normal forms and inverses
- Automated Deduction – CADE-20
- On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography
- Deciding knowledge in security protocols under equational theories
- Automatic verification of security protocols in the symbolic model: the verifier ProVerif
- Title not available (Why is that?)
- Bounded memory protocols
- Protocol insecurity with a finite number of sessions and a cost-sensitive guessing intruder is NP-complete
- Crooked indifferentiability of enveloped XOR revisited
- A Proof Theoretic Analysis of Intruder Theories
- A method for symbolic analysis of security protocols
- On the semantics of Alice \& Bob specifications of security protocols
- YAPA: A Generic Tool for Computing Intruder Knowledge
- Decidability and combination results for two notions of knowledge in security protocols
- Decision procedures for the security of protocols with probabilistic encryption against offline dictionary attacks
- An NP decision procedure for protocol insecurity with XOR
- Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions
- Bounded memory Dolev-Yao adversaries in collaborative systems
- Automatic Analysis of the Security of XOR-Based Key Management Schemes
- A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
- Challenges in the Automated Verification of Security Protocols
- Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
- Low-memory attacks against two-round Even-Mansour using the 3-XOR problem
- Computing knowledge in equational extensions of subterm convergent theories
- Symbolic protocol analysis for monoidal equational theories
- On the Automatic Analysis of Recursive Security Protocols with XOR
- Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case
- Efficient representation of the attacker's knowledge in cryptographic protocols analysis
- The gap between promise and reality: on the insecurity of XOR arbiter PUFs
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Limits of the cryptographic realization of Dolev-Yao-style XOR
- Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables
- Satisfiability of general intruder constraints with and without a set constructor
- Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach
- Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive Or
- Deciding knowledge in security protocols under some e-voting theories
This page was built for publication: An NP decision procedure for protocol insecurity with XOR
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q557799)
