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.
@article{51,
title = {Formal analysis of security protocols for Wireless Sensor Networks},
journal = {Tatra Mountains Mathematical Publications},
volume = {49},
year = {2011},
doi = {10.2478/tatra.v47i0.51},
language = {EN},
url = {http://dml.mathdoc.fr/item/51}
}
Novotný, Marián. Formal analysis of security protocols for Wireless Sensor Networks. Tatra Mountains Mathematical Publications, Tome 49 (2011) . doi : 10.2478/tatra.v47i0.51. http://gdmltest.u-ga.fr/item/51/