Prosecco

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.

Scientific goals

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#.
  • Provably secure web applications. We are developing analysis tools and verified libraries to help programmers build provably secure web applications. The tools include: static and dynamic verification tool for client-side JavaScript web applications, annotated JML libraries for verifying the security of Android smartphone applications, and the type systems F7 and F* for verifying clients and servers written in F#.

Further details about our scientific goals can be found in our project proposal.

Funding

Our group receives funding from the following projects:

How to find us

We are located at 23 Avenue d'Italie, 75013 Paris, France (Google map) and our office is accessible as follows: