Formal analysis of security protocols for Wireless Sensor Networks
Abstract
In the paper we present a formal analysis of the Canvas pro-
tocol. The Canvas protocol was designed by Harald Vogt in [11]. Dieter Gollmann published an attack on the protocol in the paper [6]. We propose a formal model of the Canvas protocol in the applied pi-calculus. This model includes the model of the network topology, communication channels, captured nodes and capabilities of the attacker. Moreover, we present the solution for correcting the protocol and prove security properties of the fixed version in the proposed formal model. Finally, we discuss the usability of the formal model for other security protocols for Wireless Sensor Networks.
tocol. The Canvas protocol was designed by Harald Vogt in [11]. Dieter Gollmann published an attack on the protocol in the paper [6]. We propose a formal model of the Canvas protocol in the applied pi-calculus. This model includes the model of the network topology, communication channels, captured nodes and capabilities of the attacker. Moreover, we present the solution for correcting the protocol and prove security properties of the fixed version in the proposed formal model. Finally, we discuss the usability of the formal model for other security protocols for Wireless Sensor Networks.
Full Text:
PDFDOI: https://doi.org/10.2478/tatra.v47i0.51