Work Package 1 - Obtaining symbolic guarantees.
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.
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 [https://tamarin-prover.github.io/].
le fichier joint proverifhashconsing.tar.gz inclut une version de ProVerif qui utilise la technique de « hash consing » pour réduire la consommation mémoire.
Cependant, il s’agit d’un premier prototype, qui nécessite encore des améliorations avant d’être intégré dans la version diffusée de ProVerif disponible à https://proverif.inria.fr. (GSVerif n’est pas inclut dans le fichier joint : la version standard de GSVerif disponible à https://sites.google.com/site/globalstatesverif/ peut-être utilisée sans changement avec cette version de ProVerif.)
– le lien de l’outil : https://proverif.inria.fr
This report is about Task 3.1, symbolic proof of protocol implementation, and covers results obtained in the Prosecco team and the Spicy team.
Context. Symbolic verification tools have good automation capabilities, but at the cost of a high level of abstraction. As a result, the proven protocol is an abstract version of the protocol that will actually be executed, and there is no formal link between the two.
The aim of Task 3.1 is to bridge this gap by developing ways of formally linking abstract symbolic proofs and concrete proofs of implementations. The ultimate aim is to be able to write models and proofs at the symbolic level, with all the convenience that this brings, in order to obtain more
concrete security guarantees for the actual implementation of the protocol. We present here two main approaches that we are developping in the SVP project.
L’objectif de la tâche 4.3 est d’appliquer nos techniques pour analyser la sécurité des protocoles de vote électronique, les améliorer et mieux comprendre comment formaliser les propriétés souhaitées. Une tâche préliminaire pour cette tâche est d’identifier les études de cas
qui seront considérées. Nous avons choisi des protocoles de vote correspondants à des systèmes déployés :
— protocole de SwissPost, utilisée pour des élections nationales et cantonales en Suisse
— protocole FLEP, utilisé lors des élections législatives en France en 2022 et 2023
— Belenios, protocole conçu et développé par des équipes impliquées dans le projet. La plateforme de vote libre https://vote.belenios.org/admin est utilisée chaque année dans plus de 1000 élections.
L’objet de ce document est de présenter succinctement les réalisations effectuées pour chaque protocole, l’ensemble de ces réalisations consituant la partie technique du livrable 4A.
