Affiliations: [a] Federal University of Paraíba, João Pessoa, Brazil. E-mail: abraauc@gmail.com | [b] KFUPM, Dhahran, Saudi Arabia. E-mail: musab@kfupm.edu.sa | [c] Runtime Verification Inc., USA | [d] Department of Mathematics, University of Rijeka, Rijeka, Croatia. E-mail: bank@math.uniri.hr | [e] University College London, London, UK. E-mail: m.kanovich@ucl.ac.uk | [f] National Research University Higher School of Economics, Moscow, Russian Federation | [g] fortiss, Germany. E-mail: nigam@fortiss.org | [h] University of Pennsylvania, Philadelphia, PA, USA. E-mail: scedrov@math.upenn.edu | [i] National Research University Higher School of Economics, Moscow, Russian Federation, until July 2020 | [j] SRI International, Menlo Park, CA, USA. E-mail: clt@csl.sri.com
Correspondence:
[*]
Corresponding author: Tajana Ban Kirigin, Department of Mathematics, University of Rijeka, Radmile Matejcic 2, 51000 Rijeka, Croatia. Tel.: +385-51-584650; E-mail: bank@math.uniri.hr.
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
