Datum održavanja: petak, 30.11.2018. u 11:00 sati, prostorija O-357
Predavač: doc. dr. sc.Tajana Ban-Kirigin, Odjel za matematiku, Sveučilište u Rijeci
Naziv predavanja:Statistical Model Checking in the Analysis of Distance-bounding Protocols

Abstract:

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.

CV:

Tajana Ban Kirigin is an Assistant Professor at Department of Mathematics, University of Rijeka. She is a member of Seminar of mathematical logic and Seminar for Computer science at Department of Mathematics, Faculty of Natural Sciences and Mathematics, University of Zagreb. Her main research interests are in mathematical logic and theoretical computer science, in particular in collaborative systems and protocol security, as well as interdisciplinary applications of logic and computer science. She has been involved in collaboration on both national and international research projects resulting in several scientific articles presented at renowned international conferences and published in recognized international journals.