Secure Neighbor Discovery in Wireless Networks: Formal Investigation of Possibility

TL;DR

This paper provides a formal analysis of secure neighbor discovery in wireless networks, proving the impossibility of certain protocols under general conditions and identifying scenarios where security can be achieved.

Contribution

It introduces a formal model for wireless neighbor discovery, proves an impossibility result for time-based protocols, and shows that time- and location-based protocols can secure neighbor discovery.

Findings

Impossibility of secure neighbor discovery with time-based protocols under general conditions

Conditions under which the impossibility result does not hold

Time- and location-based protocols can achieve secure neighbor discovery

Abstract

Wireless communication enables a broad spectrum of applications, ranging from commodity to tactical systems. Neighbor discovery (ND), that is, determining which devices are within direct radio communication, is a building block of network protocols and applications, and its vulnerability can severely compromise their functionalities. A number of proposals to secure ND have been published, but none have analyzed the problem formally. In this paper, we contribute such an analysis: We build a formal model capturing salient characteristics of wireless systems, most notably obstacles and interference, and we provide a specification of a basic variant of the ND problem. Then, we derive an impossibility result for a general class of protocols we term "time-based protocols," to which many of the schemes in the literature belong. We also identify the conditions under which the impossibility result is lifted. Moreover, we explore a second class of protocols we term "time- and location-based protocols," and prove they can secure ND.