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 metadatas

Cited literature [33 references]  Display  Hide  Download

https://hal-upec-upem.archives-ouvertes.fr/hal-01132722
Contributor : Quentin Monnet <>
Submitted on : Tuesday, March 17, 2015 - 5:52:35 PM
Last modification on : Friday, October 4, 2019 - 1:13:15 AM
Long-term archiving on: Monday, April 17, 2017 - 4:59:29 PM

File

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

Identifiers

  • HAL Id : hal-01132722, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

303

Files downloads

428