SVP PEPR Cybersécurité

PEPR Cybersecurity Security Verification Protocol


Work Package 1 - Obtaining symbolic guarantees.

SVP jalon 0B

Cryptography secures our online  interactions, transactions, and trust. To achieve this goal, not only do the cryptographic primitives and protocols need to be secure in theory, they also need to be securely implemented by cryptographic library developers in practice.
However, implementing cryptographic algorithms securely is challenging, even for skilled professionals, which can lead to vulnerable implementations, especially to side-channel attacks. For timing attacks, a severe class of side-channel attacks, there exist a multitude of tools that are supposed to help cryptographic library developers assess whether their code is vulnerable to timing attacks. Previous work has established that despite an interest in writing constant-time code, cryptographic library developers do not routinely use these tools due to their general lack of usability. However, the precise factors affecting the usability of these tools remain unexplored. While many of the tools are developed in an academic context, we believe that it is worth exploring the factors that  contribute to or hinder their effective use by cryptographic library developers.
To assess what contributes to and detracts from usability of tools that verify constant-timeness (CT), we conducted a two-part usability study with 24 (post) graduate student participants on 6 tools across diverse tasks that approximate real-world use cases for cryptographic library developers.
We find that all studied tools are affected by similar usability issues to varying degrees, with no tool excelling in usability, and usability issues preventing their effective use.
Based on our results, we recommend that effective tools for verifying CT need usable documentation, simple installation, easy to adapt examples, clear output corresponding to CT violations, and minimal noninvasive code markup. We contribute first steps to achieving these with limited academic resources, with our documentation, examples, and installation scripts.


SVP jalon 1A

Symbolic protocol verification generally abstracts probabilities away, considering computations that succeed only with negligible probability, such as guessing random numbers or breaking an encryption scheme, as impossible. This abstraction, sometimes referred to as the perfect cryptography assumption, has shown very useful as it simplifies automation of the analysis. However, probabilities may also appear in the control flow where they are generally not negligible. In this paper we consider a framework for symbolic protocol analysis with a probabilistic choice operator: the probabilistic applied pi calculus. We define and explore the relationships between several behavioral equivalences. In particular we show the need to require randomized schedulers – indeed we exhibit a counter-example to one of the main results in a previous work that relied on non-randomized ones. As in other frameworks that mix both non-deterministic and probabilistic choices, schedulers may sometimes be unrealistically powerful. We therefore consider two subclasses of processes that avoid this problem. When considering purely non-deterministic protocols, as is done in classical symbolic verification, we show that a probabilistic adversary has—maybe surprisingly—a strictly superior distinguishing power for may testing, which, when the number of sessions is bounded, we show to coincide with purely possibilistic similarity.
Finally, we consider fully probabilistic protocols and show that trace equivalence corresponds to a notion of may testing with purely probabilistic attackers. We also briefly discuss complexity and automation for these subclasses when the number of sessions is bounded.

Sapic+: protocol verifiers of the world, unite!


Symbolic security protocol verifiers have reached a high degree of automation and maturity. Today, experts can model real-world protocols, but this often requirqes model-specific encodings and deep insight into the strengths and weaknesses of each of those tools. Sapic+ is a protocol verification platform, designed by Cheval, Jacomme, Kremer and Künnemann, that lifts this burden and permits choosing the right tool for the job, at any development stage. It provides automated translations from Sapic+ to Tamarin, ProVerif and DeepSec. We prove each part of these translations sound. A user can thus, with a single Sapic+ file, verify reachability and equivalence properties on the specified protocol, either using ProVerif, Tamarin or DeepSec. Moreover, the soundness of the translation allows to directly assume results proven by another tool which allows to exploit the respective strengths of each tool. We demonstrate our approach by analyzing various existing models.  This includes, among others, a large case study of the 5G authentication protocols, previously analyzed in Tamarin. Encoding this model in Sapic+ we demonstrate the effectiveness of our approach. The Sapic+ platform is completely integrated in, and distributed with the open source Tamarin prover [].

SVP jalon 1B