Vulnerability of INSENS to denial of service attacks

Wireless Sensor Networks (WSNs) may be deployed in hostile or inaccessible environments and are often unattended. In these conditions securing a WSN against malicious attacks is a particular challenge. This paper proposes to use formal methods to investigate the security of the INSENS protocol, in respect of its capability to withstand several denial of service attacks. The paper is an extension to our previous work where we proposed a formal framework to verify some wireless routing protocols. We have confirmed that the bidirectional verification employed by INSENS prevents attacks such as hello flood. However, INSENS is shown to be vulnerable to invisible node, wormhole and black hole attacks, even in a network of only a few nodes communicating over ideal channels. Packet loss in the presence of these attacks has been demonstrated and quantified using the TOSSIM wireless simulator.