Model-Checking DoS Amplification for VoIP Session Initiation

Published in European Symposium on Research in Computer Security, Springer, LNCS 5789, pp 390-405, 2009

Ravinder Shankesi, Musab A. Alturki, Ralf Sasse, Carl A. Gunter and José Meseguer

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 model-checking 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.