SVP PEPR Cybersécurité

PEPR Cybersecurity Security Verification Protocol

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.


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.

Among the existing verification toolsaddressing computational guarantees, we can mention CRYPTOVERIF and EASYCRYPT, both largely developed by the partners of this project.
We wish to continue the development of these tools, but also to develop a new one, SQUIRREL, based on a promising new approach. Our efforts will also focus on the cooperation between these tools, and on their possible extensions in front of the quantum threat.

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.