Naslov
Modelling 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 2020 / - , 2020, 4-6

Skup
Logic and Applications, FORMALS 2020

Mjesto i datum
Dubrovnik, Hrvatska, 21.09.2020. - 25.09.2020

Vrsta sudjelovanja
Ostalo

Vrsta recenzije
Međunarodna recenzija

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

Sažetak
Formal methods in protocol security verification led to discovery of a number of attacks and countermeasures. Even though valid protocol verification should rely on the careful formalization of all the relevant assumptions of the protocol execution, 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 particularly 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. This paper introduces a multiset rewriting model 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 timed protocol theories that specify service resource usage during protocol execution. Also, a refined Dolev-Yao intruder model is proposed, that can only consume at most some specified amount of resources in any given time window. We formally define the DoS problem that takes into account the duration of the attack. It is shown that the proposed DoS problem is undecidable in general and is PSPACE-complete for the class of balanced resource-bounded systems. Additionally, protocol theories for protocols particularly susceptible to time, such as e.g., distance-bounding protocols, are proposed and some decidable fragments of related verification problems, such as the secrecy problem, are described.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo

POVEZANOST RADA