Formal Model for (k)-Neighborhood Discovery Protocols - Archive ouverte HAL Access content directly
Book Sections Year : 2013

Formal Model for (k)-Neighborhood Discovery Protocols

(1) , (2)


Neighborhood discovery is a critical part of wireless sensor networks, yet little work has been done on formal verification of the protocols in presence of both intruder nodes and mobility. We present a formal trace-based model to verify protocols doing neighborhood discovery, and we provide a formal definition of (1)neighborhood and (k)-neighborhood. We also analyze a protocol from the literature, and show some conditions needed for its correctness. Finally, we present the groundwork for a protocol which discovers (k)-neighborhood based on (1)-neighborhood data under some assumptions, and prove that it remains secure even if an intruder interferes.
Fichier principal
Vignette du fichier
JL12.pdf (676.99 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03885239 , version 1 (05-12-2022)



Raphaël Jamet, Pascal Lafourcade. Formal Model for (k)-Neighborhood Discovery Protocols. Advances in Network Analysis and its Applications, 18, 2013, Advances in Network Analysis and its Applications. Mathematics in Industry, 978-3-642-30903-8. ⟨10.1007/978-3-642-30904-5_8⟩. ⟨hal-03885239⟩
0 View
0 Download



Gmail Facebook Twitter LinkedIn More