<abstract xmlns="http://www.w3.org/1999/xhtml"><p> Design of security protocols is notoriously error-prone. For this reason, it is required to use formal methods to analyze their security properties. In the paper we present a formal analysis of the Canvas protocol. The Canvas protocol was developed by Harald Vogt and should provide data integrity inWireless Sensor Networks. However, Dieter Gollmann published an attack on the protocol. We consider the fallacy of the Canvas scheme in different models of the attacker and present a solution for correcting the scheme.We propose a formal model of the fixed Canvas protocol in the applied pi-calculus. This model includes a model of the network topology, communication channels, captured nodes, and capabilities of the attacker. Moreover, we formulate and analyze the data integrity property of the scheme in the semantic model of the applied pi-calculus. We prove that the fixed Canvas scheme, in the presence of an active adversary, provides data integrity of messages assuming that captured nodes are not direct neighbors in the communication graph of a sensor network. Finally, we discuss the applicability of the proposed formal model for analysis of other WSN security protocols.</p></abstract>

Design of security protocols is notoriously error-prone. For this reason, it is required to use formal methods to analyze their security properties. In the paper we present a formal analysis of the Canvas protocol. The Canvas protocol was developed by Harald Vogt and should provide data integrity inWireless Sensor Networks. However, Dieter Gollmann published an attack on the protocol. We consider the fallacy of the Canvas scheme in different models of the attacker and present a solution for correcting the scheme.We propose a formal model of the fixed Canvas protocol in the applied pi-calculus. This model includes a model of the network topology, communication channels, captured nodes, and capabilities of the attacker. Moreover, we formulate and analyze the data integrity property of the scheme in the semantic model of the applied pi-calculus. We prove that the fixed Canvas scheme, in the presence of an active adversary, provides data integrity of messages assuming that captured nodes are not direct neighbors in the communication graph of a sensor network. Finally, we discuss the applicability of the proposed formal model for analysis of other WSN security protocols.

Formal analysis of security protocols for wireless sensor networks

Institute of Computer Science Faculty of Science Pavol Jozef ˇSaf´arik University Jesenn´a 5 SK–040 01–Koˇsice SLOVAKIA

Tatra Mountains Mathematical Publications

{"article-title":"Formal analysis of security protocols for wireless sensor networks"}

Design of security protocols is notoriously error-prone. For this reason, it is required to use formal methods to analyze their security properties. In the...

Formal analysis of security protocols for wireless sensor networks

Published Online: Nov 13, 2012

Page range: 81 - 97

DOI: https://doi.org/10.2478/v10127-010-0032-7

Keywords
security protocols, Wireless Sensor Networks, formal analysis, Dolev-Yao model of the attacker, data integrity, the applied pi-calculus.

This content is open access.

Formal analysis of security protocols for wireless sensor networks

Published Online: Nov 13, 2012

Page range: 81 - 97

DOI: https://doi.org/10.2478/v10127-010-0032-7

Keywordssecurity protocols, Wireless Sensor Networks, formal analysis, Dolev-Yao model of the attacker, data integrity, the applied pi-calculus.

This content is open access.

Keywords
security protocols, Wireless Sensor Networks, formal analysis, Dolev-Yao model of the attacker, data integrity, the applied pi-calculus.