Nalazite se na CroRIS probnoj okolini. Ovdje evidentirani podaci neće biti pohranjeni u Informacijskom sustavu znanosti RH. Ako je ovo greška, CroRIS produkcijskoj okolini moguće je pristupi putem poveznice www.croris.hr
izvor podataka: crosbi !

A Multiset Rewriting Model for the Specification and Verification of Resource and Timing Aspects of Security Protocols (CROSBI ID 681711)

Prilog sa skupa u zborniku | sažetak izlaganja sa skupa | međunarodna recenzija

Urquiza, Abraão Aires ; Alturki, Musab A. ; Kanovich, Max ; Ban Kirigin, Tajana ; Nigam, Vivek ; Scedrov, Andre ; Talcott, Carolyn A Multiset Rewriting Model for the Specification and Verification of Resource and Timing Aspects of Security Protocols // Book of Abstracts LAP 2019. 2019. str. 8-10

Podaci o odgovornosti

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

engleski

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

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.

Security Protocols, Dolev-Yao Intruder, Denial of Service Attacks, Distancebounding protocols, Multiset Rewriting, Computational Complexity

nije evidentirano

nije evidentirano

nije evidentirano

nije evidentirano

nije evidentirano

nije evidentirano

Podaci o prilogu

8-10.

2019.

objavljeno

Podaci o matičnoj publikaciji

Book of Abstracts LAP 2019

Podaci o skupu

8th International Conference Logic and Applications (LAP 2019)

ostalo

23.09.2019-27.09.2019

Dubrovnik, Hrvatska

Povezanost rada

Matematika, Računarstvo