Home // Research // FSTC // Computer Sci... // Research Pro... // Distance Bounding: a graph theoretical and formal approach

Distance Bounding: a graph theoretical and formal approach

Budget Code: C15/IS/10428112
Funding: Fonds National de la Recherche
Start Date: April 1, 2016
End Date: March 30, 2018


Physical proximity is a common requirement in access control policies in the physical world. One normally expects someone to be present when opening a door or turning on a car. In practice, the very design of many access control mechanisms enforces physical proximity naturally, e.g., mechanic locks or biometric identification. In wireless systems, however, providing the same kind of guarantee is far from being trivial. The most reliable approach to proximity checking in wireless systems is distance bounding, that is, a cryptographic protocol where the propagation time of messages traveling at the speed of light determine an upper bound on the distance between two devices. Distance bounding protocols can be used as efficient building blocks for a variety of services and applications, such as routing, physical access control, neighbor discovery, tracking and localization.

The purpose of this project is to improve and formally verify the security guarantees of distance bounding protocols. In particular, we will focus on graph-based distance bounding protocols; a prominent family of distance bounding protocols based on random walks in graphs. Graph-based distance bounding protocols are efficient building blocks suitable to be implemented
in low-cost devices such as RFID tags. One based on trees and another one based on a peculiar graph structure named Poulidor, are the two graph-based distance bounding protocols proposed up to now. They remain unbroken, and no other distance bounding protocol has proven to outperform them. Nevertheless, very little is known about this type of protocols. In this project, we will study the relation between graph properties and the security properties of graph-based distance bounding protocols. Our starting point is an observation that, to the best of our knowledge, has not been made before: the Poulidor graph belongs to the well known family of Cayley graphs. Therefore, understanding and studying the relation between graph-based hash functions (where Cayley graphs are used) and graph-based distance bounding protocols, may lead to better designs of this type of security protocols. We will also develop a symbolic approach for the formal verification of distance bounding protocols, which will be used to verify the security and correctness of our own solutions. The few existing symbolic approaches explicitly introduce either timestamps or a global notion of time to the security model. The novelty of our approach is that we expect to formalize the notion of proximity as an ordering problem instead. This keeps the model simple and more appealing to practitioners.