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

Youcef Hammal (1) , Quentin Monnet (2) , Lynda Mokdad (2) , Jalel Ben-Othman (3) , Abdelkarim Abdelli (1)

1 USTHB - Université des Sciences et de la Technologie Houari Boumediene = University of Sciences and Technology Houari Boumediene [Alger]
2 LACL - Laboratoire d'Algorithmique Complexité et Logique
3 L2TI - Laboratoire de Traitement et Transport de l'Information

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.

Mots clés: Wireless sensor networks; Reliability availability and serviceability; Energy- aware systems; Model-checking; Simulation

Domaines: Modélisation et simulation; Cryptographie et sécurité [cs.CR]; Réseaux et télécommunications [cs.NI]

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, 2014, 12 (1), pp 1−46. ⟨hal-01132722⟩