We propose SR3, a secure and resilient algorithm for convergecast routing in WSNs. SR3 uses lightweight cryptographic primitives to achieve data confidentiality and data packet unforgeability. SR3 has a security proven by formal tool. We made simulations to show the resiliency of SR3 against various scenarios, where we mixed selective forwarding, blackhole, wormhole, and Sybil attacks. We compared our solution to several routing algorithms of the literature. Our results show that the resiliency accomplished by SR3 is drastically better than the one achieved by those protocols, especially when the network is sparse. Moreover, unlike previous solutions, SR3 self-adapts after compromised nodes suddenly change their behavior.

Analyses of routing protocols security are nearly always supported by simulations, which often evaluate the ability to deliver messages to a given destination. Several competing definitions for secure routing exist, but to our knowledge, they only address source routing protocols. In this paper, we propose the notion of corruptibility, a quantitative computational definition for routing security based on the attacker's ability to alter the routes used by messages. We first define incorruptibility, and we follow with the definition of bounded corruptibility, which uses two routing protocols as bounds for the evaluated protocol. These definitions are then illustrated with several routing algorithms.

To secure Wireless Ad-hoc Networks (WANET) against malicious behaviors, three components are needed: prevention, detection, and response. In this paper, we focus on Intrusion Detection Systems (IDS) for WANET. We classify the different inputs used by the decision process of these IDS, according to their level of cooperation, and the source of their data. We then propose a decision aid which allows automated discovery of attacks for IDS, according to the inputs used. Finally we apply our framework to discover weaknesses in two existing IDS.

Nous proposons un algorithme resilient et securise pour le routage dans les reseaux de capteurs sans fil. Il garantit la confidentialite des donnees routees, ainsi que l'authenticite et l'integrite des messages les transportant. Ces proprietes ont ete prouvees avec CryptoVerif. Nos resultats experimentaux montrent que la resilience de notre algorithme face a plusieurs scenarios d'attaque est meilleure que celle de plusieurs autres protocoles de routage, surtout dans des reseaux peu denses. De plus, notre algorithme s'adapte face aux attaquants dont le comportement evolue au cours du temps.

Neighborhood discovery is a critical part of wireless sensor networks, yet little work has been done on formal verification of the protocols in presence of both intruder nodes and mobility. We present a formal trace-based model to verify protocols doing neighborhood discovery, and we provide a formal definition of (1)neighborhood and (k)-neighborhood. We also analyze a protocol from the literature, and show some conditions needed for its correctness. Finally, we present the groundwork for a protocol which discovers (k)-neighborhood based on (1)-neighborhood data under some assumptions, and prove that it remains secure even if an intruder interferes.