Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish (US)
Pages (from-to)3-18
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Volume234
Issue numberC
DOIs
StatePublished - Mar 28 2009

Keywords

  • Adaptive Selective Verification
  • DoS
  • Formal Statistical Analysis
  • Maude
  • Probabilistic Rewrite Theories
  • Rewriting Logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol'. Together they form a unique fingerprint.

  • Cite this