Publication
This thesis addresses the security of two fundamental elements of wireless networking: neighbor discovery and ranging. Neighbor discovery consists in discovering devices available for direct communication or in physical proximity. Ranging, or distance bounding, consists in measuring the distance between devices, or providing an upper bound on this distance. Both elements serve as building blocks for a variety of services and applications, notably routing, physical access control, tracking and localization. However, the open nature of wireless networks makes it easy to abuse neighbor discovery and ranging, and thereby compromise overlying services and applications. To prevent this, numerous works proposed protocols that secure these building blocks. But two aspects crucial for the security of such protocols have received relatively little attention: formal verification and attacks on the physical-communication-layer. They are precisely the focus of this thesis. In the first part of the thesis, we contribute a formal analysis of secure communication neighbor discovery protocols. We build a formal model that captures salient characteristics of wireless systems such as node location, message propagation time and link variability, and we provide a specification of secure communication neighbor discovery. Then, we derive an impossibility result for a general class of protocols we term "time-based protocols", stating that no such protocol can provide secure communication neighbor discovery. We also identify the conditions under which the impossibility result is lifted. We then prove that specific protocols in the time-based class (under additional conditions) and specific protocols in a class we term "time- and location-based protocols," satisfy the neighbor discovery specification. We reinforce these results by mechanizing the model and the proofs in the theorem prover Isabelle. In the second part of the thesis, we explore physical-communication-layer attacks that can seemingly decrease the message arrival time without modifying its content. Thus, they can circumvent time-based neighbor discovery protocols and distance bounding protocols. (Indeed, they violate the assumptions necessary to prove protocol correctness in the first part of the thesis.) We focus on Impulse Radio Ultra-Wideband, a physical layer technology particularly well suited for implementing distance bounding, thanks to its ability to perform accurate indoor ranging. First, we adapt physical layer attacks reported in prior work to IEEE 802.15.4a, the de facto standard for Impulse Radio, and evaluate their performance. We show that an adversary can achieve a distance-decrease of up to hundreds of meters with an arbitrarily high probability of success, with only a minor cost in terms of transmission power (few dB). Next, we demonstrate a new attack vector that disrupts time-of-arrival estimation algorithms, in particular those designed to be precise. The distance-decrease achievable by t