Secure Neighbor Discovery in Wireless Networks: Formal Investigation of Possibility
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, the authors contribute such an analysis: They build a formal model capturing salient characteristics of wireless systems, most notably obstacles and interference, and they provide a specification of a basic variant of the ND problem. Then, they derive an impossibility result for a general class of protocols they term "Time-based protocols", to which many of the schemes in the literature belong.