!!Provably secure systems: foundations, design, and modularity
February 2011 - January 2016

Our research project ProSecure is supported by the [European Research Council|http://erc.europa.eu/] ("Starting Grant Project"). This is a long-term project (5 years) aiming at developping provably secure systems such as security protocols.

!Context of the project
Security protocols are short distributed computer programs dedicated to securing communications on 
digital networks. They are designed to achieve various goals such as data privacy and data authenticity, 
even when communication channels are controlled by malicious users. Their increasing penetration 
in many important applications makes it a very important research challenge to design and establish 
security properties. In the last decade, formal approaches and automated verification techniques have 
been successfully applied for detecting potential attacks. However, the security guarantees obtained so 
far usually hold in a rather abstract model, and are limited to isolated specific protocols analyzed for a 
few set of specific security properties. Moreover new types of protocols are still emerging in order to 
face new technological and societal challenges.

!Goals of the project
The goal of the project is to propose foundations for a careful analysis and design of large classes of up-to-date protocols. We plan to develop general verification techniques for new classes of protocols that are of primary interest in nowadays life like e-voting protocols, routing protocols or APIs. Our techniques will first be developed in symbolic models where messages are represented by terms but we will also consider the cryptographic part of the primitives that are used in such protocols (encryption, signatures, ...), obtaining higher security guarantees. We aim at proposing modular results both for the analysis and design of protocols. As a particular outcome, we should characterize simple design principles that ease the analysis (thus the security) of protocols and discard families of attacks.

!Research themes

* Security protocols: authentication and confidentiality protocols, e-votings, security APIs, routing protocols
* Automatic verification: rewriting, constraint solving, automatic deduction
* Provable security


* [Vincent Cheval|http://www.loria.fr/~chevalvi/] (permanent researcher)
* [Rémy Chrétien|http://www.lsv.ens-cachan.fr/~chretien/] (PhD student)
* [Véronique Cortier|http://www.loria.fr/~cortier/] (permanent researcher, __principal investigator of the project__)
* [Catalin Dragan|http://students.info.uaic.ro/~constantin.dragan/] (postdoc)
* [Jannik Dreier|http://www.loria.fr/~jdreier/] (permanent researcher)
* [Stéphane Glondu|http://stephane.glondu.net/] (engineer)
* [Steve Kremer|http://www.loria.fr/~skremer/] (permanent researcher)
* [Éric Le Morvan|http://www.loria.fr/~elemorva/] (PhD student)
* [Mathieu Turuani|http://www.loria.fr/~turuani/] (permanent researcher)

!Former members

* Jérémy Dubut (as internship)
* Alexandre Debant (as internship)
* Jan Degrieck (as Master internship)
* [Mounira Kourjieh|http://www.loria.fr/~kourjiem/] (as post-doc)
* [David Galindo|http://www.dgalindo.es/] (researcher)
* Joseph Lallemand (as Master internship)
* [Malika Izabachene|http://www.lsv.ens-cachan.fr/~izabache/] (post-doc)
* Joseph Lallemand (Master internship)
* Antoine Plet (as internship)
* [Guillaume Scerri|http://www.lsv.ens-cachan.fr/~scerri/] (PhD student)
* [Ben Smyth|http://www.bensmyth.com/] (as post-doc)
* [Cyrille Wiedling|http://www.loria.fr/~wiedling/] (PhD student)

!Visiting researchers

* [Myrto Arapinis|http://www.cs.bham.ac.uk/~arapinmd/]
* [David Galindo|http://www.dgalindo.es/] 
* [Zhiwei Li|http://webpages.uncc.edu/~zli19/]
* [Graham Steel|http://www.lsv.ens-cachan.fr/~steel/]
* [Bogdan Warinschi|http://www.cs.bris.ac.uk/~bogdan/]