Formal Analysis of Secure Neighbor Discovery in Wireless Networks

Jean-Pierre Hubaux, Panagiotis Papadimitratos, Marcin Poturalski
Ieee Computer Soc, 2013
Article

Résumé

We develop a formal framework for the analysis of security protocols in wireless networks. The framework captures characteristics necessary to reason about neighbor discovery protocols, such as the neighbor relation, device location, and message propagation time. We use this framework to establish general results about the possibility of neighbor discovery. In particular, we show that time-based protocols cannot in general provide secure neighbor discovery. Given this insight, we also use the framework to prove the security of four concrete neighbor discovery protocols, including two novel time-and-location-based protocols. We mechanize the model and some proofs in the theorem prover Isabelle.

Official source

https://infoscience.epfl.ch/record/191015?ln=fr

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés

Chargement

Publications associées

Chargement

Formal Analysis of Secure Neighbor Discovery in Wireless Networks

Marcin Poturalski

We develop a formal framework for the analysis of security protocols in wireless networks. The framework captures characteristics necessary to reason about neighbor discovery protocols, such as the neighbor relation, device location, and message propagation time. We use this framework to establish general results about the possibility of neighbor discovery. In particular, we show that time-based protocols cannot in general provide secure neighbor discovery. Given this insight, we also use the framework to prove the security of four concrete neighbor discovery protocols, including two novel time-and-location based protocols. We mechanize the model and some proofs in the theorem prover Isabelle.

2011

Chargement

, , , ,

We expose the vulnerability of an emerging wireless ranging technology, impulse radio ultra-wide band (IR-UWB), to distance-decreasing attacks on the physical communication layer (PHY). These attacks violate the security of secure ranging protocols that allow two wireless devices to securely estimate the distance between them, with the guarantee that the estimate is an upper-bound on the actual distance. Such protocols serve as crucial building blocks in security-sensitive applications such as location tracking, physical access control, or localization. Prior works show the theoretical possibility of PHY attacks bypassing cryptographic mechanisms used by secure ranging protocols. They also demonstrates that for physical layers used in ISO 14443 RFID and wireless sensor networks, some PHY attacks are indeed feasible. IR-UWB was proposed as a possible solution, but we show that the de facto standard for IR-UWB, IEEE 802.15.4a, does not automatically provide security against such attacks. We find that with the mandatory modes of the standard an external attacker can decrease the measured distance by as much as 140 meters with a high probability (above 99%).

2010

Chargement

Short 2-Move Undeniable Signatures

Jean Monnerat, Serge Vaudenay

Attempting to reach a minimal number of moves in cryptographic protocols is a quite classical issue. Besides the theoretical interests, minimizing the number of moves can clearly facilitate practical implementations in environments with communication constraints. In this paper, we offer a solution to this problem in the context of undeniable signatures with interactive verification protocols by proposing a way to achieve these protocols in 2 moves. To this goal, we review a scheme we proposed at Asiacrypt 2004 whose property is the full scalability of the signature length against security. We slightly modify (to make it non-transferable) a 2-move version of this scheme which was mentioned in the original article without a proof of security. In the random oracle model, we prove the security of the modified version against an active adversary and precisely assess the security in terms of the signature length. To the best of our knowledge, this scheme is the first 2-move undeniable signature scheme with a security proof.

2006

Chargement