Customizing protocol specifications for detecting resource exhaustion and guessing attacks

Abstract

Model checkers for security protocols often focus on basic properties, such as confidentiality or authentication, using a standard model of the Dolev-Yao intruder. In this paper, we explore how to model other attacks, notably guessing of secrets and denial of service by resource exhaustion, using the AVANTSSAR platform with its modelling language ASLan. We do this by adding custom intruder deduction rules and augmenting protocol transitions with constructs that keep track of these attacks. We compare several modelling variants and find that writing deductions in ASLan as Horn clauses rather than transitions using rewriting rules is crucial for verification performance. Providing automated tool support for these attacks is important since they are often neglected by protocol designers and open up other attack possibilities. © 2011 Springer-Verlag Berlin Heidelberg.