David Cadé

Version française
I am a PhD student working in the computer security team Prosecco at INRIA Paris-Rocquencourt, and supervised by Bruno Blanchet.

Publications

From Computationally-Proved Protocol Specifications to Implementations and Application to SSH
This publication to JoWUA is a joint work with Bruno Blanchet. It is an extension of the ARES article.
Proved Generation of Implementations from Computationally-Secure Protocol Specifications
This publication to POST '13 is a joint work with Bruno Blanchet. We present the proof of correctness of our compiler that generates an OCaml implementation from a CryptoVerif specification. Full version with proofs.
From Computationally-proved Protocol Specifications to Implementations
This publication to ARES '12 is a joint work with Bruno Blanchet. We present our compiler that generates an OCaml implementation from a CryptoVerif specification, and an application of this on the SSH protocol.
From CryptoVerif Specifications to Computationally Secure Implementations of Protocols (Work in Progress)
This has been published at FCC '09 and is an abstract presenting the work I did in my internship in 2009.
Traductions de spécifications en implémentations de protocoles
This is the report for my internship supervised by Bruno Blanchet in 2009.
Isotopic Meshing of Intersection of Implicit Surfaces in Higher Dimension
This is the report for my internship supervised by Gert Vegter in 2008.
Réduction de réseaux euclidiens : vers un code fiable, souple et puissant
This is the report for my internship supervised by Damien Stehlé in 2007.

Contact

INRIA
23 avenue d'Italie
75013 Paris

Email: david<dot>cade<at>inria<dot>fr
Office: Fifth floor, office 13