The team organizes as often as possible seminars related to formal methods and security. Most of the talks present the latest results obtained by the different members of the team but invited speakers are also welcome.
Upcoming talks
Maïwenn Racouchot
Date: November, 17th 2023 – 10:30 am
Place: B013
Title: A UC analysis of Android Protected Confirmation
Abstract: Today, smartphones allow their user to use sensitive services and perform very sensitive transactions. For example, services like Google Pay make it possible to use the phone as a credit card. To secure this type of operation, Trusted Execution Environments (TEEs) have been added to the phone’s processor. This environment is isolated from the rest of the RichOS (ROS) and can securely store data and run honest code even if the rest of the phone is corrupted. However, more and more applications could use the benefits of having access to the TEE but not all of them have trusted code. To remedy this problem, Android is currently working with Google on a new protocol called Protected Confirmation. The goal of this protocol is to give to any server using it a way to verify that the transaction that they are receiving have been seen and accepted by the user. The protocol is not yet widely released, but is already implemented on Google Pixel 3 and more.
In this talk, I will present the UC analysis of Android Protected Confirmation we did with Myrto Arapinis and Thomas Zacharias, from extracting the protocol specification from Android documentation to finding attacks (and implementing one) to proposing a fix.
Rafieh Mosaheb (SnT – University of Luxembourg)
Date: December, 8th 2023 – 10:30 am
Place: A008
Title: Secure e-voting with everlasting privacy
Abstract: In this talk, we delve into the critical topic of vote privacy – a fundamental right which needs to be protected not only during an election, or for a limited time afterwards, but for the foreseeable future. Numerous electronic voting (e-voting) protocols have been proposed to address this challenge, striving for everlasting privacy. This property guarantees that even computationally unbounded adversaries cannot break privacy of past elections. The broad interest in secure e-voting with everlasting privacy has spawned a large variety of protocols over the last three decades. These protocols differ in many aspects, in particular the precise security properties they aim for, the threat scenarios they consider, and the privacy-preserving techniques they employ. Unfortunately, these differences are often opaque, making analysis and comparison cumbersome.
In order to overcome this non-transparent state of affairs, we systematically analyze all e-voting protocols designed to provide everlasting privacy. First, we illustrate the relations and dependencies between all these different protocols. Next, we analyze in depth which protocols do provide secure and efficient approaches to e-voting with everlasting privacy under realistic assumptions, and which ones do not. Eventually, based on our extensive and detailed treatment, we identify which research problems in this field have already been solved, and which ones are still open.
To sum up, this talk offers a well-founded reference point for conducting research on secure e-voting with everlasting privacy as well as for future-proofing privacy in real-world electronic elections.
Charlie Jacomme
Date: January, 19th 2024 – 10:30 am
Place: A008
Title: (* available soon *)
Abstract: (* available soon *)
Previous talks
Vincent Laporte
Date: November, 10th 2023 – 11:00 am
Place: A008
Title: Typing High-Speed Cryptography against Spectre v1
Abstract:
The current gold standard of cryptographic software is to write efficient libraries with systematic protections against timing attacks. In order to meet this goal, cryptographic engineers increasingly use high-assurance cryptography tools. These tools guide programmers and provide rigorous guarantees that can be verified independently by library users. However, high-assurance tools reason about overly simple execution models that elide micro-architectural leakage. Thus, implementations validated by high-assurance cryptography tools remain potentially vulnerable to micro-architectural attacks such as Spectre or Meltdown. Moreover, proposed countermeasures are not used in practice due to performance overhead.
We propose, analyze, implement and evaluate an approach for writing efficient cryptographic implementations that are protected against Spectre v1 attacks. Our approach ensures speculative constant-time, an information flow property which guarantees that programs are protected against Spectre v1. Speculative constant-time is enforced by means of a (valuedependent) information flow type system. The type system tracks security levels depending on whether execution is misspeculating. We implement our approach in the Jasmin framework for high-assurance cryptography, and use it for protecting all implementations of an experimental cryptographic library that includes highly optimized implementations of symmetric primitives, of elliptic-curve cryptography, and of Kyber, a latticebased KEM recently selected by NIST for standardization. The performance impact of our protections is very low; for example, less than 1% for Kyber and essentially zero for X25519.
Sylvain Ruhault (ANSSI)
Date: September, 29th 2023 – 10:30 am
Place: B013
Title: A Unified Symbolic Analysis of WireGuard
Abstract: Both the symbolic and the computational model, with or without computer-aided proof assistants. These analyses however consider different adversarial models or refer to incomplete versions of the protocols. In this work, we propose a unified formal model of WireGuard protocol in the symbolic model. Our model uses the automatic cryptographic protocol verifiers Sapic+, ProVerif and Tamarin. We consider a complete protocol execution, including cookie messages used for resistance against denial of service attacks. We model a precise adversary that can read or set static, ephemeral or pre-shared keys, read or set ecdh pre-computations, control key distribution. Eventually, we present our results in a unified and interpretable way, allowing comparisons with previous analyses. Finally thanks to our model, we confirm a flaw on the anonymity of the communications and point an implementation choice which considerably weakens its security. We propose a remediation that we prove secure using our models.
This is joint work with Dhekra Mahmoud and Pascal Lafourcade.
Ala Eddine Laouir
Date: May, 12th 2023 – 10:30 am
Place: A008
Title: On Privacy of Multidimensional Data Against Aggregate Knowledge Attacks
Abstract: In this presentation, we explore the challenge of preserving individual privacy when publishing data cubes that are queried using SUM functions. We focus on the threat of malicious users obtaining aggregate knowledge (e.g., average information) over data ranges and propose a solution that maximizes the utility of SUM queries while mitigating inference attacks. Our solution combines cube compression, which suppresses data cells. We first present a formal statement for the privacy of aggregate knowledge based on data suppression. Then, we introduce a Linear Programming (LP) model to determine the optimal number of data cells to remove, and a heuristic method to effectively suppress data cells. To further enhance privacy, we supplement data suppression with appropriate data perturbation. Finally, we evaluate the performance of our solution on benchmark data cubes and demonstrate that it achieves the best balance between utility and privacy.
Thomas Haines (Australian National University)
Date: May, 10th 2023 – 11:00 am
Place: B013
Title: Security Implications of Microservices in the Swiss Post E-voting System
Abstract: It is increasingly common to implement systems as a collection of small components, called microservices, which are independent and communicate over well-defined APIs. This has many advantages including: independently deployable which aids scalability, small in size and highly modular, and highly maintainable and testable. However, the security definitions common for cryptographic primitives and protocols tend to encode strong assumptions on what inputs are allowed, in what state, and at what times; this contrasts strongly with the tendency of microservices. In this talk, Thomas Haines (Senior Lecturer at the Australian National University) will discuss the Swiss Post E-voting System’s use of microservices and the possible security impacts.
Mathieu Turuani
Date: April, 14th 2023 – 10:30 am
Place: A008
Title: Themis: an On-Site Voting System with Systematic Cast-as-intended Verification and Partial Accountability
Slides: [pdf]
Abstract: We propose an on-site voting system Themis, that aims at improving security when local authorities are not fully trusted. Voters vote thanks to voting sheets as well as smart cards that produce encrypted ballots. Electronic ballots are systematically audited, without compromising privacy. Moreover, the system includes a precise dispute resolution procedure identifying misbehaving parties. We conduct a full formal analysis of Themis using ProVerif, with a novel approach in order to cover the modular arithmetic needed in our protocol. In order to evaluate the usability of our system, we organized a voting experiment on a (small) group of voters.
Johannes Mueller (University of Luxembourg)
Date: April, 5th 2023 – 10:00 am
Place: B013
Title: Towards End-to-End Formal Verification of Voting Protocols
Abstract: Formal verification has made unprecedented contributions to the analysis and development of secure electronic voting systems. However, there exists a blind spot in all previous computer-aided formal verifications: they idealize the tallying phase of voting protocols.
In the first part of my talk, I will demonstrate how this idealization can undermine the expressiveness of formal verification. On the one hand, I will show that vulnerabilities in the tallying phases of some voting protocols had been overlooked. On the other hand, I will explain that the idealization of the tallying phase also lead to flaws in those phases that had in fact been modeled. In order to close this gap and thus to improve the expressiveness of computer-aided formal verification, we need to model and verify voting protocols end-to-end.
In the second part of my talk, I will present our work-in-progress towards this goal: a formally verified model of a verifiable re-encryption mix net. While this model is a significant step towards end-to-end verification, we are still facing some open problems that I will share and discuss with the audience.
Léo Robert (LIMOS)
Date: March, 3rd 2023 – 10:30 am
Place: A008
Title: How fast do you heal? A taxonomy for post-compromise security in secure-channel establishment.
Slides: [pdf]
Abstract: Post-Compromise Security (PCS) is a property of secure-channel establishment schemes, which limits the security breach of an adversary that has compromised one of the endpoint to a certain number of messages, after which the channel heals. An attractive property, especially in view of Snowden’s revelation of mass-surveillance, PCS features in prominent messaging protocols such as Signal. In this talk, we introduce a framework for quantifying and comparing PCS security, with respect to a broad taxonomy of adversaries. The generality and flexibility of our approach allows us to model the healing speed of a broad class of protocols, including Signal, but also an identity-based messaging protocol named SAID, and even a composition of 5G handover protocols. We also apply the results obtained for this latter example in order to provide a quick fix, which massively improves its post-compromise security.
Maïwenn Racouchot
Date: March, 17th 2023 – 10:30 am
Place: A008
Title: Enhencing tamarin-prover automation
Abstract: Tamarin includes by default eight static heuristics. They help cover most cases, but can sometimes be really inefficient. In order to deal with these cases, Tamarin allows its users to create personalized heuristics by writing a script in a foreign programing language (usually python). However, this functionality has several limits. First the call to a foreign language create unnecessary operations. Then, due to the parameters given to the script, it only has a few information about the state of the proof. Finally, it requires a good knowledge of the internal functioning of Tamarin from the user to write it. In order to tackle these issues, we have created an internal language called Tactic which should provide more freedom to the user while being easier to start using.
Moreover, while going through the proof tree, Tamarin can get stuck in a loop which prevents the proof from finishing. It can be avoided by finding an heuristic that avoids the problematic choices, but it means the user needs to find the loop first. The tool SmartVerif been implemented to answer this problem by using reinforcement learning. However, this method had a major drawback regarding the time of execution. Due to the need of training, it was very long even in very basic cases. To propose a more time efficient solution, we have decided to add a system of loop detection to Tamarin.The first step has been to detect when the proof was about to repeat a step it has already taken and make it go another way. Then, we implemented a system of backtracking to completely get out of the loop. At last we implemented a black list to recognize the problematic situations before entering in a loop.
Christophe Ringeissen
Date: January, 20th 2023 – 10:30 am
Place: B013
Title: Reasoning and Solving Modulo (Intruder) Theories
Slides: [pdf]
Abstract: In this talk, we present some results obtained recently in the development of reasoners and solvers modulo theories. In the context of (combined) equational theories, we briefly introduce our recent work on hierarchical unification. Then, we focus on the knowledge problems that arise in the symbolic analysis of security protocols, namely the deduction problem and the static equivalence problem. In this field some restricted standard term rewrite systems, such as subterm-convergent, have proven useful since the knowledge problems are decidable for such systems. We discuss the possibility of lifting these decidability results to the case of subterm-convergent systems modulo an equational theory. Then we consider the knowledge problems in a class of standard rewrite systems including the classical “beyond subterm-convergent” examples. We introduce a new form of restricted term rewrite system, the graph-embedded term rewrite system. These systems are more flexible extensions of the well known homeomorphic-embedded property of term rewrite systems. Here we show that many of the “beyond subterm-convergent'” systems belong to a particular subclass of graph-embedded convergent systems where the knowledge problems can be decided just like in the subterm-convergent case.
Peter Roenne
Date: December, 16th 2022 – 10:30 am
Place: A008
Title: The Estonian IVXV System and PQ Verifiable Decryption
Abstract: In this informal talk, I will present two topics. First, a recent experience investigating the Estonian IVXV system and a problem found in the verification app implementations. Secondly, I will discuss a new general method for verifiable decryption which is particularly efficient for batch decryption e.g. in e-voting.
Joseph Lallemand (Univ Rennes, CNRS, IRISA)
Date: December, 12th 2022 – 11:00 am
Place: A008
Title: One vote is enough to analyse privacy
Abstract: Electronic voting promises the possibility of convenient and efficient systems for recording and tallying votes in an election. To be widely adopted, ensuring the security of the cryptographic protocols used in e-voting is of paramount importance. However, the security analysis of this type of protocols raises a number of challenges, and they are often out of reach of existing verification tools.
In our work, we study vote privacy, a central security property that should be satisfied by any e-voting system. More precisely, we propose the first formalisation of the state-of-the-art BPriv notion in the symbolic setting. To ease the formal security analysis of this notion, we propose a reduction result allowing one to bound the number of voters and ballots needed to mount an attack. Our result applies on a number of case studies including several versions of Helios, Belenios, JCJ/Civitas, and Prêt-à-Voter. For some of these protocols, thanks to our result, we are able to conduct the analysis relying on the automatic tool ProVerif.
Alexandre Debant
Date: November, 18th 2022 – 10:30 am
Place: A008
Title: Reversing, Breaking, and Fixing the French Legislative Election E-Voting Protocol
Slides: [pdf]
Abstract: We conduct a security analysis of the e-voting protocol used for the largest political election using e-voting in the world, the 2022 French legislative election for the citizens overseas. Due to a lack of system and threat model specifications, we built and contributed such specifications by studying the French legal framework and by reverse-engineering the code base accessible to the voters. Our analysis reveals that this protocol is affected by two design-level and implementation-level vulnerabilities. We show how those allow a standard voting server attacker and even more so a channel attacker to defeat the election integrity and ballot privacy due to 5 at- tack variants. We propose and discuss 5 fixes to prevent those attacks. Our specifications, the attacks, and the fixes were acknowledged by the relevant stakeholders during our respon- sible disclosure. They will implement our fixes to prevent our attacks for future elections. Beyond this protocol, we draw general lessons, recommendations, and open questions from this instructive experience where an e-voting protocol meets the real-world constraints of a large-scale, political election.
Élise Klein
Date: October, 21st 2022 – 10:30 am
Place: A008
