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}, }