%0 Journal Article
%T On Formal and Automatic Security Verification of WSN Transport Protocols
%A Vinh Thong Ta
%A Levente Butty¨˘n
%A Amit Dvir
%J ISRN Sensor Networks
%D 2014
%R 10.1155/2014/891467
%X We address the problem of formal and automated security verification of transport protocols for wireless sensor networks (WSN) that may perform cryptographic operations. The verification of this class of protocols is difficult because they typically consist of complex behavioral characteristics, such as real-time, probabilistic, and cryptographic operations. To solve this problem, we propose a probabilistic timed calculus for cryptographic protocols and demonstrate how to use this formal language for proving security or vulnerability of protocols. The main advantage of the proposed language is that it supports an expressive syntax and semantics, allowing for studying real-time, probabilistic, and cryptographic issues at the same time. Hence, it can be used to verify systems that involve these three properties in a convenient way. In addition, we propose an automatic verification method, based on the well-known PAT process analysis toolkit, for this class of protocols. For demonstration purposes, we apply the proposed manual and automatic proof methods for verifying the security of DTSN and SDTP, which are two of the recently proposed WSN transport protocols. 1. Introduction Numerous transport protocols have been proposed specifically designed for applications of wireless sensor networks (WSN), requiring particularly reliable delivery and congestion control (e.g., multimedia sensor networks) [1]. Two of the latest protocols are the distributed transport for sensor networks (DTSN) [2] and its secured version, the secure distributed transport protocol for sensor networks (SDTP) [3]. In DTSN and SDTP the intermediate nodes can cache the packets with some probability and retransmit them upon request, providing reliable transmission, energy efficiency, and distributed functionality. Unfortunately, existing transport protocols for WSNs (including DTSN) do not include sufficient security mechanisms or totally ignore the security issue. Hence, many attacks have been found against existing WSN transport protocols [4]. Broadly speaking, these attacks can be classified into two groups: attacks against reliability and energy depleting attacks. Reliability attacks aim to mislead the nodes so that loss of a data packet remains undetected. In the case of energy depleting attacks, the goal of the attacker is to perform energy-intensive operations in order to deplete the nodesĄŻ batteries [4]. In particular, using a fake or altered acknowledgment message, an attacker can give the sender the impression that data packets arrived safely when they may actually have been lost.
%U http://www.hindawi.com/journals/isrn.sensor.networks/2014/891467/