Modelling and Analysing a WSN Secure Aggregation Protocol: A Comparison of Languages and Tool Support

Volkan Cambazoglu, Ramūnas Gutkovas, Johannes Åman Pohjola, and Björn Victor

November 2015

Abstract:

A security protocol promises protection of a significant piece of information while using it for a specific purpose. Here, the protection of the information is vital and a formal verification of the protocol is an essential step towards guaranteeing this protection. In this work, we study a secure aggregation protocol (SHIA) for Wireless Sensor Networks and verify the protocol in three formal modelling tools (Pwb, mCRL2 and ProVerif). The results of formal verification heavily depend on the model specification and the ability of the tools to deal with the model. Among the three tools, there is difference in data representation, communication types and the level of abstraction in order to represent SHIA. ProVerif and mCRL2 are mature and well-established tools, geared respectively towards security and distributed systems; however, their expressiveness constrains modelling SHIA and its security properties. Pwb is an experimental tool developed by the authors; its relative immaturity is offset by its increased expressive power and customisability. This leads to different models of the same protocol, each contributing in different ways to our understanding of SHIA's security properties.

Note: Updated 2015-12-02: The results in subsection 4.1.3 are updated because we realised that Pwb can evaluate the SHIA model faster for network sizes of 2 and 4, and also can handle network size of 8.

Available as PDF (651 kB, no cover)

Download BibTeX entry.