Publication

Equivalences and calculi for formal verification of cryptographic protocols

Related publications (78)

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Chaum's Designated Confirmer Signature Revisited

Serge Vaudenay, Jean Monnerat

This article revisits the original designated confirmer signature scheme of Chaum. Following the same spirit we naturally extend the Chaum's construction in a more general setting and analyze its security in a formal way. We prove its security in the rando ...

2005

On Bisimulations for the Spi Calculus

Johannes Borgström

The spi calculus is an extension of the pi calculus with cryptographic primitives, designed for the verification of cryptographic protocols. Due to the extension, the naive adaptation of labeled bisimulations for the pi calculus is too strong to be useful ...

2004

Concurrency Combinators for Declarative Synchronization

Developing computer systems that are both concurrent and evolving is challenging. To guarantee consistent access to resources by concurrent software components, some synchronization is required. A synchronization logic, or policy, is at present entangled i ...

Springer2004

Data-Aware Multicast

Rachid Guerraoui, Patrick Eugster

This paper presents a multicast algorithm for peer-to-peer dissemination of events in a distributed topic-based publish-subscribe system, where processes publish events of certain topics, organized in a hierarchy, and expect events of topics they subscribe ...

2004

On Bisimulations for the Spi Calculus

Johannes Borgström

2003

Modeling Consensus in a Process Calculus

Rachele Fuzzati, Massimo Merro

We give a process calculus model that formalizes a well-known algorithm (introduced by Chandra and Toueg) solving consensus in the presence of a particular class of failure detectors; we use our model to formally prove that the algorithm satisfies its spec ...

2003

Modeling Consensus in a Process Calculus

Rachele Fuzzati, Massimo Merro

We give a process calculus model that formalizes a well known algorithm (introduced by Chandra and Toueg) solving consensus in the presence of a particular class of failure detectors (Diamond S); we use our model to formally prove that the algorithm satisf ...

2003

Mobility Helps Security in Ad Hoc Networks

Jean-Pierre Hubaux, Levente Buttyan, Srdan Capkun

Contrary to the common belief that mobility makes security more difficult to achieve, we show that node mobility can, in fact, be useful to provide security in ad hoc networks. We propose a technique in which security associations between nodes are establi ...

2003

Data-Aware Multicast

Rachid Guerraoui, Patrick Eugster

2003

Building blocks for secure services

Levente Buttyan

This thesis is concerned with two security mechanisms: authenticated key transport and rational exchange protocols. These mechanisms are potential building blocks in the security architecture of a range of different services. Authenticated key transport pr ...

EPFL2002