A Probabilistic Attacker Model for Quantitative Verification of DoS Security Threats