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 = {http://people.irisa.fr/Stephanie.Delaune/PUBLICATIONS/rr-lsv-2004-1.rr.pdf}, }