Publication

How to specify and how to prove correctness of secure routing protocols for MANET

Publications associées (45)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

Formal Analysis of Secure Neighbor Discovery in Wireless Networks

Jean-Pierre Hubaux, Panagiotis Papadimitratos, 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 propagatio ...

Ieee Computer Soc2013

We define a new primitive, input-aware equivocable commitment, baring similar hardness assumptions as plaintext-aware encryption and featuring equivocability. We construct an actual input-aware equivocable commitment protocol, based on a flavor of Diffie-H ...

Springer2013

Speculative Linearizability

Rachid Guerraoui, Viktor Kuncak, Giuliano Losa

Linearizability is a key design methodology for reasoning about implementations of concurrent abstract data types in both shared memory and message passing systems. It provides the illusion that operations execute sequentially and fault-free, despite the a ...

Assoc Computing Machinery2012

Model Checking Security Protocols: A Multiagent System Approach

Security protocols specify the communication required to achieve security objectives, e.g., data-privacy. Such protocols are used in electronic media: e-commerce, e-banking, e-voting, etc. Formal verification is used to discover protocol-design flaws. In t ...

Imperial College London2011

Secure Neighbor Discovery and Ranging in Wireless Networks

Marcin Poturalski

This thesis addresses the security of two fundamental elements of wireless networking: neighbor discovery and ranging. Neighbor discovery consists in discovering devices available for direct communication or in physical proximity. Ranging, or distance boun ...

EPFL2011

Formal Analysis of Secure Neighbor Discovery in Wireless Networks

Marcin Poturalski

2011

To aid the formal verification of fault-tolerant distributed protocols, we propose an approach that significantly reduces the costs of their model checking. These protocols often specify atomic, process-local events that consume a set of messages, change t ...

IEEE2011

, ,

This paper experimentally studies the reliability and delay of flooding based multicast protocols for a sniper detection application. In particular using an emulator it studies under which conditions protocols based on network coding deliver performance im ...

2011

Zebrafish: Methods and Protocols

In the last 20 years, research activity using the zebrafish Danio rerio has increased dramatically, due in part to the ease of breeding and raising them, their genetic tractability, embryonic accessibility, and their imaging potential. In Zebrafish: Method ...

Humana Press2009

, ,

In wireless systems, neighbor discovery (ND) is a fundamental building block: determining which devices are within direct radio communication is an enabler for networking protocols and a wide range of applications. To thwart abuse of ND and the resultant c ...

2008