Model Checking Techniques for Verification of an Encryption Scheme for Wireless Sensor Networks

TL;DR

This paper presents a formal verification framework for an encryption scheme in Wireless Sensor Networks using Petri nets, Promela, and SPIN model checker to ensure correctness and identify potential issues.

Contribution

It introduces a novel approach to model and verify WSN encryption schemes with Petri nets and SPIN, providing a systematic method for correctness validation.

Findings

Successfully modeled WSN encryption in Promela

Verified correctness properties with SPIN

Identified counterexamples to improve system reliability

Abstract

In this paper, we deal with the formal verification of an encryption scheme for Wireless Sensor Networks (WSNs). Especially, we present our first results on building a framework dedicated to modelling and verification of WSNs aspects. To achieve our goal, we propose to specify WSNs models written in Petri nets using Promela constructs in order to verify correctness properties of them using SPIN Model checker. We first specify in Promela a Petri net description of an encryption scheme for WSNs that describes its behavior. Then, correctness properties that express requirements on the system's behavior are formulated in Linear Temporal Logic (LTL). Finally, SPIN model checker is used to check if a specific correctness property holds for the model, and, if not, to provide a counterexample: a computation that does not satisfy this property. This counterexample will help to detect the source of the eventual problem and to correct it.