My name is Théo Winterhalter and I am a permanent researcher (CR) in Deducteam at Inria Saclay and LMF . Previously I was a postdoctoral researcher at Max Planck Institute for Security and Privacy (MPI-SP) in Bochum (Germany), working with Cătălin Hrițcu . My main interest lies in type theory and its applications to proof assistants. As such, most of my results are formalised in a proof assistant, generally Coq . I strive to make proof assistants better and safer. You can contact me at theo.winterhalter@inr
SSProve is a framework combining high-level modular proofs about composed cryptography protocols with a probabilistic relational program logic to treat lower-level details. All of it is formalised in Coq.
As a stress-test, we formalised in SSProve a security theorem for KEM-DEM. This proof follows the original SSP paper by Brzuska et al. Thanks to our formalisation effort, and in collaboration with the authors, we found a bug in their original theorem. This has led them to update their proof, which we then formalised in full in SSProve.
MetaCoq | Website of the MetaCoq Project
Catalin Hritcu - MPI-SP
ERC SECOMP - Efficient Formally Secure Compilation to a Tagged Architecture
Cezar Andrici
Yannick Forster
Matthieu Sozeau :: News
Ambroise Lafont