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
CNRS - Centre National de la Recherche Scientifique : UMR8643, Inria Saclay - Ile de France, ENS Cachan - École normale supérieure - Cachan, LSV - Laboratoire Spécification et Vérification [Cachan]
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 metadatas

Cited literature [31 references]  Display  Hide  Download

https://hal.inria.fr/inria-00578855
Contributor : Florent Jacquemard <>
Submitted on : Tuesday, March 22, 2011 - 2:57:47 PM
Last modification on : Thursday, February 7, 2019 - 5:29:25 PM
Long-term archiving on : Thursday, June 23, 2011 - 2:46:26 AM

File

DJ-jar05.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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. ⟨http://www.springerlink.com/content/g1504263136433v6/⟩. ⟨10.1007/s10817-005-9017-7⟩. ⟨inria-00578855⟩

Share

Metrics

Record views

305

Files downloads

176