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

10 years 5 months ago
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...
Ajay Mahimkar, Vitaly Shmatikov
Added 24 Jun 2010
Updated 24 Jun 2010
Type Conference
Year 2005
Where CSFW
Authors Ajay Mahimkar, Vitaly Shmatikov
Comments (0)