Model-Checking DoS Amplification for VoIP Session Initiation

Current techniques for the formal modeling analysis of DoS attacks do not adequately deal with amplification attacks that may target a complex distributed system as a whole rather than a specific server. Such threats have emerged for important applications such as the VoIP Session Initiation Protocol (SIP). We demonstrate a modelchecking technique for finding amplification threats using a strategy we call measure checking that checks for a quantitative assessment of attacker impact using term rewriting. We illustrate the effectiveness of this technique with a study of SIP. In particular, we show how to automatically find known attacks and verify that proposed patches for these attacks achieve their aim. Beyond this, we demonstrate a new amplification attack based on the compromise of one or more SIP proxies. We show how to address this threat with a protocol change and formally analyze the effectiveness of the new protocol against amplification attacks.

• Type: Conference
• Year: 2009
• Where: ESORICS
• Authors: Carl A. Gunter, José Meseguer, Musab AlTurki, Ralf Sasse, Ravinder Shankesi
• Keywords: Amplification Attacks, Amplification Threats, DoS Attacks, ESORICS 2009, Security Privacy