Game-Based Analysis of Denial-of-Service Prevention Protocols

Availability is a critical issue in modern distributed systems. While many techniques and protocols for preventing denial of service (DoS) attacks have been proposed and deployed in recent years, formal methods for analyzing and proving them correct have not kept up with the state of the art in DoS prevention. This paper proposes a new protocol for preventing malicious bandwidth consumption, and demonstrates how game-based formal methods can be successfully used to verify availability-related security properties of network protocols. We describe two classes of DoS attacks aimed at bandwidth consumption and resource exhaustion, respectively. We then propose our own protocol, based on a variant of client puzzles, to defend against bandwidth consumption, and use the JFKr key exchange protocol as an example of a protocol that defends against resource exhaustion attacks. We specify both protocols as alternating transition systems (ATS), state their security properties in alternatingtime te...

• Type: Conference
• Year: 2005
• Where: CSFW
• Authors: Ajay Mahimkar, Vitaly Shmatikov
• Keywords: Bandwidth Consumption, CSFW 2005, Formal Methods, Resource Exhaustion, Security Privacy