Modelling Denial of Service Attacks on JFK with Meadow's Cost-Based Framework

We present the first detailed application of Meadows’s cost-based modelling framework to the analysis of JFK, an Internet key agreement protocol. The analysis identifies two denial of service attacks against the protocol that are possible when an attacker is willing to reveal the source IP address. The first attack was identified through direct application of a cost-based modelling framework, while the second was only identified after considering coordinated attackers. Finally, we demonstrate how the inclusion of client puzzles in the protocol can improve denial of service resistance against both identified attacks.