Protocol insecurity with a finite number of sessions and a cost-sensitive guessing intruder is NP-complete

Guessing attacks in security protocols arise when honest agents make use of data easily guessable by an intruder, such as passwords generated from a small dictionary. A way to model such attacks is to formalize a Dolev-Yao style model with inference rules that capture the additional capabilities of the intruder concerning guessable data. In this paper, we formalize a cost-sensitive intruder deduction system where information is available at a cost. The intruder may apply standard operations to deduce new messages from his current knowledge, or invoke an oracle rule that allows him to get hold of data that was previously unknown to him. Our system manipulates data items by means of inference rules and uses labels to keep track of the costs associated to the application of each rule. This allows us to answer the question of what is the cost of deducing a particular data that was meant to remain a secret between honest protocol participants. We also investigate the complexity of this quantitative insecurity problem and show that it is NP-complete in the case of a finite number of protocol sessions.