Model checking approach to real-time aspects of denial-of-service attack

Abstract

Vulnerability of communication protocols can cause several kinds of attacks, which cause significant damage to systems connected to the Internet. Denial-of-service attack (DoS attack) is an instance of them. Analysis of resistance against DoS attacks is considered as significant. We previously proposed a formal framework for DoS attack resistance, the spice calculus. In this paper, we develop a method for analyzing communication protocols from the aspect of DoS attack resistance. In this method, we first formalize a communication protocol in terms of the spice calculus. Then we translate expressions of the spice calculus into timed automata and analyze them using the real-time model checker UPPAAL. We explain the method by showing an example of a simple communication protocol. © 2012 Springer-Verlag Berlin Heidelberg.