A Semantic Analysis of Key Management Protocols for Wireless Sensor Networks

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.