Oct 06

Séminaire de Crypto de l’ENS : A Decision Procedure for Trace Equivalence

Programme du séminaire Cryptographie
Ecole Normale Supérieure — 45, rue d'Ulm — Paris 5me


Conférencier : Vincent Cheval – ENS Cachan

Date : Jeudi 13 octobre 2011, 11 heures
École Normale Supérieure, Amphi Évariste Galois – NIR

Title: A Decision Procedure for Trace Equivalence

Abstract: We consider security properties of cryptographic protocols
that can be modeled using the notion of trace equivalence.
The notion of equivalence is crucial when specifying privacy-type
properties, like anonymity, vote-privacy, and unlinkability.
In this paper, we give a calculus that is close to the applied
pi calculus and that allows one to capture most existing protocols
that rely on classical cryptographic primitives.
First, we propose a symbolic semantics for our calculus relying
on constraint systems to represent infinite sets of possible traces,
and we reduce the decidability of trace equivalence to deciding a
notion of symbolic equivalence between sets of constraint systems.
Second, we develop an algorithm allow- ing us to decide whether
two sets of constraint systems are in symbolic equivalence or not.
Altogether, this yields the first decidability result of trace
equivalence for a general class of processes that may involve
else branches and/or private channels (for a bounded number
of sessions).