Page d'accueil // Recherche // FSTC // Computer Sci... // Projets de r... // Distance Bounding: a graph theoretical and formal approach

Distance Bounding: a graph theoretical and formal approach

Code budgetaire: C15/IS/10428112
Financement: FNR - Other
Date de début: 1 avril 2016
Date de fin: 30 mars 2018

Description

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 identi cation. 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 ecient 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 ecient 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 veri cation 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.

Membres