Design and Analysis of a Generalized Canvas Protocol

Abstract : The Canvas protocol was developed by Harald Vogt [10] and should provide data integrity in Wireless Sensor Networks. However, Dieter Gollmann published [5] an attack on the protocol. This example supports a widespread belief that design of security protocols is notoriously error-prone. Therefore, it is required to use formal methods to analyze their security properties. In the paper we present design and analysis of a generalized Canvas protocol. We consider the fallacy of the Canvas scheme in different models of the attacker and present a solution for correcting the scheme. We discuss a motivation for generalization of the Canvas protocol and introduce a k-generalized version of the scheme for some parameter k ≥ 2. We build a formal model of the k-generalized 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. In the semantic model of the applied pi-calculus we specify the data integrity property of the scheme. We prove that the proposed k-generalized Canvas scheme, in the presence of an active adversary, provides data integrity of messages assuming that at least one honest node exists on each path of the length k − 1 in the communication graph of a sensor network. Finally, we discuss the usability of the proposed formal model for other WSN security protocols.