Affiliations: [a] Federal University of Paraíba, João Pessoa, Brazil. E-mail: [email protected] | [b] KFUPM, Dhahran, Saudi Arabia. E-mail: [email protected] | [c] Runtime Verification Inc., USA | [d] Department of Mathematics, University of Rijeka, Rijeka, Croatia. E-mail: [email protected] | [e] University College London, London, UK. E-mail: [email protected] | [f] National Research University Higher School of Economics, Moscow, Russian Federation | [g] fortiss, Germany. E-mail: [email protected] | [h] University of Pennsylvania, Philadelphia, PA, USA. E-mail: [email protected] | [i] National Research University Higher School of Economics, Moscow, Russian Federation, until July 2020 | [j] SRI International, Menlo Park, CA, USA. E-mail: [email protected]
Correspondence:
[*]
Corresponding author: Tajana Ban Kirigin, Department of Mathematics, University of Rijeka, Radmile Matejcic 2, 51000 Rijeka, Croatia. Tel.: +385-51-584650; E-mail: [email protected].
Abstract: Protocol security verification is one of the best success stories of formal methods. However, some aspects important to protocol security, such as time and resources, are not covered by many formal models. While timing issues involve e.g., network delays and timeouts, resources such as memory, processing power, or network bandwidth are at the root of Denial of Service (DoS) attacks which have been a serious security concern. It is useful in practice and more challenging for formal protocol verification to determine whether a service is vulnerable not only to powerful intruders, but also to resource-bounded intruders that cannot generate or intercept arbitrarily large volumes of traffic. A refined Dolev–Yao intruder model is proposed, that can only consume at most some specified amount of resources in any given time window. Timed protocol theories that specify service resource usage during protocol execution are also proposed. It is shown that the proposed DoS problem is undecidable in general and is PSPACE-complete for the class of resource-bounded, balanced systems. Additionally, we describe a decidable fragment in the verification of the leakage problem for resource-sensitive timed protocol theories.
Keywords: Multiset rewriting, protocol security, complexity, denial of service
