Skip to Main content Skip to Navigation
Journal articles

Timed automata based modeling and verification of denial of service attacks in wireless sensor networks

Abstract : Sensor networks have been increasingly deployed for civil and military applications over the last years. Due to their low resources, sensors come along with new issues regarding network security and energy consumption. Focusing on the network availability, previous studies proposed to protect the network against denial of service attacks with the use of traffic monitoring agents. Working on the election process, we try to enhance this solution by introducing an energy-aware and secure method to dynamically select these “cNodes” in a clustered WSN: nodes with the higher residual energy get elected. We discuss limitations of this deterministic selection and suggest to designate new control nodes, “vNodes”, to monitor the cNodes by periodically enquiring about their remaining energy, thus ensuring that they do not lie during the election process in attempt to keep their role. Validation is first carried out with a formal specification of our proposal using the UPPAAL model-checker. We model nodes by means of communicating timed automata, logical clocks and timing constraints. Through Computation Tree Logic we express and check properties for the election processes, related to energy and presence of greedy or jamming nodes.
Complete list of metadata

Cited literature [33 references]  Display  Hide  Download
Contributor : Quentin Monnet Connect in order to contact the contributor
Submitted on : Tuesday, March 17, 2015 - 5:52:35 PM
Last modification on : Friday, August 5, 2022 - 2:54:44 PM
Long-term archiving on: : Monday, April 17, 2017 - 4:59:29 PM


Timed automata based modeling ...
Files produced by the author(s)


  • HAL Id : hal-01132722, version 1


Youcef Hammal, Quentin Monnet, Lynda Mokdad, Jalel Ben-Othman, Abdelkarim Abdelli. Timed automata based modeling and verification of denial of service attacks in wireless sensor networks. Studia Informatica Universalis, Hermann, 2014, 12 (1), pp 1−46. ⟨hal-01132722⟩



Record views


Files downloads