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

Pregled bibliografske jedinice broj: 951784

Zbornik radova

Autori: Alturki, M.A.; Kanovich, Max; Ban Kirigin, Tajana; Nigam, Vivek; Scedrov, Andre; Talcott, Carolyn
Naslov: Statistical Model Checking of Distance Fraud Attacks on the Hancke-Kuhn Family of Protocols
Izvornik: Proceedings of the 2018 Workshop on Cyber-Physical Systems Security and PrivaCy, CPS-SPC '18New York, NY, USA : ACM Digital Library , 2018. 60-71 (ISBN: 978-1-4503-5992-4).
Skup: ACM Workshop on Cyber-Physical Systems Security & Privacy (CPS-SPC)
Mjesto i datum: Toronto, Kanada, 19.10.2018.
Ključne riječi: Distance-bounding protocols, Distance fraud, Probabilistic rewriting, Statistical model checking, Maude
Sažetak:
Distance-bounding (DB) protocols protect against relay attacks on proximity-based access control systems. In a DB protocol, the verifier computes an upper bound on the distance to the prover by measuring the time-of-flight of exchanged messages. DB protocols are, however, vulnerable to distance fraud, in which a dishonest prover is able to manipulate the distance bound computed by an honest verifier. Despite their conceptual simplicity, 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 introduce a generic, computational model, based on Rewriting Logic, for formally analyzing various forms of distance fraud, including recently identified timing attacks, on the Hancke- Kuhn family of DB protocols through statistical model checking. While providing an insightful formal characterization on its own, the model enables a practical formal analysis method that can help system designers bridge the gap between conceptual descriptions and low-level designs. In addition to accurately confirming known results, we use the model to define new attack strategies and quantitatively evaluate their effectiveness under realistic assumptions that would otherwise be difficult to reason about manually.
Vrsta sudjelovanja: Predavanje
Vrsta prezentacije u zborniku: Cjeloviti rad (više od 1500 riječi)
Vrsta recenzije: Međunarodna recenzija
Projekt / tema: HRZZ-UIP-05-2017-9219
Izvorni jezik: ENG
Kategorija: Znanstveni
Znanstvena područja:
Matematika,Računarstvo
Upisao u CROSBI: Tajana Ban Kirigin (bank@math.uniri.hr), 30. Kol. 2018. u 10:28 sati



Verzija za printanje   za tiskati


upomoc
foot_4