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], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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.
Type de document :
Article dans une revue
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〉
Liste complète des métadonnées

Littérature citée [31 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00578855
Contributeur : Florent Jacquemard <>
Soumis le : mardi 22 mars 2011 - 14:57:47
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : jeudi 23 juin 2011 - 02:46:26

Fichier

DJ-jar05.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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〉

Partager

Métriques

Consultations de la notice

252

Téléchargements de fichiers

120