An NP decision procedure for protocol insecurity with XOR
From MaRDI portal
Publication:557799
DOI10.1016/j.tcs.2005.01.015zbMath1068.68057OpenAlexW2013689938MaRDI QIDQ557799
Michaël Rusinowitch, Mathieu Turuani, Ralf Küsters, Yannick Chevalier
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
Related Items
Deciding knowledge in security protocols under equational theories, On the semantics of Alice \& Bob specifications of security protocols, A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, Decidability and combination results for two notions of knowledge in security protocols, Bounded memory Dolev-Yao adversaries in collaborative systems, Challenges in the Automated Verification of Security Protocols, Computing knowledge in equational extensions of subterm convergent theories, Efficient representation of the attacker's knowledge in cryptographic protocols analysis, Satisfiability of general intruder constraints with and without a set constructor, Intruder deduction problem for locally stable theories with normal forms and inverses, Symbolic protocol analysis for monoidal equational theories, Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically, Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach, An NP decision procedure for protocol insecurity with XOR, A method for symbolic analysis of security protocols, Unnamed Item, On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography, A Proof Theoretic Analysis of Intruder Theories, 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, YAPA: A Generic Tool for Computing Intruder Knowledge, Deciding knowledge in security protocols under some e-voting theories, Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif, Bounded memory protocols, Limits of the Cryptographic Realization of Dolev-Yao-Style XOR
Cites Work
- An attack on a recursive authentication protocol. A cautionary tale
- An NP decision procedure for protocol insecurity with XOR
- An attack on the Needham-Schroeder public-key authentication protocol
- Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
- On the security of public key protocols
- Using encryption for authentication in large networks of computers
- FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
