Napredna pretraga

Pregled bibliografske jedinice broj: 700992

Towards Timed Models for Cyber-Physical Security Protocols


Kanovich, Max; Ban Kirigin, Tajana; Nigam, Vivek; Scedrov, Andre; Talcott, Carolyn
Towards Timed Models for Cyber-Physical Security Protocols // Joint Workshop on Foundations of Computer Security and Formal and Computational Cryptography
Beč, Austria, 2014. (predavanje, međunarodna recenzija, neobjavljeni rad, znanstveni)


Naslov
Towards Timed Models for Cyber-Physical Security Protocols

Autori
Kanovich, Max ; Ban Kirigin, Tajana ; Nigam, Vivek ; Scedrov, Andre ; Talcott, Carolyn

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

Skup
Joint Workshop on Foundations of Computer Security and Formal and Computational Cryptography

Mjesto i datum
Beč, Austria, 18.7.2014

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
Timed Collaborative Systems ; Multiset Rewriting ; Distance Bounding Protocols ; Cyber-Physical Security Protocols ; Computational Complexity

Sažetak
Many security protocols rely on the assumptions on the physical properties in which its protocols essions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. We classify such security protocols as cyber- physical. The key elements of such protocols are the use of cryptographic keys, nonces and time. This paper investigates timed models for the verification of such protocols. Firstly, we introduce a multiset rewriting framework with continuous time and fresh values. We demonstrate that in this framework one can specify distance bounding protocols and intruder models for cyber-physical security protocols that take into account the physical properties of the environment. Then we prove that models with discrete time are not able to expose as many security flaws as models with continuous time. This is done by proposing a protocol and demonstrating that there is no attack to this protocol when using the model with discrete time, but there is an attack when using the model with continuous time. For the important class of Bounded Memory Cyber-Physical Security Protocols with a Memory Bounded Intruder the reachability problem is PSPACE-complete if the size of terms is bounded.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo, Filozofija



POVEZANOST RADA


Projekt / tema
009-0091328-0941 - Logika i stvarnost (Majda Trobok, )
120-1203164-3074 - Matematička logika i primjene (Zvonimir Šikić, )

Ustanove
Filozofski fakultet, Rijeka,
Fakultet strojarstva i brodogradnje, Zagreb,
Sveučilište u Rijeci - Odjel za matematiku

Autor s matičnim brojem:
Tajana Ban-Kirigin, (229313)