Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Journal articles

Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks

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 formal automatic verification of cryptographic protocols when some data, like poorly chosen passwords, can be guessed by dictionary attacks. First, we define a theory of these attacks and propose an inference system modeling the deduction capabilities of an intruder. This system extends a set of well-studied deduction rules for symmetric and public key encryption, often called Dolev–Yao rules, with the introduction of a probabilistic encryption operator and guessing abilities for the intruder. Then, we show that the intruder deduction problem in this extended model is decidable in PTIME. The proof is based on a locality lemma for our inference system. This first result yields to an NP decision procedure for the protocol insecurity problem in the presence of a passive intruder. In the active case, the same problem is proved to be NP-complete: we give a procedure for simultaneously solving symbolic constraints with variables that represent intruder deductions. We illustrate the procedure with examples of published protocols and compare our model to other recent formal definitions of dictionary attacks.
Document type :
Journal articles
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download
Contributor : Florent Jacquemard Connect in order to contact the contributor
Submitted on : Tuesday, March 22, 2011 - 2:57:47 PM
Last modification on : Thursday, January 20, 2022 - 4:12:11 PM
Long-term archiving on: : Thursday, June 23, 2011 - 2:46:26 AM


Files produced by the author(s)



Stéphanie Delaune, Florent Jacquemard. Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks. Journal of Automated Reasoning, Springer Verlag, 2006, 36 (1-2), pp.85-124. ⟨10.1007/s10817-005-9017-7⟩. ⟨inria-00578855⟩



Record views


Files downloads