Lightweight Specification Language and Verification Framework for Sensor Network Security Protocols

Hanna, Youssef, Rajan, Hridesh and Zhang, Wensheng (2006) Lightweight Specification Language and Verification Framework for Sensor Network Security Protocols. Technical Report 06-31, Computer Science, Iowa State University.

This is the latest version of this eprint.

Abstract

The contribution of this work is an approach for lightweight specification and verification of nesC implementations of sensor networks security protocols. Our approach provides annotations to specify objectives, network topology, intruder models, and channel fault models. The objectives of the protocols can be specified in terms of user-defined events, which is significantly more expressive compared to earlier approaches such as CAPSL that provide a fixed set of objectives. Moreover, our approach is extensible in that it allows new intruder and channel fault models to be added to the verification process. These models are themselves written in nesC. To show the feasibility of our approach, we describe the implementation of our verification framework. Our verification framework uses the model checker SPIN as the underlying technology. Our approach was able to detect earlier known bugs in protocols and an assumption violation in the protocol implementation.

Available Versions of This Paper

• SLEDE: Event-Based Specification of Sensor Network Protocols (deposited 12 October 2006)
  • Lightweight Specification Language and Verification Framework for Sensor Network Security Protocols (deposited 11 December 2006) [Currently displayed]