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

Statistical Model Checking of Distance Fraud Attacks on the Hancke-Kuhn Family of Protocols (CROSBI ID 664942)

Prilog sa skupa u zborniku | izvorni znanstveni rad | međunarodna recenzija

Alturki, M.A. ; Kanovich, Max ; Ban Kirigin, Tajana ; Nigam, Vivek ; Scedrov, Andre ; Talcott, Carolyn Statistical Model Checking of Distance Fraud Attacks on the Hancke-Kuhn Family of Protocols // Proceedings of the 2018 Workshop on Cyber-Physical Systems Security and PrivaCy, CPS-SPC '18. New York (NY): The Association for Computing Machinery (ACM), 2018. str. 60-71 doi: 10.1145/3264888.3264895

Podaci o odgovornosti

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

engleski

Statistical Model Checking of Distance Fraud Attacks on the Hancke-Kuhn Family of Protocols

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.

Distance-bounding protocols ; Distance fraud ; Probabilistic rewriting ; Statistical model checking ; Maude

nije evidentirano

nije evidentirano

nije evidentirano

nije evidentirano

nije evidentirano

nije evidentirano

Podaci o prilogu

60-71.

2018.

objavljeno

10.1145/3264888.3264895

Podaci o matičnoj publikaciji

Proceedings of the 2018 Workshop on Cyber-Physical Systems Security and PrivaCy, CPS-SPC '18

New York (NY): The Association for Computing Machinery (ACM)

978-1-4503-5992-4

Podaci o skupu

4th ACM Workshop on Cyber-Physical Systems Security & Privacy (CPS-SPC)

predavanje

15.10.2018-19.10.2018

Toronto, Kanada

Povezanost rada

Matematika, Računarstvo

Poveznice