Skip to Main content Skip to Navigation
Conference papers

A Theory of Dictionary Attacks and its Complexity

Stéphanie Delaune 1 Florent Jacquemard 2
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
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. 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download
Contributor : Florent Jacquemard <>
Submitted on : Tuesday, March 22, 2011 - 11:17:07 PM
Last modification on : Thursday, July 2, 2020 - 5:26:03 PM
Long-term archiving on: : Thursday, June 23, 2011 - 3:00:00 AM


Files produced by the author(s)


  • HAL Id : inria-00579014, version 1



Stéphanie Delaune, Florent Jacquemard. A Theory of Dictionary Attacks and its Complexity. 17th IEEE Computer Security Foundations Workshop (CSFW), Jun 2004, Asilomar, Pacific Grove, United States. pp.2-15. ⟨inria-00579014⟩



Record views


Files downloads