CTL
29 January 2016 - 10h00
Methods for cryptographic protocol verification in the computational model (Phd Defense)
by Mathilde Duclos from Université Grenoble-Alpes
Abstract: Security proofs for cryptographic systems can be carried out in different models which
reflect different kinds of security assumptions. In the symbolic model, an attacker cannot
guess a secret at all and can only apply a pre-defined set of operations, whereas in the
computational model, he can hope to guess secrets and apply any polynomial-time opera-
tion. Security properties in the computational model are more difficult to establish and to
check.
During this work, we improved a framework for certified proofs of computational in-
distinguishability, written using the Coq proof assistant, and based on cil, a specialized
logic for computational frames that can be applied to primitives and protocols. We de-
monstrate how cil and its Coq-formalization allow proofs beyond the classical black-box
security framework, where an attacker only uses the input/output relation of the system
by executing on chosen inputs without having additional information on the state.
We enlarged cil to take into account other model derived from the computational
model. Specifically, we adapt it to include information leakage from honest machine in
the model such that the adversary can retrieve some secret data. This model is called the
bounded storage memory model. We illustrate this improvement on the security proof of
an intrusion-resilient key exchange protocol. We choose to model the intrusion outside of
the logic itself so that cil would keep a broad and non specific usage.
With this strategy, we show that one may model information leakage from honest
machines (and possibly other specificity of other models) without any major modification
of cil. The intrusion is modeled at the core of the proof, while keeping the proof simple
to the user. This method is meant to be adaptive to other security models and is the main
concern of this work.
To reach this goal, we developped several general libraries (as distribution over bits-
trings), and procedures allowing the automation of the most trivial parts of the proof.
Moreover, we developed a complex architecture to modelise this protocol proof, which
is built upon the security of several different primitives. The result is a complex proof
constructed from the security statements of these primitives.
Keywords: cryptography, security, proof, formal methods, certification, intrusion resi-
lience, computationnal model, bounded storage memory model, Coq
Composition du jury:
Christine Paulin : Université Paris Sud, INRIA - Saclay, Rapporteur
Véronique Cortier : CNRS, Nancy, Rapporteur
Bruno Blanchet : INRIA Paris - Rocquencourt, Examinateur
Steve Kremer : INRIA Nancy - Grand Est, Examinateur
Jean-François Monin : Université Grenoble-Alpes, Examinateur
Jean-Guillaume Dumas : Université Grenoble-Alpes, Examinateur
Yassine Lakhnech : Université Grenoble-Alpes, Directeur de thèse
Pierre Corbineau : Université Grenoble-Alpes, Co-Directeur de thèse
