Marion Daubignard
Université Joseph Fourier PhD student,
under the direction
of Pr Yassine Lakhnech,
in Laboratoire VERIMAG.
e-mail: prenom . nom @ imag.fr / firstname.name @ imag.fr
Technical report
with proofs of submission to CCS11 !!!
- Year 2010-2011
- Assisting lab work in Algorithmics, first year, first semester,
at ENSIMAG.
- T.A. of Progamming Languages and Compiler Design.
You are recommended to have a look at
the Nielsons' book
Of course, you can also find resources on Pr Mounier's website
- Year 2009-2010
- Assisting lab work in Algorithmics, first year, first semester,
at ENSIMAG.
- T.A. of Progamming Languages and Compiler Design.
- Year 2008-2009
- Assisting lab work in Algorithmics, first year, first semester,
at ENSIMAG.
- Introduction to Computer Science (basics about algorithms and how
to design a website), first year of Biology, Université Joseph Fourier.
- PhD
In a nutshell, my PhD topic consists in studying how to
automate the verification (or synthesis) of proofs of cryptographic
protocols.
Pr Lakhnech, Pr Bruce Kapron,
Pr
Gilles Barthe
and myself are currently developping a logics designed to carry out proofs
of security schemes directly in the computational framework.
The need for this kind of formal tools to help clarify
proofs of security is now widely accepted in the community
(e.g., see [Halevi'05]).
As a lot of security notions are defined in terms of
indistinguishability and negligibility of events, this is the kind
of statements the logics addresses. It allows to state exact security
results for active adversaries.
Called CIL, for Computational Indistinguishability Logic,
the logic is independent from any specific computational hypothesis or
general paradigm (e.g. the Random
Oracle Model), though those
can be plugged in to close branches of proof trees if needed.
CIL does not depend on a particular form of programming language. We believe
this versatility and the generality of the logic rules will allow
to carry out a lot of proofs in CIL.
Proofs have been designed already for IND-CPA security of OAEP, the FDH
signature scheme, PSS, and IND-CCA security of OAEP in undergoing work.
CIL was presented at CCS'10, you can find the final version of the paper here .
Slides from talks about CIL:
- at the Formacrypt meeting in Paris in June '09: slides
- at the ECRYPT summer school on provable security in Sept.'09: slides
Part of my work is supported by the ANR project SCALP.
In this framework, I have the opportunity
to interact and help formalize CIL in the french proof assistant
Coq.
- Other papers:
- to appear, LPAR-16 : An equational logic for probabilistic terms.
- Automation of Proofs for Assymetric Encryption
- Game-Based Criterion Partition Applied to Computational Soundness of Adaptive Security, here