A Semantic Analysis of Key Management Protocols for Wireless Sensor Networks
Francesco Ballardin, Damiano Macedonio, Massimo Merro, Mattia, Tirapelle

TL;DR
This paper introduces a timed process calculus for modeling wireless network protocols and uses it to analyze key management protocols, revealing previously unknown security vulnerabilities.
Contribution
It develops a novel timed calculus and applies it to perform a semantic analysis of key management protocols, uncovering new attacks.
Findings
Identified new security attacks on , LEAP+, and LiSP protocols.
Provided a formal semantic framework for analyzing wireless sensor network protocols.
Reformulated the tGNDC scheme for timed security protocol analysis.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity in Wireless Sensor Networks · Access Control and Trust · Advanced Authentication Protocols Security
