An NP decision procedure for protocol insecurity with XOR

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

zbMATH Keywords

ComplexityXORVerificationSecurityProtocols

Mathematics Subject Classification ID

Cryptography (94A60) Data encryption (aspects in computer science) (68P25)

Related Items (27)

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

This page was built for publication: An NP decision procedure for protocol insecurity with XOR