Naslov
Specifying and verifying timing aspects of security protocols

Autori
Alturki, Musab A. ; Kanovich, Max ; Ban Kirigin, Tajana ; Nigam, Vivek ; Scedrov, Andre ; Talcott, Carolyn

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

Skup
2nd workshop Formal Reasoning and Semantics (FORMALS 2019)

Mjesto i datum
Zagreb, Hrvatska, 17.06.2019. - 18.06.2019

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Domaća recenzija

Ključne riječi
Multiset Rewriting, Security Protocols, Dolev-Yao Intruder, DistanceBounding Protocols, Computational Complexity

Sažetak
Protocol Security Verification is one of the greatest success stories of formal methods. Indeed, a number of attacks on security protocols have been found using formal methods. Tools are used in the automated discovery of new attacks and the shaping of new protocols. However, some aspects relevant to protocol security are not covered by many formal models. Time is one of such important aspects. We describe the use of Multiset Rewriting for the specification and verification of timing aspects of protocols, such as network delays, processing time, timeouts, timed intruder models and distance bounding properties. We investigate such timed features and specify these timing aspects of security protocols using multiset rewriting with real time. We formalize timed Dolev-Yao intruder theories, as well as network and protocol theories that take into account physical laws related to time. We also investigate related verification problems, such as the secrecy problem and the false acceptance and the false rejection problems related to DistanceBounding Protocols. We describe decidable fragments of our framework for the specification and verification of timing properties of security protocols and provide PSPACE complexity results.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo

POVEZANOST RADA