Prosecco
Software Tools
- HACL*: High-Assurance Cryptographic Library
- F*: Verification system for effectful programs
- CryptoVerif: Cryptographic protocol verifier in the computational model
- ProVerif: Cryptographic protocol verifier in the symbolic model
- miTLS: Verified reference implementation of TLS
- Noise Explorer: design, implementation and verification for Noise handshakes (Symbolic Software startup)
- FlexTLS: Testing TLS Implementations
- Defensive JavaScript: Protect your scripts
- QuickChick: Property-based testing for Coq
- Tookan: Security API analyzer (now Cryptosense startup)
Recruitment
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:
- CryptoVerif: Mechanized Prover in the Computational Model (Postdoc or Research Engineer position)
- miTLS*: Attacking and Proving TLS 1.3 Implementations (website; code; papers)
- Privacy Preserving Machine Learnng
If you are interested in applying or have any questions please send us an email at karthikeyan.bhargavan@inria.fr and bruno.blanchet@inria.fr. 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.
Postal address
Inria Prosecco team, Centre de Recherche Inria de Paris, 2 rue Simone Iff, CS 42112, 75589 Paris Cedex 12
News
November 2020
New release of CryptoVerif, version 2.04
September 2020
New release of ProVerif, version 2.02pl1
June 2019
We have 3 papers at ICFP 2019
May 2019
Our Journey Beyond Full Abstraction paper won a Distinguished Paper Award at CSF 2019
April 2019
We have 2 papers at EuroS&P'19
January 2019
We contributed three talks at Real World Crypto 2019
October 2018
We have a paper at ACM CCS 2018
July 2018
Éric Tanter from University of Chile joins Prosecco as Visiting Professor for 9 months
May 2018
Prasad Naldurg from IBM Research India joins Prosecco as a Visiting Researcher
New release of F*, version 0.9.6.0
December 2017
September 2017
Amal Ahmed from Northeastern University joins Prosecco as Visiting Professor for one year
May 2017
Best paper award at Oakland S&P 2017 for Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate (video)
We have 3 papers at Oakland S&P 2017
April 2017
2nd IEEE European Symposium on Security and Privacy (EuroS&P) that we organized in Paris was an astounding success.
November 2016
Karthik Bhargavan is awarded the Prix Jeune Chercheur Inria – Académie des sciences 2016.
October 2016
Sweet32: Birthday attacks on 64-bit block ciphers in TLS and OpenVPN
Book on ProVerif
August 2016
Cătălin Hriţcu awarded ERC Starting Grant on
SECOMP: Efficient Formally Secure Compilers to a Tagged Architecture
July 2016
Karthik Bhargavan is awarded a Microsoft Research Outstanding Collaborator Award
Cătălin Hriţcu awarded ANR JCJC grant on QuickChick project
June 2016
We have 3 papers at IEEE CSF 2016
February 2016
Transcript Collision Attacks: Breaking Authentication in TLS, IKE, and SSH wins a best paper award at NDSS 2016
January 2016
Karthik Bhargavan awarded ERC Consolidator Grant
miTLS wins the Levchin prize for contributions to real world cryptography
Sloth Attack: Colliding weak hash constructions in TLS, IKE, and SSH.