PhD Defense
Mathieu Baudet
Title of the thesis
Security of cryptographic protocols : logical and computational aspects
Day and location
Tuesday, January 16th 2007, in Cachan at 11am.
Salle de conférences, Pavillon des Jardins, École Normale Supérieure
de Cachan.
Access
Jury
-
Martín ABADI, examiner
-
Bruno BLANCHET, examiner
-
Jean GOUBAULT-LARRECQ, supervisor
-
Ralf KÜSTERS, referee
-
Yassine LAKHNECH, referee
-
Jacques STERN, examiner
Abstract
This thesis is dedicated to the automatic verification of
cryptographic protocols in the logical and computational settings.
The first part concerns the security of procotols in the logical
("formal") framework. To begin with, we show how to specify various
security properties of protocols in a concurrent language, and how to
analyze them automatically for a bounded number of sessions. The properties
under consideration include notably simple
secrecy, authentication and resistance to dictionary attacks.
The second part
deals with the computational soundness of logical models. The main
question here is to what extent the fact that no logical attack exists
on a protocol implies that it is provably secure in the usual
cryptographic model (called the computational model). We
concentrate on static equivalence, applied notably to several kinds of
encryption and data vulnerable to dictionary attacks (such as passwords).
We show that under simple conditions, any (logical) proof
of static equivalence between two messages implies their
(computational) indistinguishability.
This entails computational soundness in the passive case for the notion
of dictionary attacks developped in the first part.
Keywords
Cryptographic protocols, computational soundness of formal methods,
equational theories, process algebras.