Current techniques for the formal modeling analysis of DoS attacks do
not adequately deal with \textit{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 \textit{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.