CTL
12 janvier 2012 - 14h00
Formalisation de preuves de sécurité concrète (Phd Defense)
par Marion DAUBIGNARD de VERIMAG
Abstract: In this thesis, we address the lack of formalisms to carry out
concrete security proofs.
Our contributions are threefold.
First, we present a logic, named Computational Indistinguishability
Logic (CIL), for reasoning about cryptographic systems. It consists
in a small set of
rules capturing reasoning principles common to many
proofs.
Their formalization relies
on classic tools such as bisimulation
relations and contexts.
Second, and in order to increase proof automation,
it presents a Hoare logic dedicated to asymmetric encryption
schemes in the Random Oracle Model that yields an
automated and sound verification method.
It has been successfully applied to existing
encryption schemes.
Third, it presents a general reduction theorem for proving
indifferentiability of iterative hash constructions from a random
oracle. The theorem is proven in CIL demonstrating the
usefulness of the logic and has been applied to constructions
such as the SHA-3 candidate Keccak
and the Chop-MD construction.
Jury:
Advisor Pr. Y. Lakhnech
Reviewer Dr. S. Kremer
Reviewer Dr. D. Pointcheval
Reviewer Dr. B. Warinschi
Dr. G. Barthe
Dr. E. Bresson
Dr. A. Datta
Pr. B. Kapron
Dr. P. Lafourcade
