Abstract:

A Formalization of Off-Line Guessing for Security Protocol Analysis

Paul Hankes Drielsma and Sebastian Mödersheim and Luca Viganò


Guessing, or dictionary, attacks arise when an intruder exploits the fact that certain 
data like passwords may have low entropy, i.e. stem from a small set of values. In the 
case of off-line guessing, in particular, the intruder may employ guessed values to 
analyze the messages he has observed. Previous attempts at formalizing off-line guessing 
consist of extending a Dolev-Yao-style intruder model with inference rules to capture the 
additional capabilities of the intruder concerning guessable messages. While it is easy 
to convince oneself that the proposed rules are correct, in the sense that an intruder 
can actually perform such ``guessing steps'', it is difficult to see whether such a 
system of inference rules is complete in the sense that it captures all the kinds of 
attacks that we would intuitively call ``guessing attacks''. Moreover, the proposed 
systems are specialized to particular sets of cryptographic primitives and intruder 
capabilities. As a consequence, these systems are helpful to discover some off-line 
guessing attacks but are not fully appropriate for formalizing what off-line guessing 
precisely means and verifying that a given protocol is not vulnerable to such guessing 
attacks.In this paper, we give a formalization of off-line guessing by defining a 
deduction system that is uniform and general in that it is independent of the overall 
protocol model and of the details of the considered intruder model, i.e.~cryptographic 
primitives, algebraic properties, and intruder capabilities.