arXiv · 1109.5088
A Semantic Analysis of Key Management Protocols for Wireless Sensor Networks
Abstract
We propose a simple timed broadcasting process calculus for modelling wireless network protocols. The operational semantics of our calculus is given in terms of a labelled transition semantics which is used to derive a standard (weak) bi-simulation theory. Based on our simulation theory, we reformulate Gorrieri and Martinelli's timed Generalized Non-Deducibility on Compositions (tGNDC) scheme, a well-known general framework for the definition of timed properties of security protocols. We use tGNDC to perform a semantic analysis of three well-known key management protocols for wireless sensor networks: \mu TESLA, LEAP+ and LiSP. As a main result, we provide a number of attacks to these protocols which, to our knowledge, have not yet appeared in the literature.
Explore related subjects
Keep this discovery
Francesco Ballardin, Damiano Macedonio, Massimo Merro, Mattia Tirapelle. 2011-09-23. A Semantic Analysis of Key Management Protocols for Wireless Sensor Networks. https://arxiv.org/abs/1109.5088
Cite the original work for its findings. Save a collection to share your selection of sources.