About The project
What is SVP?
SVP is a 6-year research project funded by the French National Research Agency (ANR) and the France 2030 strategy under the frameworks of the Priority Research Programs and Equiments (PEPR). In order to find technic and tools offering security guarantees to cryptographic protocols.
Summary
In the field of formal protocol verification, two approaches are traditionally distinguished. The so-called symbolic approach, in which cryptographic details are abstracted, allows automated security analyses. The so-called computational approach, closer to cryptographers, proposes a modeling closer to reality, at the expense of automation. The symbolic and computational approaches are analyzing respectively in batches 1 and 2. The security of the protocols according to their specification is essential, but it is by no means sufficient: certain types of attacks are introduced at the time of the implementation, which is dealt with in work package 3. Finally, work package 4 gathers the applications on which we will rely to validate the techniques and tools mentioned in the previous work packages.
Work package 1.
Obtaining symbolic guarantees at the specification level.
The symbolic approach is well advanced in the research, in particular for the treatment of so-called trace properties such as weak secrecy or authentication. Nevertheless, there are still improvements to be made to better model certain cryptographic primitives, for the verification of properties such as anonymity and non-traceability. The PROVERIF, TAMARIN and DEEPSEC tools will be developed in this sense. Improving the experience is also important for these tools to be adopted by protocol designers. Thus, a protocol verification platform will be developed to translate, from a single language protocol, models for these three complementary verification tools.
Work package 2.
Obtaining computational guarantees at the specification level.
Work package 3.
Obtaining guarantees at the implementation level.
The above-mentioned tools make it possible to establish security proofs for protocol models that can be more or less abstract. In this work package, we are interested in obtaining security guarantees for the implementation of these protocols.
Work package 4.
Application.
This last work package focuses on the application of aforementioned results to several contexts. First, we will focus on some practical use cases: protocols proposed as standards (e.g. for payment or copyright protection), eletronics voting protocols, etc. We will also address some Human aspects related to particular settings, e.g. for disabled persons. At last, we will also derive proofs for cryptographic constructions involved in the design of some primitives.
