TY - JOUR
T1 - Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol
AU - AlTurki, Musab
AU - Meseguer, José
AU - Gunter, Carl A.
N1 - Funding Information:
This work was supported in part by NSF CNS05-5170 CNS05-09268 CNS05-24695, NSF CNS 07-16421, NSF CNS 07-16638, ONR N00014-04-1-0562 N00014-02-1-0715, DHS 2006-CS-001-000001 and a grant from the MacArthur Foundation. The views expressed are those of the authors only.
PY - 2009/3/28
Y1 - 2009/3/28
N2 - The Adaptive Selective Verification (ASV) protocol was recently proposed as an effective and efficient DoS countermeasure within the shared channel model, in which clients and attackers probabilistically share communication bandwidth with the server. ASV has been manually shown to satisfy some desirable availability and bandwidth consumption properties. Due to the probabilistic nature of the protocol and its underlying attacker model, it is intrinsically difficult to build a faithful model of the protocol with which one may automatically verify its properties. This paper fills the gap between manual analysis and simulation-based experimental analysis of ASV, through automated formal analysis. We describe a formal model of ASV using probabilistic rewrite theories, implemented in a probabilistic extension of Maude, and show how it can be used to formally verify various characteristics of ASV through automated statistical quantitative model checking analysis techniques. In particular, we formally verify ASV's connection confidence theorem and a slightly more general bandwidth consumption theorem of ASV. This is followed by a statistical comparison of ASV with non-adaptive selective verification protocols. We conclude with remarks on possible further development and future work.
AB - The Adaptive Selective Verification (ASV) protocol was recently proposed as an effective and efficient DoS countermeasure within the shared channel model, in which clients and attackers probabilistically share communication bandwidth with the server. ASV has been manually shown to satisfy some desirable availability and bandwidth consumption properties. Due to the probabilistic nature of the protocol and its underlying attacker model, it is intrinsically difficult to build a faithful model of the protocol with which one may automatically verify its properties. This paper fills the gap between manual analysis and simulation-based experimental analysis of ASV, through automated formal analysis. We describe a formal model of ASV using probabilistic rewrite theories, implemented in a probabilistic extension of Maude, and show how it can be used to formally verify various characteristics of ASV through automated statistical quantitative model checking analysis techniques. In particular, we formally verify ASV's connection confidence theorem and a slightly more general bandwidth consumption theorem of ASV. This is followed by a statistical comparison of ASV with non-adaptive selective verification protocols. We conclude with remarks on possible further development and future work.
KW - Adaptive Selective Verification
KW - DoS
KW - Formal Statistical Analysis
KW - Maude
KW - Probabilistic Rewrite Theories
KW - Rewriting Logic
UR - http://www.scopus.com/inward/record.url?scp=62849120147&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=62849120147&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2009.02.069
DO - 10.1016/j.entcs.2009.02.069
M3 - Article
AN - SCOPUS:62849120147
VL - 234
SP - 3
EP - 18
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
SN - 1571-0661
IS - C
ER -