Formal modelling of a robust wireless sensor network routing protocol

Kashif Saghar, William Henderson, David Kendall, Ahmed Bouridane

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

28 Citations (Scopus)


Because of their low cost, small size, low resources and self-organizing nature a Wireless Sensor Network (WSN) is a potential solution in hostile environments including military applications. However, the broadcasting nature of radio transmission; their limited computing, power and communication resources; unattended and potentially hostile nature of the environment they operate in make WSNs prone to Denial of Service (DoS) attacks. Although many schemes have been proposed to address DoS attacks their effectiveness is yet to be proven. The traditional methods used (i.e. visual inspection, computer simulations and hardware implementations) can only detect errors but cannot verify that the whole system is error free. Therefore, new techniques to automatically determine the worst cases and hidden errors in WSNs are much desired. After an initial investigation using a formal verification which clearly shows that Arrive routing protocol is vulnerable to different DoS attacks, this paper proposes a method for its security. The finding contradicts the claim of the developers of Arrive that it is immune to black hole attacks. Several other DoS attacks were also found to be successful in Arrive routing protocol. The formal model generates the trace to confirm how an attack is possible in the protocol. However, it was found that INA attacks are addressed by Arrive protocol. To our best knowledge the results discussed in this paper have not been presented, proved or published before.
Original languageEnglish
Title of host publication2010 NASA/ESA Conference on Adaptive Hardware and Systems (AHS)
Place of PublicationPiscataway, NJ
ISBN (Print)978-1-4244-5887-5
Publication statusPublished - 2010
EventAdaptive Hardware and Systems (AHS) 2010 NASA/ESA Conference - Anaheim Convention Center, Anaheim, California, USA
Duration: 1 Jan 2010 → …


ConferenceAdaptive Hardware and Systems (AHS) 2010 NASA/ESA Conference
Period1/01/10 → …


Dive into the research topics of 'Formal modelling of a robust wireless sensor network routing protocol'. Together they form a unique fingerprint.

Cite this