engleski

Statistical Model Checking in the Analysis of Distance- bounding Protocols

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.

Distance-bounding protocols, Distance fraud, Probabilistic rewriting, Sta- tistical model checking, Maude

nije evidentirano