Naslov
A Multiset Rewriting Model for the Specification and Verification of Resource and Timing Aspects of Security Protocols

Autori
Urquiza, Abraão Aires ; Alturki, Musab A. ; Kanovich, Max ; Ban Kirigin, Tajana ; Nigam, Vivek ; Scedrov, Andre ; Talcott, Carolyn

Vrsta, podvrsta i kategorija rada
Sažeci sa skupova, sažetak, znanstveni

Izvornik
Book of Abstracts LAP 2019 / - , 2019, 8-10

Skup
8th International Conference Logic and Applications (LAP 2019)

Mjesto i datum
Dubrovnik, Hrvatska, 23.09.2019. - 27.09.2019

Vrsta sudjelovanja
Ostalo

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
Security Protocols, Dolev-Yao Intruder, Denial of Service Attacks, Distancebounding protocols, Multiset Rewriting, Computational Complexity

Sažetak
Protocol security verification is one of the best success stories of formal methods. Tools can automatically discover logical attacks and many new attacks have been found by existing methods. However, other aspects important to protocol security are not covered by many formal models. Time and resources are some of such aspects. For example, Denial of Service (DoS) attacks have been a serious security concern, as no service is, in principle, protected against them. Although a Dolev-Yao intruder with unlimited resources can trivially render any service unavailable, DoS attacks do not necessarily have to be carried out by such (extremely) powerful intruders. It is useful in practice and more challenging for formal protocol verification to determine whether a service is vulnerable even to resource-bounded intruders that cannot generate or intercept arbitrary large volumes of traffic. Similarly, formal intruder models should take into account the physical properties related to time, such as message transmission time and processing delays. Other timing aspects of protocols, such as timeouts, may affect protocol execution and security. This paper describes the use of Multiset Rewriting for the specification and verification of resource and timing aspects of protocols, such as network delays, timeouts, distance bounding properties and DoS attacks. We propose a novel, more refined intruder model where the intruder can only consume at most some specified amount of resources in any given time window. Additionally, we propose protocol theories that may contain timeouts and specify service resource usage during protocol execution. We detail these timed features with a number of examples and describe decidable fragments of related secrecy problem as well as false acceptance and false rejection problems related to distance bounding protocols. We also illustrate the power of our approach by representing a number of classes of DoS attacks, such as, Slow, Asymmetric and Amplification DoS attacks, exhausting different types of resources of the target, such as, number of workers, processing power, memory, and network bandwidth. We show that the proposed DoS problem is undecidable in general and is PSPACE-complete for the class of resource-bounded, balanced systems.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo

POVEZANOST RADA