- F*: Verification system for ML programs
- CryptoVerif: Cryptographic protocol verifier in the computational model
- ProVerif: Cryptographic protocol verifier in the symbolic model
- miTLS: Verified reference implementation of TLS
- FlexTLS: Testing TLS Implementations
- QuickChick: Property-based testing for Coq
- WebSpi: Web security verifier
- Tookan: Security API analyzer (now Cryptosense startup)
We are always on the lookout for excellent, highly motivated students and young researchers for research internships and PhD, PostDoc, Research Engineer, or Researcher positions. We have external funding for a couple of PhD and PostDoc positions we can fill over several years with significant flexibility and can also support strong candidates for Researcher positions funded and awarded competitively by Inria. The projects to which students and young researchers could currently contribute include:
- F*: From Program Verification System to Proof Assistant (hot topics; website; code; tutorial; paper)
- miTLS*: Attacking and Proving TLS 1.3 Implementations (website; code; papers; sample internship topic)
- Efficient Formally Secure Compilers to a Tagged Architecture
(brief project description; draft paper #1, paper #2, paper #3, code)
- A Verified Browser Security Engine
- Dependable Property-Based Testing (project description; paper #1; paper #2; draft paper #3; code)
If you are interested in applying or have any questions please send us an email at email@example.com and firstname.lastname@example.org. For applying please include your CV, a short description of your research interests, and the emails of one or two people who can act as your references.
How to reach us
We are located at 2 rue Simone Iff, 75012 Paris, France. This address is, however, so new that mapping applications might not know it; if that's the case please use this old equivalent address: 43 Rue du Charolais, 75012 Paris, France. Here are more details.
Inria Prosecco team, Centre de Recherche Inria de Paris, 2 rue Simone Iff, CS 42112, 75589 Paris Cedex 12
Karthik Bhargavan is awarded the Prix Jeune Chercheur Inria – Académie des sciences 2016.
New release of CryptoVerif, version 1.24
Sweet32: Birthday attacks on 64-bit block ciphers in TLS and OpenVPN
New release of ProVerif, version 1.95
Book on ProVerif
Cătălin Hriţcu awarded ERC Starting Grant on
SECOMP: Efficient Formally Secure Compilers to a Tagged Architecture
Karthik Bhargavan is awarded a Microsoft Research Outstanding Collaborator Award
Cătălin Hriţcu awarded ANR JCJC grant on QuickChick project
We're organizing the 2nd IEEE European Symposium on Security and Privacy in Paris, 26-28 April 2017.
Transcript Collision Attacks: Breaking Authentication in TLS, IKE, and SSH wins a best paper award at NDSS 2016
Sloth Attack: Colliding weak hash constructions in TLS, IKE, and SSH.
Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice wins a best paper award at ACM CCS 2015
Logjam Attack: How Diffie-Hellman Fails in Practice
Messy State of the Union wins a Distinguished Paper award at IEEE S&P (Oakland) 2015