soutenance de thèse

Bonjour à tous,

j'ai le grand plaisir de vous inviter à ma soutenance de thèse
le 11 janvier à 14h à l'antenne parisienne de INRIA, salle Orange (la
pièce jointe explique comment s'y rendre).

A bientôt!
Nataliya

Titre: Auditability for Security Protocols
Jury:
 Gilles Barthe (rapporteur)
 Robert Harper (rapporteur)
 Roberto Di Cosmo
 Cédric Fournet
 Carl Gunter
 Francesco Zappa Nardelli

Résumé:
Security protocols often log some data available at runtime for an
eventual a posteriori analysis, called audit. In practice, audit
procedures remain informal, and the choice of log contents is left to
the programmer's common sense. The goal of this dissertation is to
formalize and verify the properties expected from audit logs.

First we consider the use of logs in so called optimistic security
protocols which, as opposed to classic security protocols, rely on the
logs to postpone certain security checks until the end of execution.
We formally study two optimistic schemes: value commitment scheme and
offline e-cash; using process languages techniques, we prove that the
information logged by their implementations suffices to detect the
cheat of participants, if any.

Then we define auditability as the ability of a protocol to collect
enough evidence to convince an audit procedure (judge). We propose a
method based on types with logical refinements to verify auditability,
and implement it as an extension to an existing typechecker. We show
that verifying auditability boils down to typechecking the protocol
implementation. We also implement logical support for generic pre- and
post-conditions to enhance modular typechecking of higher-order
functions.