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.
Type de document :
Article dans une revue
Studia Informatica Universalis, Hermann, 2014, 12 (1), pp 1−46. 〈http://studia.complexica.net〉
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger

https://hal-upec-upem.archives-ouvertes.fr/hal-01132722
Contributeur : Quentin Monnet <>
Soumis le : mardi 17 mars 2015 - 17:52:35
Dernière modification le : mardi 13 mars 2018 - 11:10:08
Document(s) archivé(s) le : lundi 17 avril 2017 - 16:59:29

Fichier

Timed automata based modeling ...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. 〈http://studia.complexica.net〉. 〈hal-01132722〉

Partager

Métriques

Consultations de la notice

246

Téléchargements de fichiers

324