@inproceedings{kanovich18fcs, author = {Alturki, Musab A. and Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn and Ban Kirigin, Tajana}, title = {Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols.}, booktitle = {"Workshop on Foundations of Computer Security"}, year = {2018}, abstract = {Distance-bounding (DB) protocols were proposed tothwart relay attacks on proximity-based access control systems.In a DB protocol, the verifier computes an upper bound on thedistance to the prover by measuring the time needed for a signalto travel to the prover and back. DB protocols are, however,vulnerable to distance fraud, in which a dishonest prover isable to manipulate the distance bound computed by an honestverifier. Despite their conceptual simplicity, devising a formalcharacterization of DB protocols and distance fraud attacks thatis amenable to automated formal analysis is non-trivial, primarilybecause of their real-time and probabilistic nature. In this work,we present a framework, based on rewriting logic, for formallyanalyzing different forms of distance-fraud, including recentlyidentified timing attacks. We introduce a generic, real-time andprobabilistic model of DB protocols and use it to (mechanically)verify false-acceptance and false-rejection probabilities undervarious settings and attacker models through statistical modelchecking with MAUDE and PVESTA. Using this framework,we first accurately confirm known results and then define andquantitatively evaluate new guessing-ahead attack strategies thatwould otherwise be difficult to analyze manually.}, }