An NP decision procedure for protocol insecurity with XOR
- 22 December 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10436871,p. 261-270
- https://doi.org/10.1109/lics.2003.1210066
Abstract
We provide a method for deciding the insecurity of cryptographic protocols in presence of the standard Dolev-Yao intruder (with a finite number of sessions) extended with so-called oracle rules, i.e., deduction rules that satisfy certain conditions. As an instance of this general framework, we ascertain that protocol insecurity is in NP for an intruder that can exploit the properties of the XOR operator. This operator is frequently used in cryptographic protocols but cannot be handled in most protocol models. An immediate consequence of our proof is that checking whether a message can be derived by an intruder (using XOR) is in P. We also apply our framework to an intruder that exploits properties of certain encryption modes such as cipher block chaining (CBC).Keywords
This publication has 14 references indexed in Scilit:
- Athena: a new efficient automatic checker for security protocol analysisPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Mechanized proofs for a recursive authentication protocolPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- On the Decidability of Cryptographic Protocols with Open-Ended Data StructuresPublished by Springer Nature ,2002
- Constraint solving for bounded-process cryptographic protocol analysisPublished by Association for Computing Machinery (ACM) ,2001
- Protocol insecurity with finite number of sessions is NP-completePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2001
- Computing symbolic models for verifying cryptographic protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2001
- Lazy Infinite-State Analysis of Security ProtocolsPublished by Springer Nature ,1999
- An attack on a recursive authentication protocol A cautionary taleInformation Processing Letters, 1998
- Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDRPublished by Springer Nature ,1996
- An attack on the Needham-Schroeder public-key authentication protocolInformation Processing Letters, 1995