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:
Our team has an Inria PhD fellowship topic on Speeding up Theorem Proving with Property-Based Testing. The deadline for applications is May 2.
We are seeking interns
17 July 2013
11 June 2013
25 March 2013
We have a post-doctoral researcher position focusing on Formal Analysis for Security APIs available.
5 March 2013
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.