Formal Analysis of DNS Attacks and Their Countermeasures Using Probabilistic Model Checking

Tushar Deshpande1, Panagiotis Katsaros2, and Scott A. Smolka1

1Department of Computer Science, Stony Brook University, Stony Brook, NY 11794-4400, USA
E-mail: {tushard, sas}
2Department of Informatics, Aristotle University of Thessaloniki, Thessaloniki, 54124, Greece
Email: {katsaros}


Abstract - The Domain Name System (DNS) is an internet-wide, hierarchical naming system used to translate domain names into physical IP addresses. Any disruption of the service DNS provides can have serious consequences. We present a formal analysis of two notable threats to DNS, namely cache poisoning and bandwidth amplification, and the countermeasures designed to prevent their occurrence. Our analysis of these attacks and their countermeasures is given in the form of a cost-benefit analysis, and is based on probabilistic model checking of Continuous-Time Markov Chains. We use CTMCs to model the race between legitimate and malicious traffic in a DNS server under attack. Countermeasure costs and benefits are quantified in terms of probabilistic reachability and reward properties, which are evaluated over all possible execution paths. The results of our analysis support substantive conclusions about the relative effectiveness of the different countermeasures under varying operating conditions. We also validate the criticism that the DNS security extensions devised to eliminate cache poisoning render DNS more vulnerable to bandwidth amplification attacks.

Download Model Code for DNS Cache-Poisoning Attack
Model Code Download
CSL Properties File Download
Groovy Script to Determine Countermeasure Parameters for RDQ Download
Input Data for the Groovy Script Download

Download Model Code for DNS Bandwidth Amplification Attack (BAA)
BAA without any countermeasure (No-fix) Download
BAA with Filtering (FTR) Download
BAA with Random Drops (RND) Download
BAA with Aggressive Retries (AGR) Download
BAA with Aggressive Retries and Filtering (AGF) Download
BAA with Aggressive Retries and Random Drops (RDR) Download
CSL Properties File Download

PRISM model checker is needed to run the models files. More information about PRISM can be found at
Groovy interpreter is required to run the groovy script. More information about Groovy scripting language, please visit