@phdthesis{'Duc6',
title = { Methods for cryptographic protocols verification in the computational model },
author = {Duclos, Mathilde},
month = {Jan},
year = {2016},
pages = {151},
school = {Universit\'e Grenoble-Alpes},
team = {PACSS, DCS},
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 operation. 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 indistinguishability, 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 demonstrate 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 developed several general libraries (as distribution over bitstrings), and procedures allowing the automation of the most trivial parts of the proof. Moreover, we developed a complex architecture to model 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.},
}
