# Official LSV Web Site

# PhD Thesis Defense

## Author: Ștefan Ciobâcă

## Thesis: Automated Verification of Security Protocols with Appplications to Electronic Voting

### Manuscript

The thesis manuscript is available

here.

### Time and Date

Friday, December 9th, 2011 at 10:00 A.M.

Salle Condorcet, bâtiment d'Alembert

École Normale Supérieure de Cachan

61, avenue du Président Wilson
94235 CACHAN Cedex, France

### Jury

Bruno Blanchet (reviewer)

Véronique Cortier (advisor)

Thomas Genet (examiner)

Steve Kremer (advisor)

Jean Goubault-Larrecq (advisor)

Jean-Jacques Lévy (examiner)

Luca Viganò (reviewer)

### Abstract

This thesis is about the formal verification and composition
of security protocols, motivated by applications to electronic voting
protocols. Chapters 3 to 5 concern the verification of security
protocols while Chapter 6 concerns composition. We show in Chapter 3
how to reduce certain problems from a quotient term algebra to the
free term algebra via the use of strongly complete sets of
variants. We show that, when the quotient algebra is given by a
convergent optimally reducing rewrite system, finite strongly complete
sets of variants exist and are effectively computable. In Chapter 4,
we show that static equivalence for (classes of) equational theories
including subterm convergent equational theories, trapdoor commitment
and blind signatures is decidable in polynomial time. We also provide
an efficient implementation. In Chapter 5 we extend the previous
decision procedure to handle trace equivalence. We use finite strongly
complete sets of variants introduced in Chapter 3 to get rid of the
equational theory and we model each protocol trace as a Horn theory
which we solve using a refinement of resolution. Although we have not
been able to prove that this procedure always terminates, we have
implemented it and used it to provide the first automated proof of
vote privacy of the FOO electronic voting protocol. In Chapter 6, we
study composition of protocols. We show that two protocols that use
arbitrary disjoint cryptographic primitives compose securely if they
do not reveal or reuse any shared secret. We also show that a form of
tagging is sufficient to provide disjointness in the case of a fixed
set of cryptographic primitives.

### Getting to ENS Cachan

How
to get to ENS Cachan (french)
##### From nearest RER station to ENS Cachan:

Google Maps walk from Bagneux to ENS Cachan
##### Campus map:

Map of campus (pdf)
The defense is in "batiment d'Alembert", a building denoted (1) appearing in blue on the campus map. To get
to the Condorcet room, climb up the horseshoe entrance, climb up one
floor and make a right turn. The Condorcet room is at the end of the
corridor.
The "pot" will be on the gorund floor of " PdJ", a building denoted (5) appearing in green on the campus map.