Hrvatska znanstvena Sekcija img
3 gif
 O projektu
4 gif
Pregledavanje radova
Jednostavno pretraživanje
Napredno pretraživanje
Skupni podaci
Upis novih radova
Ispravci prijavljenih radova
Ostale bibliografije
Slični projekti
 Bibliografske baze podataka

Pregled bibliografske jedinice broj: 953306

Zbornik radova

Autori: Alturki, M.A.; Kanovich, Max; Ban Kirigin, Tajana; Nigam, Vivek; Scedrov, Andre; Talcott, Carolyn
Naslov: Statistical Model Checking in the Analysis of Distance- bounding Protocols
Izvornik: Book of Abstracts
Skup: Logic and Applications 2018
Mjesto i datum: Dubrovnik, Hrvatska, 24-28.9.2018.
Ključne riječi: Distance-bounding protocols, Distance fraud, Probabilistic rewriting, Sta- tistical model checking, Maude
Proximity based access control systems, such as systems using smart-cards or smart keys, use cryptographic protocols to ensure their security requirements. However, ensuring authentication alone may not meet the security goals. Namely, proximity based access is well-known to be vulnerable to relay attacks, also known as Mafia fraud. Distance- bounding (DB) protocols were proposed to prevent such relay attacks on proximity-based access control systems. Besides authentication DB protocols aim to ensure physical proximity between the parties involved, namely between the verifier, controling the access to some resource, and the prover, requesting access. In a DB protocol, the verifier computes an upper bound on the distance to the prover. This is done by measuring the time needed for a signal to travel to the prover and back, relying on the assumptions on the maximum signal's velocity. DB protocols are, however, vulnerable to distance fraud, in which a dishonest prover is able to manipulate the distance estimation computed by the verifier in order to make himself appear closer than he actually is. Distance fraud attacks are timing attacks which are particularly significant as they may appear without collusion with external entities. Despite their conceptual simplicity, formal analysis of DB protocols is challenging, involving many subtleties. Devising a formal characterization of DB protocols and distance fraud attacks that is amenable to automated formal analysis is non-trivial, primarily because of their real-time and probabilistic nature. In this work, we present a framework, based on rewriting logic, for formal analysis of different forms of distance-fraud, including recently identified timing attacks. We introduce a generic, real-time and probabilistic model of DB protocols and use it to (mechanically) establish false-acceptance and false-rejection probabilities through statistical model checking with Maude and PVeStA. In the analysis we consider various settings and attacker models. Using this framework, we firstly accurately confirm known results. We then define and quantitatively evaluate new guessing-ahead attack strategies that would otherwise be difficult to analyze manually.
Vrsta sudjelovanja: Predavanje
Vrsta prezentacije u zborniku: Sažetak
Vrsta recenzije: Međunarodna recenzija
Projekt / tema: HRZZ-UIP-05-2017-9219
Izvorni jezik: ENG
Kategorija: Znanstveni
Znanstvena područja:
URL Internet adrese:
Upisao u CROSBI: Tajana Ban Kirigin (, 10. Ruj. 2018. u 14:34 sati

Verzija za printanje   za tiskati