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.