Published In Fine-Grained MSR Specifications for Quantitative Security Analysis

Abstract. The traditional Dolev-Yao model of security limits attacks to “com-putationally feasible ” operations. We depart from this model by assigning a cost to protocol actions, both of the Dolev-Yao kind as well as non traditional forms such as computationally-hard operations, guessing, principal subversion, and fail-ure. This quantitative approach enables evaluating protocol resilience to various forms of denial of service, guessing attacks, and resource limitation. While the methodology is general, we demonstrate it through a low-level variant of the MSR specification language.