Stéphanie Delaune and Florent Jacquemard. Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks. Journal of Automated Reasoning, 36(1-2):85–124, Springer, January 2006.
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 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 which represent intruder deductions. We illustrate the procedure with examples of published protocols and compare our model to other recent formal definitions of dictionary attacks.
@article{dj-jar05,
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 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 which
represent intruder deductions. We illustrate the
procedure with examples of published protocols and
compare our model to other recent formal definitions
of dictionary attacks.},
author = {Delaune, St{\'e}phanie and Jacquemard, Florent},
OPTDOI = {10.1007/s10817-005-9017-7},
journal = {Journal of Automated Reasoning},
month = jan,
number = {1-2},
pages = {85-124},
publisher = {Springer},
title = {Decision Procedures for the Security of Protocols
with Probabilistic Encryption against Offline
Dictionary Attacks},
volume = {36},
year = {2006},
nmonth = {1},
lsv-category = {jour},
wwwpublic = {public and ccsb},
}