Tools for automated, symbolic analysis of real-world cryptographic protocols – ASAP

Our techniques stem from different areas: automated reasoning, concurrency theory and more generally automated verification. The work on the ProVerif tool did indeed benefit from advances in automated deduction, namely feature vector indexing allowing efficient set-to-clause subsumption proposed by Schulz a few years ago. Our work on equivalences in a probabilistic applied pi calculus builds on a large body of existing results as we express our semantics in terms of general probabilistic and non-deterministic transition systems. Finally, the theory of SAPIC+ builds on classical process calculi semantics, as studied in concurrency theory.

We did study probabilistic process equivalences for security protocols and propose a new setting where protocols and attackers may use probabilistic control flow. We show that for the class of protocols that do not make any probabilistic choices, but allow the attacker to do so, the resulting may testing equivalence is strictly stronger by allowing a probabilistic attacker. For a bounded number of sessions may-testing with a probabilistic attacker coincides with purely possibilistic similarity. Also, we consider a class of simple processes, with a very limited non-determinism. For this class, we show that trace equivalence coincides with may-testing where attackers are sequential processes.

We have conducted a major revision of the popular ProVerif tool improving expressivity and automation. Its efficiency has been considerably improved using techniques from automated deduction to speed up subsumption checks. On average, ProVerif is now 10 to 50 times faster than its previous release. We also integrated into TAMARIN a protocol verification platform dubbed SAPIC+ that allows users to compile a common input language to 3 state-of-the-art verification tools: TAMARIN, ProVerif and DeepSec. Our correctness proofs guarantee that results from one tool can be used in any of the other tools. To demonstrate its usefulnes we ported (among others) the existing TAMARIN model of the complex 5G authentication protocols case study to SAPIC+: dedicated, handwritten oracles used to automate proofs in TAMARIN carried over straightforwardly, and verification time was preserved, which shows the efficiency of the generated model.

We conducted several case studies. We made an in-depth analysis of the Belenios e-voting protocol with a much more detailed model than usually considered. The analysis unveils unknown flaws in some corruption scenarios. We propose fixes and prove them to be secure. The SwissPost e-voting system is currently proposed under the scrutiny of the community, before being deployed in 2022 for political elections in several Swiss cantons. We explain how real world constraints led to shortcomings that allowed a privacy attack to be mounted. This flaw has been acknowledged by Swiss Post, made public, and the system will be patched to prevent the problem. We have worked on a detailed formal analysis of ZCash, a specification and implementation of a decentralized anonymous payment scheme. Although ProVerif is routinely used for the analysis of large, real-life cryptographic protocols this case study pushed the tool to its limits. As a result we added optimizations that speed up verification and improve memory consumption. Finally, we used SAPIC+ for an extensive formal verification of the LAKE-EDHOC protocol, an authentication protocol for IoT, currently under a standardization process.

We continue our tool developments by applying the tools to ambitious case studies. The analyses of the LAKE-EDHOC standard and the ZCash specification are still in progress. They allow to identify limitations of current tools and improvements to be made. In particular SAPIC+ will need to gain in maturity to become a usable platform. Motivated by our work on equivalences in a probabilistic applied pi calculus we plan to integrate in DEEPSEC the verification of the similarity process equivalence and an extension for probabilistic processes. During the verification of LAKE-EDHOC we identified the need to verify a liveness properties (to verify non-repudiation). A similar problem arises in e-voting when accountability is required. This is currently out of the scope of ProVerif, and we will work on extending ProVerif to provide at least a limited support for such properties. We will also work on improving automation in Tamarin: in particular we will improve the built-in heuristics and better support for «oracles« that allow a user to specify dedicated, fine-tuned heuristics.

1. ProVerif with Lemmas, Induction, Fast Subsumption, and
Much More. Bruno Blanchet, Vincent Cheval, and Véronique
Cortier. In Proceedings of the 42nd IEEE Symposium on Security
and Privacy (S&P'22), IEEE Computer Society Press, 2022.
hal.inria.fr/hal-03366962v1

2. A privacy attack on the Swiss Post e-voting system.
Véronique Cortier, Alexandre Debant, and Pierrick Gaudry. In
Real World Crypto Symposium (RWC'22), Amsterdam,
Netherlands, 2022. hal.inria.fr/hal-03446801/

Cryptographic protocols are an essential building block to secure online communications. Relying on cryptographic primitives, such as encryption and digital signatures, these protocols typically guarantee security properties such as confidentiality and authenticity of communications. These properties are for instance basic goals of TLS, the most widely deployed cryptographic protocol, underlying all https Internet connections. Many modern applications may also need to guarantee properties related to users' privacy: such properties include anonymity and unlinkability (users cannot be traced) properties.

History has however shown that cryptographic protocols are very error-prone and attackers have been able to exploit design and implementation flaws. The difficulty of designing and deploying secure protocols comes from an inherent asymmetry in security: while a protocol designer needs to think about all possible attacks, an attacker only needs to find a single weakness. Even on rather simple protocols, it is difficult for a human to explore all possible cases in a security proof when we take into account an attacker that has control of the underlying communication network and can intercept, modify and insert messages, in addition to the concurrent nature of the protocols. This task is even more complicated when requiring strong security properties that hold, or guaranteeing at least a degraded form of security, when parts of the system under study have been compromised. Therefore, it is essential to design algorithms that are able to automate security proofs, or automatically detect attacks in protocols. This approach, where messages are represented as first-order terms, in a symbolic model, was pioneered by Dolev and Yao and has been extremely successful, e.g., when analyzing new, upcoming security standards such as TLS 1.3 or 5G.

The goal of this project is the development of efficient algorithms and tools for automated verification of cryptographic protocols, that are able to comprehensively analyse detailed models of real-world protocols building on techniques from automated reasoning. Automated reasoning is the subfield of AI whose goal is the design of algorithms that enable computers to reason automatically, and these techniques underlie almost all modern verification tools. Current analysis tools for cryptographic protocols do however not scale well, or require to (over)simplify models, when applied on real-world, deployed cryptographic protocols. We aim at overcoming these limitations: we therefore design new, dedicated algorithms, include these algorithms in verification tools, and use the resulting tools for the security analyses of real-world cryptographic protocols. The resulting tools will have increased efficiency, better automation and a wider scope. These developments will be driven by and validated on three classes of protocols: e-voting protocols, protocols for mobile devices from the 5G standard, and protocols for modern messaging applications, in particular the NOISE protocol framework.

Our research is driven by the development of verification tools and their application to real-life protocols. Developing efficient, usable tools requires to develop solid, theoretical foundations, on the one hand, and evaluation on real-life case studies, on the other hand, to understand their limitations in practice. Our project will therefore be structured around the development of several, complementary tools that are developed in the PESTO research team, headed by Steve Kremer. On a more technical side, the methods developed in the project include symbolical reasoning on partially ordered traces, new algorithms for efficient subsumption in first-order Horn clause resolution, the design of equational reasoning techniques to enable support of associative, commutative operators and heuristics for guiding the state exploration to favor termination.