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 cryptographic 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 currently receives funding from the following projects:
- ERC project CRYSP (259639)
- ANR project AnaStaSec
- ANR project AJACS
- DGA project Analyse de sécurité des interfaces de programmation
How to find us
We are located at 23 Avenue d'Italie, 75013 Paris, France (Google map) and our office is accessible as follows:
Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice wins a best paper award at ACM CCS 2015
We are seeking interns
New release of CryptoVerif, version 1.21
Logjam Attack: How Diffie-Hellman Fails in Practice
New release of ProVerif, version 1.90
Messy State of the Union wins a Distinguished Paper award at IEEE S&P (Oakland) 2015
We are hosting the IETF TLS Interim October meeting in Paris on 21-22 October 2014.
Software and Tools
- F*: Verification system for ML turned proof assistant
- CryptoVerif: A computational protocol verifier
- ProVerif: A symbolic protocol verifier
- miTLS: A verified reference TLS implementation
- SMACK-TLS: State Machine AttaCKs on TLS
- QuickChick: Property-based testing for Coq
- F7: Security type-checker
- Tookan: A symbolic security API analyser.
- WebSpi: A web security verifier
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.