Open post-doc/engineer position on Protocol Verification in the Computational Model


The post-doc will work in the Prosecco project of the INRIA Paris research center, located at 2 rue Simone Iff, 75012 Paris (near Gare de Lyon). The Prosecco project offers an exciting research environment. It deals with formal and practical security research on cryptographic protocols, software security, web security, and hardware protection mechanisms. To this end, we design and implement programming languages, formal verification tools, dynamic monitors, testing frameworks, verified compilers, etc.

Planed work

The Prosecco project-team develops CryptoVerif (, a computational security protocol verifier that generates proofs by sequences of games, like the proofs manually written by cryptographers. This verifier is implemented in OCaml.

The post-doc will work on improvements and extensions of CryptoVerif, in the frame of the ANR project TECAP.

Possible work includes:

The post-doc will design, prove correct, and implement these extensions. He/she will obviously publish his/her work in high quality computer science conferences. He/she will collaborate with other members of the team working on CryptoVerif and related topics (Bruno Blanchet, Benjamin Lipp, Karthikeyan Bhargavan).

It is unlikely that he/she will have time to work on all these extensions, they are possible directions among which he/she will be able to choose, and his/her own ideas of possible extensions and research directions will also be most welcome.

We will also consider applications of research engineers. In this case, the design and proof part would mostly be done by other members of the team, and the engineer would focus mainly on the implementation part.

Required expertise

Further information

Bruno Blanchet