Team seminars

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

Léo Louistisserand

Date: November, 8th 2024 – 10:30 am
Place: A008
Title: Toward secure postal voting
Abstract:  Although widely used in practice, there is little interest in postal voting in the academic world. Security issues are the same as for electronic voting, but voters resources are severely limited. After a brief review of the state of the art, I will present generic attacks on existing protocols. I will then propose an original protocol to address the problem, along with its security analysis.


Joseph Lallemand (IRISA)

Date: December, 6th 2024 – 10:30 am
Place: A008
Title: Proving non-deduction properties with Squirrel
Abstract:  I will present recent advancements regarding the handling of weak secrecy properties in the computational model with Squirrel.
In the context of protocol verification, secrecy is often expressed as an equivalence property, e.g. the message expected to be secret cannot be distinguished from a random value. A weaker notion of secrecy can be formulated as non-deducibility: an attacker cannot compute the exact value of the secret. Although that property is weaker than equivalence-based ones, it is still of great interest, typically as an intermediate step in security proofs.
The Squirrel prover, a proof assistant for protocols in the computational model, had until recently limited support for reasoning on non-deducibility, often requiring users to prove instead strong secrecy properties. We have made new developments that much improve the situation. First, we have proposed an approach based on type systems to track which values in a protocol are deducible by an attacker.
This yields a sound procedure to prove non-deduction, which is, although limited in scope, fully automated. Second, we leverage recent higher-order extensions of the logic of Squirrel to reason about adversarial computations, allowing us to define a non-deducibility predicate explicitly in Squirrel, along with proof rules to manipulate it — this is still work in progress.


Previous talks

Saranya Vijayakumar (Carnegie Mellon University)

Date: October, 11th 2024 – 10:30 am
Place: A008
Title: Using ML techniques for Privacy and Security
Abstract:  In this talk, I will explore the intersection of machine learning (ML) techniques and their application to privacy and security challenges. I will begin by examining how topics-based APIs can leak sensitive information through data patterns and inference attacks. I’ll discuss how adversarial ML techniques and privacy-preserving models, such as differential privacy, can be applied to minimize these risks. Moving into security, I will focus on the detection of obfuscated malware, showcasing how dynamic analysis and ML classifiers can effectively detect and prevent malicious binaries from evading detection systems. By utilizing clustering techniques and reinforcement learning, I will demonstrate how these approaches can improve detection accuracy and adapt to evolving threats, highlighting the crucial role of ML in defending against both privacy breaches and security attacks in modern environments.


Prashant Agrawal (IIT Delhi)

Date: September, 27th 2024 – 10:30 am
Place: A008
Title: Building trust in large public elections
Abstract:  In this talk, I will present current challenges in building secure voting systems for large public elections. I will highlight various factors that prevent the adoption of current cryptographic end-to-end verifiable (E2E-V) voting systems in large elections and contrast them with the problems faced by paper-based voting methods. Given this, I will argue that dual voting — a system that supports both E2E-V voting and paper audit trails — presents unique opportunities in building public trust in large elections. Nevertheless, dual voting comes with its own unique challenges, e.g., how to recover from the situation when the E2E-V tally differs from the paper tally. I will dissect these challenges and present a dual voting protocol called OpenVoting that attempts to address them. Our work is done in the context of Indian elections, which are the world’s largest elections; so I will also point out at some problems specific to the Indian context.


Élise Klein

Date: June, 28th 2024 – 10:30 am
Place: B013
Title: Automation for Tamarin: Augmented equational theories with user defined AC function symbols
Abstract:  Tamarin is a symbolic verification tool for cryptographic protocols, allowing the user to specify equational theories to define the algebraic properties of the cryptographic primitives. Currently, the equational theories are limited on several points : the user can neither enhance the equational theory of a built-in symbol nor define associative and commutative (AC) function symbol. The reason for the latter is that AC symbols often cause terminaison issues due to infinite chains in the intruder deduction.
In this talk, I will present, first, improvements in Tamarin to allow user defined AC function symbols and, second, an algorithm checking sufficient conditions to bound the length of chains. As a running example, I will discuss the case of the xor operator.


Wafik Zahwa

Date: June, 7th 2024 – 10:30 am
Place: B013
Title: Automated Placement of In-Network ACL Rules
Abstract:  Access control lists (ACLs) control and manage access to resources and protect against unauthorized access. They dictate the actions taken for each packet entering the network. ACL rules are stored in tables implemented using ternary content addressable memories (TCAM).TCAMs provide fast match-action operations as they use a parallel search system. However, they require a high amount of energy and their cost is high. The growing number of attacks coming from diverse sources continually increases the number of entries in access control lists (ACL). Thus, to avoid relying on large and expensive memory capacities in network switches, a complementary approach is to split ACLs and distribute their parts over the network to provide the same control functionality between end points. We will introduce the ACL placement problem with algorithms based on graph theory and machine learning approach to address it.


Johannes Mueller

Date: May, 3rd 2024 – 11:00 am
Place: B013
Title: Post-Quantum Secure E-Voting: Challenges, Solutions, and Open Problems
Abstract:  In order to protect e-voting systems from the risk of future quantum attacks, several solutions have been developed in recent years that exclusively use post-quantum cryptography. Since post-quantum cryptography differs from classical cryptography in terms of efficiency and other properties, existing post-quantum e-voting systems take different approaches than many established e-voting systems such as Helios or Belenios.
In this talk, I will give an overview of the state of research on post-quantum e-voting protocols: how they work, what properties they offer, and what limitations they have. We will see which challenges have already been satisfactorily solved and which interesting research questions are still open.


Alexandre Debant

Date: April, 12th 2024 – 10:30 am
Place: C103
Title: ProVerif, restrictions, equivalence… what could go wrong?
Slides: [pdf]
Abstract:  Assuming that the audience is familiar with symbolic models, ProVerif syntax and semantics, and equivalence definitions, I will discuss in this presentation the impact of the use of restrictions in ProVerif when proving equivalence queries. I will recall what ProVerif is actually proving and what it is not (compared to what is presented in the seminal paper [JCS’16]), what the user could expect and what they can’t. Based on this elements, I will finish with a presentation of an ongoing work whose aim is to overcome (some of) these limitations.


Léo Louistisserand

Date: March, 15th 2024 – 10:30 am
Place: A008
Title: Formal verification of the Lightning Network
Abstract: Bitcoin is a widely deployed protocol for decentralized transactions. To improve its scalability, the Lightning Network protocol has been proposed, as an additional layer. It enables anyone to perform an arbitrary number of transactions with any other participant, at the cost of only one publication on the blockchain and without any trust assumption.  This protocol, however, has not been proven secure, and some flaws like the wormhole attack have been found.
In this work in collaboration with Simon Jeanteur and Matteo Maffei, we conduct a security analysis of the Lightning Network. We state the desired security properties and design a formal model of the complete protocol. Then, we create a lighter model and prove its security using the  Proverif automated tool. Finally, we prove the equivalence of the two models using a composition result.


Vincent Diemunsch

Date: February, 23rd 2024 – 10:30 am
Place: B013
Title: Formal Analysis of the Security Properties of the OPC-UA Industrial Control Systems protocol
Abstract: Industrial Control Systems typically use proprietary protocols with no or weak security. To remedy this state of affairs, both ANSSI and BSI are promoting the transition to OPC-UA: an open protocol, standardized as IEC 62541, that allows operators in a control room to command and control industrial automation systems through a SCADA. Based on TCP/IP, and the deployment of a PKI, OPC-UA offers integrity for data exchanges and when required confidentiality. It also offers authentication of users, by passwords or certificates, and autorisation through Role Based Access Control. We are currently trying to prove OPCU-UA protocol security properties with the ProVerif symbolic model prover. This turns out to be challenging because its specifications are ambiguous and the state machine that we have modelled from them is complex. Several weaknesses have been reported to the Security Group of the OPC-UA Foundation to be fixed in future releases of the specifications. I will also discuss challenges we face to extend the configurations on which ProVerif is able to prove the security properties.


Dhekra Mahmoud

Date: February, 16th 2024 – 11:00 am
Place: B013
Title: Transferable, Auditable and Anonymous Ticketing Protocol
Abstract: Dgital ticketing systems typically offer ticket purchase, refund, validation, and, optionally, anonymity of users. However, it would be interesting for users to transfer their tickets, as is currently done with physical tickets. In this work, we propose Applause, a ticketing system allowing the purchase, refund, validation, and transfer of tickets based on trusted authority, while guaranteeing the anonymity of users, as long as the used payment method provides anonymity. To study its security, we formalise the security of the transferable E-Ticket scheme in the game-based paradigm. We prove the security of Applause computationally in the standard model and symbolically using the protocol verifier ProVerif. Applause relies on standard cryptographic primitives, rendering our construction efficient and scalable, as shown by a proof-of-concept. In order to obtain Spotlight, an auditable version of the protocol that we also proved to be secure, users will remain anonymous except for a new third party, which will be able to disclose their identity in the event of a disaster.


Charlie Jacomme

Date: January, 19th 2024 – 10:30 am
Place: B013
Title: Models and proofs against the real world – when do we start trusting that a communication protocol is secure ?
Abstract: As a new member of the PESTO team, I will introduce myself as well as my past, present and future research works.
My main goal is to provide guarantees on the privacy and security of communication protocols, which includes a broad range of things such as HTTPS for securing internet browsing, as well as Signal for a secure messaging application. Most of my work, while not always so clearly focused toward this goal, in fact turns out to either try to provide such guarantees, or try to make it possible.
In this talk, I will discuss how such guarantees can be obtained by making models of the real world and making proofs over those models. I will then touch on many related subjects, notably:
* What tools can we use to make proofs over such complex models?
* How do the different models compare together, how far are they from the real world, and can we reduce this gap?
* When models are simply too big, can we find ways to simplify the proofs?
This will notably bring us to discuss tools such as ProVerif, Tamarin, Sapic+,Squirrel, CryptoVerif, all of which I have either extensively used or participated in their development, as well as discussing the classical assumptions used in the computational and symbolic model that I worked on for hashes and authenticated encryption, as well as look at what I hope to improve in the future.


Previous seminars in 2023

Diane Leblanc-Albarel (KU Leuven)

Date: December, 18th 2023 – 11:00 am
Place: A008
Title:  Optimising Time-Memory Trade-Off
Abstract: In this seminar, I will present my PhD research on Time-Memory Trade-Off (TMTO) attacks, with a focus on my work on rainbow tables. Prior to my PhD, research on TMTOs focused primarily on the attack phase of the algorithm, with little attention paid to the precomputation phase. However, it is the precomputation phase that has become the bottleneck in the use of TMTOs today. During my PhD, I introduced and implemented several variants and improvements that reduce precomputation time without negatively affecting the attack phase and, in some cases, have even improved the attack. To conclude, I will provide insights into my current work and outline the areas I am eager to pursue in future research.


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.


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.


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.


Previous seminars in 2022

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

Comments are closed.