Prosecco is a research team (équipe) at INRIA Paris-Rocquencourt that focuses on building and verifying programs that use cryptography. Our target applications include cryptographic protocol implementations (e.g., TLS), hardware-based security APIs (e.g., Smartcards), smartphone- and browser-based web applications (e.g., Facebook), and cloud-based web services (e.g. Dropbox). Our analysis techniques include dependent type systems, symbolic and computational cryptographic protocol verifiers, general-purpose theorem provers, formal testing frameworks, and run-time analysis tools.
Ultimately, our goal is to help developers to program securely with cryptography and, to achieve this objective, we are actively researching the following key areas:
- Symbolic verification of cryptographic applications. We are developing verification tools for models and implementations of cryptographic protocols and security APIs using symbolic verification techniques. Our tools include: the specialized cryptographic prover ProVerif, the reverse engineering and formal test tool Tookan, and the security type systems F7 and F* for the programming language F#.
- Computational verification of crytpographic applications. In addition to the development of symbolic tools, we are also developing tools using computational verification techniques. Our tools include: the computational prover CryptoVerif and the computationally sound type system Computational F7 for applications written in F#.
Further details about our scientific goals can be found in our project proposal.
Our group receives funding from the following projects:
- ANR project VERSO ProSe
- DGA project Analyse de sécurité des interfaces de programmation
- ERC project CRYSP (259639)
- FUI project PISCO
How to find us
We are located at 23 Avenue d'Italie, 75013 Paris, France (Google map) and our office is accessible as follows:
We are organizing The Joint EasyCrypt-F*-CryptoVerif School 2014 in Paris on 24-28 November 2014. Registration is free and open!
We presented our Triple Handshake attacks to the TLS Working Group at IETF'89 and proposed a new countermeasure
We had one paper at NDSS 2013
Our team has an Inria PhD fellowship topic on Speeding up Theorem Proving with Property-Based Testing. The deadline for applications is May 2.
Mozilla issued CVE-2014-1491 in response to our vulnerability report.
We are seeking interns
The following positions are currently open:
- 2x Post-doctoral researcher (1-2 year)
- 2x Ph.D. studentships (3 year)
- 3x Masters internships (6 months)
- 3x Internships for Ph.D. students, masters students, and undergraduates (2-3months)
Applicants should have a strong interest on topics in hardware and software security, cryptography, formal verification, and program analysis. One of the post-doctoral positions focuses on Formal Analysis for Security APIs and one of the intern positions focuses on Hardware-based Privilege Separation for Cryptographic Protocol Implementations; we are also seeking post-doctoral researchers and interns who propose their own projects in alignment with our research interests. Positions will be kept open until filled. To apply email any one of the group members with your CV and the name of two references.