Stéphanie Delaune and Florent Jacquemard. A Theory of Dictionary Attacks and its Complexity. In Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW'04), pp. 2–15, IEEE Computer Society Press, Asilomar, Pacific Grove, California, USA, June 2004.
We consider the problem of automating proofs of cryptographic protocols when some data, like poorly chosen passwords, can be guessed by dictionary attacks. First, we define a theory of these attacks: we introduce an inference system modeling the guessing capabilities of an intruder. This system extends the classical Dolev-Yao rules. Using proof rewriting techniques, we show a locality lemma for our inference system which yields the PTIME-completeness of the deduction problem.
This result is lifted to the simultaneous solving of intruder deduction constraints with variables. Constraint solving is the basis of a NP algorithm for the protocol insecurity problem in the presence of dictionary attacks, assuming a bounded number of sessions. This extends the classical NP-completeness result for the Dolev-Yao model.
We illustrate the procedure with examples of published protocols. The model and decision algorithm have been validated on some examples in a prototype implementation.
@inproceedings{dj-csfw2004,
abstract = {We consider the problem of automating proofs of
cryptographic protocols when some data, like poorly
chosen passwords, can be guessed by dictionary
attacks. First, we define a theory of these attacks:
we introduce an inference system modeling the
guessing capabilities of an intruder. This system
extends the classical Dolev-Yao rules. Using proof
rewriting techniques, we show a locality lemma for
our inference system which yields the
PTIME-completeness of the deduction problem.\par This
result is lifted to the simultaneous solving of
intruder deduction constraints with variables.
Constraint solving is the basis of a NP algorithm for
the protocol insecurity problem in the presence of
dictionary attacks, assuming a bounded number of
sessions. This extends the classical NP-completeness
result for the Dolev-Yao model.\par We illustrate the
procedure with examples of published protocols. The
model and decision algorithm have been validated on
some examples in a prototype implementation.},
address = {Asilomar, Pacific Grove, California, USA},
author = {Delaune, St{\'e}phanie and Jacquemard, Florent},
booktitle = {{P}roceedings of the 17th {IEEE} {C}omputer
{S}ecurity {F}oundations {W}orkshop ({CSFW}'04)},
month = jun,
pages = {2-15},
publisher = {{IEEE} Computer Society Press},
title = {A Theory of Dictionary Attacks and its Complexity},
year = {2004},
acronym = {{CSFW}'04},
nmonth = {6},
longpdf = {https://people.irisa.fr/Stephanie.Delaune/PUBLICATIONS/rr-lsv-2004-1.rr.pdf},
}