3.2.1 Generic proof techniques

Most automated tools for verifying security properties rely on techniques stemming from automated deduction. Often existing techniques do however not apply directly, or do not scale up due to state explosion problems. For instance, the use of Horn clause resolution techniques requires dedicated resolution methods 4245. Another example is unification modulo equational theory, which is a key technique in several tools, e.g. 54. Security protocols however require to consider particular equational theories that are not naturally studied in classical automated reasoning. Sometimes, even new concepts have been introduced. One example is the finite variant property 47, which is used in several tools, e.g., Akiss  45, Maude-NPA 54 and TAMARIN  60. Another example is the notion of asymmetric unification 53 which is a variant of unification used in Maude-NPA to perform important syntactic pruning techniques of the search space, even when reasoning modulo an equational theory. For each of these topics we need to design efficient decision procedures for a variety of equational theories.

3.2.2 Dedicated procedures and tools

We design dedicated techniques for automated protocol verification. While existing techniques for security protocol verification are efficient and have reached maturity for verification of confidentiality and authentication properties (or more generally safety properties), our goal is to go beyond these properties and the standard attacker models, verifying the properties and attacker models identified in Section 3.1. This includes techniques that:

• can analyse indistinguishability properties, including for instance anonymity and unlinkability properties, but also properties stated in simulation-based (also known as universally composable) frameworks, which express the security of a protocol as an ideal (correct by design) system;
• take into account protocols that rely on a notion of mutable global state which does not arise in traditional protocols, but is essential when verifying tamper-resistant hardware devices, e.g., the RSA PKCS#11 standard, IBM's CCA and the trusted platform module (TPM);
• consider attacker models for protocols relying on weak secrets that need to be copied or remembered by a human, such as multi-factor authentication.

These goals are beyond the scope of most current analysis tools and require both theoretical advances in the area of verification, as well as the design of new efficient verification tools.

3.3.1 General design techniques

Design techniques include composition results that allow one to design protocols in a modular way 48, 46. Composition results come in many flavours: they may allow one to compose protocols with different objectives, e.g. compose a key exchange protocol with a protocol that requires a shared key or rely on a protocol for secure channel establishment, compose different protocols in parallel that may re-use some key material, or compose different sessions of the same protocol.

Another area where composition is of particular importance is Service Oriented Computing, where an “orchestrator” must combine some available component services, while guaranteeing some security properties. In this context, we work on the automated synthesis of the orchestrator or monitors for enforcing the security goals. These problems require the study of new classes of automata that communicate with structured messages.

3.3.2 New protocol design

We also design new protocols. Application areas that seem of particular importance are:

• External hardware devices such as security APIs that allow for flexible key management, including key revocation, and their integration in security protocols. The security fiasco of the PKCS#11 standard 43, 50 witnesses the need for new protocols in this area.
• Election systems that provide strong security guarantees. We have been working (in collaboration with the Caramba team) on a prototype implementation of an e-voting system, Belenios.
• Mechanisms for publishing personal information (e.g. on social networks) in a controlled way.

7.1.1 Belenios

• Name:
  Belenios - Verifiable online voting system
• Keyword:
  E-voting
• Functional Description:

  Belenios is an open-source online voting system that provides vote confidentiality and verifiability. End-to-end verifiability relies on the fact that the ballot box is public (voters can check that their ballots have been received) and on the fact that the tally is publicly verifiable (anyone can recount the votes). Vote confidentiality relies on the encryption of the votes and the distribution of the decryption key (no one detains the secret key).

  Belenios supports various kind of elections. In the standard mode, Belenios supports simple elections where voters simply select one or more candidates. It also supports arbitrary counting functions at the cost of a slightly more complex tally procedure for the authorities. For example, Belenios supports Condorcet, STV, and Majority Judgement, where voters order candidates and grade them.

  Belenios is available in several languages for the voters as well as the administrators of an election. More languages can be freely added by users.

• News of the Year:

  In 2022, our platform was used to run about 1400 elections, with about 50,000 ballots counted.

  This year we released a major update of Belenios (2.0) that introduces a new election format where election events (e.g., ballot submission) are chained to each other. This sets the stage for a future release where the server will be able to commit to the actual content of an election. We have also improved the monitoring of the server (eg by making the voting authority code constant) and we have initiated compliance with the CNIL recommendations. We have hardened the security of Belenios by linking a voter to the public part of their voting code from the setup phase. To ensure better availability, Belenios is now hosted on OVH servers. Finally, we have pursued the development of the REST API in preparation of a major overhaul of the election administration interface.

• URL:
  https://­www.­belenios.­org/
• Contact:
  Stéphane Glondu
• Participants:
  Pierrick Gaudry, Stéphane Glondu, Véronique Cortier
• Partners:
  CNRS, Inria

7.1.2 Tamarin

• Name:
  Tamarin prover
• Keywords:
  Security, Verification
• Functional Description:
  The Tamarin prover is a security protocol verification tool that supports both falsification and unbounded verification of security protocols specified as multiset rewriting systems with respect to (temporal) first-order properties and a message theory that models Diffie-Hellman exponentiation, bilinear pairing, multisets, and exclusive-or (XOR), combined with a user-defined convergent rewriting theory. Its main advantages are its ability to handle stateful protocols and its interactive proof mode. Moreover, it has been extended to verify equivalence properties. The tool is developed jointly by the PESTO team, the Institute of Information Security at ETH Zurich, and CISPA. In a joint effort, the partners wrote and published a user manual in 2016, available from the Tamarin website.
• News of the Year:
  One major strength of Tamarin is that it offers an interactive mode, allowing users to go beyond what pushbutton tools can typically handle. Tamarin is for example able to verify complex protocols such as TLS or the authentication protocols from the 5G standard. However, one of its drawback is its lack of automation. For many simple protocols, the user often needs to help Tamarin by writing specific lemmas, called “sources lemmas”, which requires some knowledge of the internal behaviour of the tool. In 2020, Cortier and Dreier, in collaboration with Delaune, proposed a technique to automatically generate sources lemmas in Tamarin. They proved formally that the lemmas indeed hold, for arbitrary protocols that make use of cryptographic primitives that can be modelled with a subterm convergent equational theory (modulo associativity and commutativity). They have implemented their approach within Tamarin. Experiments show that, in most examples of the literature, suitable sources lemmas can now be automatically generated, in replacement of the handwritten lemmas. As a direct application, many simple protocols can now be analysed fully automatically, while they previously required user interaction. This year the same authors, together with Klein, improved their previous technique so that now sources lemmas can be generated in even further cases. Moreover, Dreier, Kremer and Racouchot recently developed a new "tactics" language that allows users to specify their own proof heuristics in a simple way. This can help them to fine-tune proof strategies if the built-in heuristics fail, for example on complex examples. Finally, Cheval, Jacomme, Kremer and Künnemann have significantly re-designed the SAPIC plugin, which allows protocol specification in a stateful dialect of the applied pi calculs. The resulting SAPIC+ is a protocol verification platform that additionally features automated translations from SAPIC+ to ProVerif and DeepSec. It also extends the exiting translation with powerful, protocol-independent optimizations.
• URL:
  http://­tamarin-prover.­github.­io/
• Publications:
  hal-03767104, hal-02903620, hal-02358878, hal-03693843
• Contact:
  Jannik Dreier
• Participants:
  Jannik Dreier, Elise Klein, Maiwenn Racouchot, Véronique Cortier, Steve Kremer
• Partner:
  CISPA Helmholtz Center for Information Security

7.1.3 Jasmin

• Name:
  Jasmin compiler and analyser
• Keywords:
  Cryptography, Static analysis, Compilers
• Functional Description:

  The Jasmin programming language smoothly combines high-level and low-level constructs, so as to support “assembly in the head” programming. Programmers can control many low-level details that are performance-critical: instruction selection and scheduling, what registers to spill and when, etc. The language also features high-level abstractions (variables, functions, arrays, loops, etc.) to structure the source code and make it more amenable to formal verification. The Jasmin compiler produces predictable assembly and ensures that the use of high-level abstractions incurs no run-time penalty.

  The semantics is formally defined to allow rigorous reasoning about program behaviors. The compiler is formally verified for correctness (the proof is machine-checked by the Coq proof assistant). This justifies that many properties can be proved on a source program and still apply to the corresponding assembly program: safety, termination, functional correctness…

  Jasmin programs can be automatically checked for safety and termination (using a trusted static analyzer). The Jasmin workbench leverages the EasyCrypt toolset for formal verification. Jasmin programs can be extracted to corresponding EasyCrypt programs to prove functional correctness, cryptographic security, or security against side-channel attacks (constant-time).

• Release Contributions:
  It contains the following major improvements: - a new instruction "#randombytes" to fill an array with “random” data, - access to mmx registers, - support for Windows calling convention, in addition to Linux, - "else if" blocks for readability, - strict preservation of source-level intrinsics, - an option to extract all the functions of a file to EasyCrypt, - many fixes to the extraction to EasyCrypt.
• News of the Year:

  In 2022, two major versions were released. The first one, 2022.04.0, is the result of more than two years of development, and thus brings major new features to the language, including the support for local functions and sub-arrays. The second one, 2022.09.0, adds in particular the support for system calls, which allows for instance to call an operating system function returning random data.

  Work to support multiple architecture has progressed well. The support for ARM 32 bits was merged and is being polished.

  Work on "Speculative Load Hardening", a transformation making a program resistant to some Spectre attacks, are ongoing. In parallel, another line of work tries to add arrays whose length is not known at compile time.

• URL:
  https://­github.­com/­jasmin-lang/­jasmin
• Publications:
  hal-03844366, hal-03430789, hal-03352062, hal-02404581, hal-02974993, hal-01649140
• Contact:
  Benjamin Grégoire
• Participants:
  Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Jean-Christophe Lechenet, Swarn Priya
• Partners:
  The IMDEA Software Institute, Ecole Polytechnique, Universidade do Minho, Université de Porto, Max Planck Institute for Security and Privacy

7.1.4 tlspuffin

• Name:
  TLS Protocol Under FuzzINg
• Keywords:
  Fuzzing, Formal methods, Cryptographic protocol
• Functional Description:
  tlspuffin is a full-fledged and modular DY fuzzer implementation in Rust. DY Fuzzing is a novel approach to fuzzing cryptographic protocols. It is based on the idea of using formal Dolev-Yao (DY) models as domain-specific knowledge to guide the fuzzer and give it the ability to detect logical attacks in protocol implementations. tlspuffin revolves around three main layers and modules that are of independent interest. First, the protocol- and Program Under Test-agnostic DY fuzzer that we implemented in a standalone module puffin uses the main fuzzing loop of the modular, state-of-the art fuzzer LibAFL. It implements custom test cases using DY traces, mutations, and objective oracle. On top of puffin, we built protocol-dependent fuzzers. We currently support tlspuffin for TLS and the preliminary sshpuffin for SSH. Third, we connect PUTs such as OpenSSL, LibreSSL, and wolfSSL to the fuzzers.
• News of the Year:
  In 2022 we made the first release of the tlspuffin fuzzer. We have connected the following PUTs to our fuzzer: OpenSSL, LibreSSL, and wolfSSL to tlspuffin and libssh to the preliminary sshpuffin.
• URL:
  https://­github.­com/­tlspuffin/­tlspuffin
• Contact:
  Lucca Hirschi
• Participants:
  Max Ammann, Lucca Hirschi, Steve Kremer
• Partner:
  Trail of Bits

8.1.1 Foundations of Automated Verification: Semantics, Decidability and Complexity

Participants: Véronique Cortier, Steve Kremer, Raphaëlle Crubillé, Christophe Ringeissen.

Security properties of cryptographic protocols are typically expressed as reachability or equivalence properties. Secrecy and authentication are examples of reachability properties while privacy properties such as untraceability, vote secrecy, or anonymity are generally expressed as behavioral equivalence in a process algebra that models security protocols.

Cortier, Dallon, and Delaune 20 identify a (decidable) class of security protocols for which it is possible to significantly bound the number of sessions, for both reachability and equivalence properties. The class sets up three main assumptions. (i) Protocols need to be without else branch and “simple”, meaning that an attacker can precisely identify from which participant and which session a message originates from. (ii) Protocols should be type-compliant which is intuitively guaranteed as soon as two encrypted messages of the protocol cannot be confused. (iii) Finally, the dependency graph of the protocol must be acyclic. The dependency graph is a new notion that characterises how actions depend on each other. The class covers all standard cryptographic primitives. Experiments show that on most basic protocols of the literature, the proposed algorithm computes a small number of sessions (a dozen). As a consequence, tools for a bounded number of sessions like DeepSec can then be used to conclude that a protocol is secure for an unbounded number of sessions. These results have been published at CSF'22.

Cheval (Inria Paris), Crubillé and Kremer study probabilistic process equivalences for security protocols. Symbolic models are classically purely non-deterministic. Indeed, generating random keys and nonces, or using randomized cryptographic primitives (like any secure encryption scheme) is idealized in symbolic models, replacing random numbers that can be guessed with only a negligible probability with perfectly fresh values that cannot be guessed at all. This abstraction has been widely used and has shown its usefulness. Another source of randomness may however come from the control flow. Typically, protocols aiming at anonymity, such as the Dining Cryptographers protocol, require users to take one action or another probabilistically. In this work we propose an extension of the applied pi calculus with a probabilistic choice operator (${+}_p$) and corresponding process equivalences. We show that it is essential that schedulers in such a probabilistic calculus are randomized, as non-randomized schedulers lead to definitions that have undesirable properties. We for instance show that typical behavioral relations would not be transitive and point out a flaw in the main theorem of a previous framework  56 that chose non-randomized schedulers. Mixing non-determinism and probabilistic choices generally leads to unsatisfactory behavioral equivalences: as the non-deterministic choices can leak the probabilistic choices, the resulting equivalences is too strong, modeling unrealistic attacker capabilities. We therefore investigate two sub-classes of protocols. We first consider the class of protocols that do not make any probabilistic choices, but allow the attacker to do so. Even though the honest processes may be purely non-deterministic, the resulting may testing equivalence is strictly stronger by allowing a probabilistic attacker. We show that for a bounded number of sessions may-testing with a probabilistic attacker coincides with purely possibilistic similarity. Second, 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 (no parallel, nor non-deterministic choice). These results have been published at CSF'22 18.

In collaboration with Erbatur (UT Dallas, USA) and Marshall (Univ Mary Washington, USA), Ringeissen studies reasoners and solvers for equational theories used in protocol analysis. In 26, hierarchical matching procedures have been developed for non-disjoint unions of theories sharing only constructor symbols modulo a common sub-theory, such as Associativity-Commutativity. In 33, the same authors plus Dwyer Satterfield (Univ Mary Washington, USA) have identified a class of term rewrite systems including the subterm convergent ones where the deduction problem and the static equivalence problem can be decided in a uniform way just like in the particular subterm convergent case. This class includes many theories of practical interest for which both deduction and static equivalence were decided until now on an individual basis. Beyond the decision problems related to equational unification and (intruder) theories, Ringeissen is also working on SMT (Satisfiability Modulo Theories) solvers to model verification conditions. In collaboration with Sheng, Zohar, Lange, Barrett (Stanford, USA) and Fontaine (University of Liège, Belgium), Ringeissen has published the journal paper showing that the theory of datatypes is strongly polite and so it can be combined with arbitrary disjoint theories to get a satisfiability procedure using polite combination 12.

8.1.2 Improving Verification Tools

Participants: Véronique Cortier, Alexandre Debant, Jannik Dreier, Lucca Hirschi, Elise Klein, Steve Kremer.

8.1.3 Analysis of Deployed Protocols

Participants: Elise Klein, Steve Kremer, Maïwenn Racouchot.

8.1.4 Symbolic Methods in Computational Cryptography Proofs

Participant: Steve Kremer.

In a paper published in ACM TOCL 8, Barthe (MPI Security and Privacy), Jacomme (CISPA) and Kremer study decidability problems for equivalence of probabilistic programs, for a core probabilistic programming language over finite fields of fixed characteristic. The programming language supports uniform sampling, addition, multiplication and conditionals and thus is sufficiently expressive to encode boolean and arithmetic circuits. We consider two variants of equivalence: the first one considers an interpretation over the finite field ${𝔽}_q$, while the second one, which we call universal equivalence, verifies equivalence over all extensions ${𝔽}_{q^k}$ of ${𝔽}_q$. The universal variant typically arises in provable cryptography when one wishes to prove equivalence for any length of bitstrings, i.e., elements of ${𝔽}_{2^k}$ for any $k$. While the first problem is obviously decidable, we establish its exact complexity which lies in the counting hierarchy. To show decidability, and a doubly exponential upper bound, of the universal variant we rely on results from algorithmic number theory and the possibility to compare local zeta functions associated to given polynomials. We then devise a general way to draw links between the universal probabilistic problems and widely studied problems on linear recurrence sequences. Finally we study several variants of the equivalence problem, including a problem we call majority, motivated by differential privacy. We also define and provide some insights about program indistinguishability, proving that it is decidable for programs always returning 0 or 1.

8.1.5 DY fuzzing: Dolev-Yao model-guided Fuzzing of Cryptographic Protocols

Participants: Lucca Hirschi, Steve Kremer.

Critical and widely used cryptographic protocols have repeatedly been found to contain flaws in their design and their implementation. A prominent class of such vulnerabilities is logical attacks, i.e., attacks that solely exploit flawed protocol logic. Automated formal verification methods, based on the Dolev-Yao (DY) attacker, excel at finding such flaws, but operate only on abstract specification models. Fully automated verification of existing protocol implementations is today still out of reach. This leaves open whether widely used protocol implementations are secure. Unfortunately, this blind spot hides numerous attacks, notably recent logical attacks on widely used TLS implementations introduced by implementation bugs.

In collaboration with Max Ammann (former master student), Hirschi and Kremer propose a novel and effective technique that we call DY model-guided fuzzing, which precludes logical attacks against protocol implementations. The main idea is to consider as possible test cases the set of abstract DY executions of the DY attacker, and use a mutation-based fuzzer to explore this set. The DY fuzzer concretizes each abstract execution to test it on the program under test. This approach enables reasoning at a more structural and security-related level of messages (e.g., decrypt a message and re-encrypt it with a different key) as opposed to random bit-level modifications that are much less likely to produce relevant logical adversarial behaviors. We implement a full-fledged and modular DY protocol fuzzer, dubbed puffin. We demonstrate its effectiveness by fuzzing three popular TLS implementations, resulting in the discovery of four novel vulnerabilities in WolfSSL, a lightweight implementation widely used by IoT and embedded devices, and able to run on OSs and CPUs otherwise not supported. Each of them has been responsibly disclosed to and fixed by WolfSSL. They have also been filed as CVEs.

8.1.6 Security of Cryptographic Implementations

Participant: Vincent Laporte.

8.1.7 Protocol Design

Participant: Jannik Dreier.

In 1968, Liu described the problem of securing documents in a shared secret project. In an example, at least six out of eleven participating scientists need to be present to open the lock securing the secret documents. Shamir proposed a mathematical solution to this physical problem in 1979, by designing an efficient $k$-out-of-$n$ secret sharing scheme based on Lagrange's interpolation. Liu and Shamir also claimed that the minimal solution using physical locks is clearly impractical and exponential in the number of participants.

In this work published in the Journal of Computer Security 11 Dreier, Dumas, Lafourcade, and Robert relax some implicit assumptions in Liu and Shamir's claim and propose an optimal physical solution to the problem of Liu that uses physical padlocks, but the number of padlocks is not greater than the number of participants. Then, we show that no device can do better for $k$-out-of-$n$ threshold padlock systems as soon as $k\ge \sqrt{2n}$, which holds true in particular for Liu's example. More generally, we derive bounds required to implement any threshold system and prove a lower bound of $Olog\left(n\right)$ padlocks for any threshold larger than 2. For instance we propose an optimal scheme reaching that bound for 2-out-of-$n$ threshold systems which requires less than $2{log}_2\left(n\right)$ padlocks. We also discuss more complex access structures, a wrapping technique, and other sublinear realizations like an algorithm to generate 3-out-of-$n$ systems with $2.5\sqrt{n}$ padlocks. Finally we give an algorithm building $k$-out-of-$n$ threshold padlock systems with only $Olog{\left(n\right)}^{k-1}$ padlocks. Apart from the physical world, our results also show that it is possible to implement secret sharing over small fields.

8.1.8 Verifiable Decryption

Participant: Peter Roenne.

In a many security protocols asymmetric encryption is employed to preserve privacy of confidential data. The data can then be manipulated in different ways while being encrypted and only the end result is decrypted and revealed. However, in some cases integrity is important and it is necessary to let users verify that the decrypted result was indeed correct without revealing the secret encryption key which would break privacy. A good example is electronic voting where the final election result is obtained as a decryption.

There exist many encryption schemes with verifiable zero-knowledge proofs of correct decryption, but they are all intimately related to the actual scheme, further many post-quantum encryption scheme are still missing such proofs or the proofs lack in efficiency. In 27 Gjoesteen, Haines, Mueller, Roenne and Silde (presented at ACISP 2022) a general transformation is constructed from any encryption scheme allowing a 2-party passively secure distributed decryption into a proof of correct decryption. The method is especially efficient when a large number of ciphertexts need to be decrypted, and an explicit efficient construction for post-quantum secure lattice-based encryption is presented and implemented.

8.2.1 Design of E-Voting Protocols

Participants: Véronique Cortier, Alexandre Debant, Jannik Dreier, Mathieu Turuani, Quentin Yang.

As a part of a contract with Idemia, Cortier, Debant, Dreier, Gaudry (project-team Caramba), and Turuani have designed a novel electronic voting system, Themis, tailored to the voting context envisioned by Idemia. The system is made for on-site elections, with the use of smart cards. However, the goal is that the trust should not be placed in one single part of the system, hence smart cards can not be trusted. One originality of the approach is the possibility to re-use existing techniques, in conjunction with the use of smart-cards and paper ballots. The designed protocol is meant to achieve vote secrecy, coercion resistance, and cast as intended. Coercion resistance is eased by the fact that voters enter a physical voting booth. Cast-as-intended was more difficult to achieve since Idemia aimed at two strong guarantees: all cast ballots should be audited by voters (this is not an option left to the choice of the voter) and whenever the system attempts to cheat, its misbehavior can be proved to a third party, possibly yielding to a punishment of the system. The proposed protocol has been proved secure with the ProVerif tool using some of its new features as explained in Section 8.1.2. A challenge was to cover three families of properties (vote secrecy, verifiability, and accountability) under various corruption scenarios, in a unified way. These results have been presented at CCS'22 16.

There are two main approaches for tallying an election in the context of electronic voting. The first one is the homomorphic tally. Thanks to the homomorphic property of the encryption scheme (typically ElGamal), the ballots are combined to compute the (encrypted) sum of the votes. Then only the resulting ciphertext needs to be decrypted to reveal the election result, without leaking the individual votes. However, it can only be applied to simple vote counting functions. The second main approach is based on mixnets. The encrypted ballots are shuffled and re-randomized such that the resulting ballots cannot be linked to the original ones. Several mixers are successively used and then each (randomized) ballot is decrypted, yielding the original votes in clear, in a random order. It can be used for any vote counting function but it reveals much more information than the result itself (the winner(s) of the election) and is subject to so-called Italian attacks. Quentin Yang, co-supervised by Cortier and Gaudry (project-team Caramba), has studied the possibility to compute the election result from a set of encrypted ballots, without leaking any other information. This can be seen as an instance of Multi-Party Computation (MPC). Cortier, Gaudry and Yang 22 have unveiled several flaws or limitations of the existing works and they have provided a toolbox to implement, at a reasonable cost, several key counting functions of the literature: Majority Judgement, Condorcet, and STV. One of the surprises of the work lies in the fact that they show that it is often preferable to use the very standard El Gamal encryption instead of Paillier encryption, that is typically considered as the Swiss-knife for MPC.

Belenios is the main voting protocol developed by the team, as described in Section 7.1.1. We presented at EVoteID'22 its new features and its usage 21. One still missing feature is the cast-as-intended property, that allows a voter to check that their vote has been sent as intended, even when their device is malicious and tries to vote for another candidate. Reusing some of the ideas proposed in the Themis protocol, Cortier, Debant, Gaudry (project-team Caramba), and Glondu are designing a variant of Belenios, called BeleniosCaI, that offers cast-as-intended, without requiring voters to use code sheets nor a second device.

8.2.2 Security analyses of E-Voting Protocols

Participants: Véronique Cortier, Alexandre Debant, Lucca Hirschi, Peter Roenne, Quentin Yang.

8.3.1 Privacy Protection in Social Networks

Participants: Bizhan Alipour, Abdessamad Imine, Kamalkumar Ramanlal Macwan, Michaël Rusinowitch.

Facebook allows users to share photos and express their feelings by using comments. However, Facebook users are vulnerable to attribute inference attacks where an attacker intends to guess private attributes (e.g., gender, age, political view) of target users through their online profiles and/or their vicinity (e.g., what their friends reveal). Given user-generated pictures on Facebook, Bizhan Alipour's thesis 34 shows how to launch gender inference attacks on their owners solely from (i) alt-texts generated by Facebook to describe the content of pictures, and (ii) comments posted by friends, friends of friends or regular users. Evaluation results demonstrate that an adversary can infer the gender with high accuracy by combining alt-texts and comments. Moreover they can identify sensitive words in the meta-data and hide them to decrease drastically the adversary's prediction accuracy. To our knowledge, this is the first inference attack on Facebook that exploits comments and alt-texts solely. Protection against these attribute inference attacks has been investigated too using machine learning explainability and adversarial defense strategies.

Social network users are provided with suggestions of friends groups, or pages, based on their personal information. However the generated recommendations may lead to indirect leakage of private elements. Macwan, Imine and Rusinowitch have investigated the application of Differential Privacy  52 with collaborative recommendation systems to prevent the disclosure of private attributes from recommendations 30, 31.

8.3.2 Privacy-Preserving Big Data Management

Participants: Abdessamad Imine, Ala Eddine Laouir.

8.3.3 Efficient Management of Filtering Rules in Software-defined Networking

Participants: Michaël Rusinowitch, Wafik Zahwa.

In a joint project with the Resist project-team and the Numeryx company, Lahmadi (Resist) and Rusinowitch have developed algorithms to automatically distribute and compress filtering rules on a set of switches of limited capacity 13. Now they investigate with Zahwa a more adaptive and autonomous approach based on reinforcement learning, aiming an application to self-configurating firewalls.

10.1.1 Visits of international scientists

10.2.1 Other european programs/initiatives

Participant: Steve Kremer.

• COST ACTION CA19122 EUGAIN — European Network For Gender Balance in Informatics, duration: 4 years, since 2020, participant and leader of Working Group 3 – From PhD to Professor: Steve Kremer

  Women are underrepresented in Informatics at all levels, from undergraduate and graduate studies to participation and leadership in academia and industry. The main aim and objective of EUGAIN is to improve gender balance in Informatics at all levels through the creation of a European network of colleagues working on the forefront of the efforts for gender balance in Informatics in their countries and research communities.

10.3.1 ANR

• ANR JCJC ProtoFuzz Cryptographic Protocol Logic Fuzz Testing, duration: January 2023 – December 2026, leader: Lucca Hirschi.

  State-of-the-art formal methods for the verification of cryptographic protocols provide no guarantee on implementations, which are the end products that must be secure. Testing, especially fuzzing, is usable by practitioners, operates on implementations and has been very successful at finding low-level flaws but is unable to capture logical flaws. Therefore, effective techniques to preclude logical flaws from protocol implementations are desperately lacking.

  To fill this gap, we will develop the foundations, the design, and the implementation of an innovative hybrid, synergetic framework combining symbolic verification and fuzzing. In particular, we will (i) devise a simple protocol language and model extractor that enable extracting formal models from lightly annotated implementations and then refining those models based on functional correctness counter-examples and (ii) develop a novel testing methodology, symbolic-model-guided fuzzing, that, assisted by symbolic verifiers, efficiently captures logical attacks. The former will leverage a novel hybrid framework where symbolic formal models and implementations are tied together and can animate each other via dual executions.

  This project's ambitions are to significantly advance fuzzing and to establish hybrid frameworks combining fuzzing and symbolic verification as a new research topic, as well as to attack and improve the security of real-world, high-profile cryptographic protocols.

• ANR Chaire IA ASAP Tools for automated, symbolic analysis of real-world cryptographic protocols, duration: September 2020 – August 2024, leader: Steve Kremer.

  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.

• ANR TECAP Protocol Analysis — Combining Existing Tools, duration: January 2018 – June 2022, leader: Vincent Cheval, other partners: ENS Cachan, Inria Paris, Inria Sophia Antipolis, IRISA, LIX.

  Despite the large number of automated verification tools, several cryptographic protocols (e.g. stateful protocols) still represent a real challenge for these tools and reveal their limitations. To cope with these limits, each tool focuses on different classes of protocols depending on the primitives, the security properties, etc. Moreover, the tools cannot interact with each other as they evolve in their own model with specific assumptions. The aim of this project is to get the best of all these tools, that is, to improve the theory and implementation of each individual tool towards the strengths of the others and to build bridges that allow the cooperation of the methods/tools. We will focus in this project on CryptoVerif, EasyCrypt, Scary, ProVerif, TAMARIN, Akiss and APTE. In order to validate the results, we will apply them to several case studies such as the Authentication and Key Agreement protocol from the telecommunication networks, the Scytl and Helios voting protocols, and the low entropy 3D-Secure authentication protocol. These protocols have been chosen to cover many challenges that the current tools are facing.

• ANR SEVERITAS Secure and Verifiable Test and Assessment System, duration: Mai 2021 – April 2025, local coordinator: Jannik Dreier, other partners: LIG/University Grenoble Alpes (coordinator France), SnT/University of Luxembourg (coordinator Luxembourg), LIMOS/Université Clermont Auvergne.

  SEVERITAS advances information socio-technical security for Electronic Test and Assessment Systems (e-TAS). These systems measure skills and performances in education and training. They improve management, reduce time-to-assessment, reach larger audiences, but they do not always provide security by design. This project recognizes that the security aspects for e-TAS are still mostly unexplored. We fill these gaps by studying current and other to-be-defined security properties. We develop automated tools to advance the formal verification of security and show how to valide e-TAS security rigorously. We develop new secure, transparent, verifiable and lawful e-TAS procedures and protocols. We also deploy novel run-time monitoring strategies to reduce frauds and study the user experience about processes to foster e-TAS usable security. Thanks to connections with players in the business of e-TAS, such as OASYS, this project will contribute to the development of secure e-TAS.

10.3.2 PEPR

• PEPR CyberSecurity - SVP Verification of Security Protocols. duration: July 2022 – July 2028, local coordinator: Véronique Cortier, other partners: SPICY - Irisa (coordinator), Prosecco - Inria Paris, INSPIRE - LMF/ Université Paris-Saclay, STAMP - Inria Sophia

  The SVP project aims at enabling the analysis of protocols (either already deployed or in the design phase) at the level of abstract specifications as well as implementations. The goal is to develop techniques and tools allowing the implementation of solutions whose security will not be questioned in a cyclic way. To achieve this challenge, building on the work already done in the community of formal methods for security protocol verification, we notably plan to take the following steps : (i) developing new functionalities in existing tools to allow the analysis of more and more complex protocols ; (ii) building bridges between the different existing proof techniques and associated tools in order to take advantage of the strengths of each of them ; (iii) validate the techniques and tools developed within this project on widely deployed protocols and on more recent, fast-growing applications, such as Internet voting.

11.1.1 Scientific events: organisation

• Jannik Dreier: co-organizer of the Annual Meeting of the WG “Formal Methods for Security” (“Journées du GT Méthodes Formelles pour la Sécurité”), together with Sébastien Bardin (CEA)

11.1.2 Scientific events: selection

11.1.3 Journal

11.1.4 Invited talks

• Véronique Cortier. Invited speaker at NordSec 2022, 27th Nordic Conference on Secure IT Systems, Reykjavik, Iceland, Novembre 2022.
• Véronique Cortier. Keynote speaker at the Summer School in Cybersecurity, Nancy, July 2022.
• Véronique Cortier. Panel at the 10 years SIF congress, Paris, June 2022.
• Véronique Cortier. Seminar at the IMT, Lucca, Italy, remote, March 2022.
• Alexandre Debant: UK-SPS/FM-Sec seminar, remote, November 2022.
• Jannik Dreier: Seminar at TU Dresden, Germany, remote, July 2022.
• Steve Kremer: Round table at Inria's Scientific Days on Integrity, reproducibility and diversity, November 2022.
• Steve Kremer: UK-SPS/FM-Sec seminar, remote, September 2022.
• Steve Kremer: Informatic Europe’s Gender Diversity webinar series, September 2022.
• Steve Kremer: Seminar at TU Dresden, Germany, remote, May 2022.
• Vincent Laporte: Cambium team seminar, Paris, September 2022.
• Vincent Laporte: GLSec/SSLR seminar, Paris, November 2022.
• Christophe Ringeissen. Colloquium at the UNM, Albuquerque, USA, remote, September 2022.

11.1.5 Leadership within the scientific community

• Véronique Cortier: vice-chair of ACM Special Interest Group on Logic and Computation (SigLog)
• Véronique Cortier: member of IFIP WG-1.7 Foundations of Security Analysis
• Véronique Cortier: member of the research council of ANSSI
• Jannik Dreier: Co-chair of the working group on formal methods for security (GT MFS) of the GdR Sécurité Informatique
• Steve Kremer: member of IFIP WG-1.7 Foundations of Security Analysis
• Steve Kremer: member of the scientific directorate of the International Computer Science Meeting Center Schloss Dagstuhl
• Michaël Rusinowitch: member of the IFIP WG-11.14 Secure Engineering

11.1.6 Scientific expertise

• Véronique Cortier: member of the expert panel on Computer Science of the Research Foundation – Flanders (FWO)
• Véronique Cortier: external expertise for ANR
• Steve Kremer: jury member of the Gilles Kahn PhD award

11.1.7 Research administration

• Steve Kremer: co-chair of Inria's Committee on Gender Equality and Equal Opportunities
• Steve Kremer: member of the Board of Directors of LIST (Luxembourg Institute of Science and Technology)

11.2.1 Teaching

• Licence:

  J. Dreier, Introduction to Logic, 20 hours (ETD), TELECOM Nancy

  J. Dreier, Awareness for Cybersecurity, 7.5 hours (ETD), TELECOM Nancy

  L. Hirschi, Introduction to Theoretical Computer Science (Logic, Languages, Automata), 32 hours (ETD), TELECOM Nancy

  V. Laporte, Introduction to Theoretical Computer Science (Logic, Languages, Automata), Spring 2022, 42 hours (ETD), TELECOM Nancy

  V. Laporte, Introduction to Logic, Fall 2022, 20 hours (ETD), TELECOM Nancy

• Master:

  J. Dreier, Protocol Security and Verification, 39 hours (ETD), M2 Computer Science, TELECOM Nancy

  J. Dreier, Advanced Cryptography, 37 hours, M2 Computer Science, TELECOM Nancy

  A. Imine, Security for XML Documents, 12 hours (ETD), M1, Univ Lorraine

  L. Hirschi, Protocol Security Theory, 24 hours (ETD), M2 Computer science, Univ Lorraine

  L. Vigneron, Introduction to cryptography, 17 hours (ETD), Polytech Nancy – Information Systems and Networks, Univ Lorraine

  L. Vigneron, Advanced Security, 42 hours (ETD), Polytech Nancy – Information Systems and Networks, Univ Lorraine

  L. Vigneron, Security of information systems, 32 hours (ETD), M2 MIAGE – Audit and Design of Information Systems, Univ Lorraine

• Summer School:

  Lucca Hirschi and Virginie Lallemand co-organized the Cyber in Nancy summer school (yearly GDR Sécurité), July 2022.

  V. Laporte. High-assurance high-speed cryptography implementations in Jasmin, Cyber in Nancy Summer School, Nancy, July 2022.

11.2.2 Supervision

• PhD defended in 2022:

  Bizhan Alipour Pijani, Attribute Inference Attacks on Social Media Publications 34, March 10th 2022, Univ. Lorraine (A. Imine and M. Rusinowitch)

• PhD in progress:

  Vincent Diemunsch, Formal Analysis of Industrial Protocols, started in June 2022. (L. Hirschi and S. Kremer)

  Elise Klein, Automatic Synthesis of Cryptographic Protocols, started in October 2021. (J. Dreier and S. Kremer)

  Maïwenn Racouchot, Automated Learning of Proof Strategies in Tamarin, started in October 2021. (J. Dreier and S. Kremer)

  Quentin Yang, Design of a cast-as-intended, verifiable, and coercion-resistant electronic voting protocol, started in November 2020. (V. Cortier and P. Gaudry (project-team Caramba))

  Wafik Zahwa, Building Self-Driven Network Functions, started in October 2022. (A. Lahmadi (project-team Resist) and M. Rusinowitch)

11.2.3 Juries

11.3.1 Articles and contents

• V. Cortier has co-authored, with P. Gaudry (project-team Caramba) a book on electronic voting, published by Odile Jacob in 2022 39.
• J. Dreier has co-authored, with D. Basin (ETH Zurich), C. Cremers (CISPA), and R. Sasse (ETH Zurich), an article in the IEEE Security and Privacy Magazine 9.

11.3.2 Interventions

• V. Cortier: interview on e-voting by various medias: AFP Factuel, Ouest France, Sud Ouest, France Info, France Culture, B-Smart, RadioTélévision Suisse, Luxemburger Wort, rubrique Start des Echos, Horizons Publics, Acteurs Publics
• S, Kremer: Invited talk at the conference "Mathématiques en Mouvement" with this year's topic "Math and democracy"

International journals

• 8 articleG.Gilles Barthe, C.Charlie Jacomme and S.Steve Kremer. Universal Equivalence and Majority of Probabilistic Programs over Finite Fields.ACM Transactions on Computational Logic231January 2022, 1-42
  HALDOIback to text
• 9 articleD.David Basin, C.Cas Cremers, J.Jannik Dreier and R.Ralf Sasse. Tamarin: Verification of Large-Scale, Real World, Cryptographic Protocols.IEEE Security and Privacy Magazine2022
  HALDOIback to text
• 10 articleV.Véronique Cortier, S.Stéphanie Delaune, J.Jannik Dreier and E.Elise Klein. Automatic generation of sources lemmas in TAMARIN: towards automatic proofs of security protocols.Journal of Computer Security304August 2022, 573-598
  HALDOIback to text
• 11 articleJ.Jannik Dreier, J.-G.Jean-Guillaume Dumas, P.Pascal Lafourcade and L.Léo Robert. Optimal Threshold Padlock Systems.Journal of Computer Security305October 2022, 655-688
  HALDOIback to text
• 12 articleY.Ying Sheng, Y.Yoni Zohar, C.Christophe Ringeissen, J.Jane Lange, P.Pascal Fontaine and C.Clark Barrett. Polite Combination of Algebraic Datatypes.Journal of Automated Reasoning663August 2022, 331-355
  HALDOIback to text

International peer-reviewed conferences

• 13 inproceedingsA.Ahmad Abboud, R.Remi Garcia, A.Abdelkader Lahmadi, M.Michael Rusinowitch, A.Adel Bouhoula and M.Mondher Ayadi. Automatically Distributing and Updating In-Network Management Rules for Software Defined Networks.NOMS 2022-2022 IEEE/IFIP Network Operations and Management SymposiumBudapest, HungaryIEEEApril 2022, 1-9
  HALDOIback to text
• 14 inproceedingsB.Basavesh Ammanaghatta Shivakumar, G.Gilles Barthe, B.Benjamin Grégoire, V.Vincent Laporte and S.Swarn Priya. Enforcing Fine-grained Constant-time Policies.CCS '22: 2022 ACM SIGSAC Conference on Computer and Communications SecurityProceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (CCS ’22)Los Angeles CA, United StatesACMNovember 2022, 83-96
  HALDOIback to text
• 15 inproceedingsB.Bruno Blanchet, V.Vincent Cheval and V.Véronique Cortier. ProVerif with Lemmas, Induction, Fast Subsumption, and Much More.S&P 2022 - 43rd IEEE Symposium on Security and PrivacySan Francisco, United StatesMay 2022
  HALback to textback to text
• 16 inproceedingsM.Mikaël Bougon, H.Hervé Chabanne, V.Véronique Cortier, A.Alexandre Debant, E.Emmanuelle Dottax, J.Jannik Dreier, P.Pierrick Gaudry and M.Mathieu Turuani. Themis: an On-Site Voting System with Systematic Cast-as-intended Verification and Partial Accountability.CCS 2022 - The ACM Conference on Computer and Communications SecurityLos Angeles, United StatesACM2022
  HALDOIback to text
• 17 inproceedingsV.Vincent Cheval, C.Cas Cremers, A.Alexander Dax, L.Lucca Hirschi, C.Charlie Jacomme and S.Steve Kremer. Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses.32nd USENIX Security SymposiumAnaheim, United States2023
  HALback to text
• 18 inproceedingsV.Vincent Cheval, R.Raphaëlle Crubillé and S.Steve Kremer. Symbolic protocol verification with dice: process equivalences in the presence of probabilities.CSF'22 - 35th IEEE Computer Security Foundations SymposiumHaifa, IsraelAugust 2022
  HALback to text
• 19 inproceedings V.Vincent Cheval, C.Charlie Jacomme, S.Steve Kremer and R.Robert Künnemann. Sapic+ : protocol verifiers of the world, unite! USENIX 2022 - 31st USENIX Security Symposium Boston, United States August 2022
  HAL back to text
• 20 inproceedingsV.Véronique Cortier, A.Antoine Dallon and S.Stéphanie Delaune. A small bound on the number of sessions for security protocols.CSF 2022 - 35th IEEE Computer Security Foundations SymposiumHaifa, IsraelAugust 2022
  HALback to text
• 21 inproceedingsV.Véronique Cortier, P.Pierrick Gaudry and S.Stéphane Glondu. Features and usage of Belenios in 2022.The International Conference for Electronic Voting (E-Vote-ID 2022)Bregenz / Hybrid, AustriaOctober 2022
  HALback to text
• 22 inproceedingsV.Véronique Cortier, P.Pierrick Gaudry and Q.Quentin Yang. A toolbox for verifiable tally-hiding e-voting systems.ESORICS 2022 - 27th European Symposium on Research in Computer SecurityCopenhague, DenmarkSeptember 2022
  HALback to text
• 23 inproceedingsC.Cas Cremers, C.Caroline Fontaine and C.Charlie Jacomme. A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols.S&P 2022 - 43rd IEEE Symposium on Security and PrivacySan Francisco / Virtual, United StatesMay 2022
  HAL
• 24 inproceedingsC. C.Constantin Catalin Dragan, F.Francois Dupressoir, E.Ehsan Estaji, K.Kristian Gjøsteen, T.Thomas Haines, P. Y.Peter Y.A. Ryan, P.Peter Rønne and M. R.Morten Rotvold Solberg. Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co.Lecture Notes in Computer Science2022 IEEE 35th Computer Security Foundations Symposium (CSF)Haifa, IsraelIEEEAugust 2022, 335-347
  HALDOIback to text
• 25 inproceedingsF.-E.Fatima-Ezzahra El Orche, R.Rémi Géraud-Stewart, P.Peter Rønne, G.Gergei Bana, D.David Naccache, P. Y.Peter Y. A. Ryan, M.Marco Biroli, M.Megi Dervishi and H.Hugo Waltsburger. Time, Privacy, Robustness, Accuracy: Trade-Offs for the Open Vote Network Protocol.Lecture Notes in Computer ScienceInternational Joint Conference on Electronic Voting 202213553Lecture Notes in Computer ScienceBregenz, AustriaSpringer International PublishingSeptember 2022, 19-35
  HALDOIback to text
• 26 inproceedingsS.Serdar Erbatur, A. M.Andrew M. Marshall and C.Christophe Ringeissen. Combined Hierarchical Matching: the Regular Case.7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)228Leibniz International Proceedings in Informatics (LIPIcs)Haifa, IsraelSchloss Dagstuhl -- Leibniz-Zentrum für InformatikAugust 2022, 6:1--6:22
  HALDOIback to text
• 27 inproceedingsK.Kristian Gjøsteen, T.Thomas Haines, J.Johannes Müller, P.Peter Rønne and T.Tjerand Silde. Verifiable Decryption in the Head.Lecture Notes in Computer ScienceAustralasian Conference on Information Security and Privacy13494Lecture Notes in Computer ScienceWollongong, AustraliaSpringer International PublishingNovember 2022, 355-374
  HALDOIback to text
• 28 inproceedingsC.Charlie Jacomme, E.Elise Klein, S.Steve Kremer and M.Maïwenn Racouchot. A comprehensive, formal and automated analysis of the EDHOC protocol.USENIX Security '23 - 32nd USENIX Security SymposiumAnaheim, CA, United StatesAugust 2023
  HALback to text
• 29 inproceedingsA. E.Ala Eddine Laouir and A.Abdessamad Imine. On Privacy of Multidimensional Data Against Aggregate Knowledge Attacks.Lecture Notes in Computer SciencePSD 2022 : PRIVACY IN STATISTICAL DATABASES 202213463International Conference on Privacy in Statistical Databases, PSD 2022Paris, FranceSpringer ChamSeptember 2022, 13
  HALDOIback to text
• 30 inproceedingsK.Kamal Macwan, A.Abdessamad Imine and M.Michaël Rusinowitch. Differentially Private Friends Recommendation.Lecture Notes in Computer ScienceThe 15th International Symposium on Foundations & Practice of SecurityOttawa (Ontario), CanadaSpringerDecember 2022
  HALback to text
• 31 inproceedingsK.Kamal Macwan, A.Abdessamad Imine and M.Michaël Rusinowitch. Privacy Preserving Recommendations for Social Networks.The 9th International Conference on Social Networks Analysis, Management and SecurityMilan, ItalyIEEENovember 2022
  HALback to text

Conferences without proceedings

• 32 inproceedingsV.Véronique Cortier, A.Alexandre Debant and P.Pierrick Gaudry. A privacy attack on the Swiss Post e-voting system.RWC 2022 - Real World Crypto SymposiumAmsterdam (NETHERLANDS), NetherlandsNovember 2021
  HALback to text
• 33 inproceedingsS.Saraid Dwyer Satterfield, S.Serdar Erbatur, A. M.Andrew M Marshall and C.Christophe Ringeissen. Graph-Embedded Term Rewrite Systems and Applications (A Preliminary Report).36th International Workshop on UnificationHaifa, IsraelAugust 2022
  HALback to text

Doctoral dissertations and habilitation theses

• 34 thesisB. A.Bizhan Alipour Pijani. Attribute inference attacks on social media publications.Université de LorraineMarch 2022
  HALback to textback to text

Reports & preprints

• 35 miscD.David Baelde, A.Alexandre Debant and S.Stéphanie Delaune. Proving Unlinkability using ProVerif through Desynchronized Bi-Processes.May 2022
  HAL
• 36 miscV.Vincent Cheval, R.Raphaëlle Crubillé and S.Steve Kremer. Symbolic protocol verification with dice: process equivalences in the presence of probabilities (extended version).June 2022
  HAL
• 37 misc V.Véronique Cortier, P.Pierrick Gaudry and Q.Quentin Yang. Is the JCJ voting system really coercion-resistant? April 2022
  HAL
• 38 miscA.Alexandre Debant and L.Lucca Hirschi. Reversing, Breaking, and Fixing the French Legislative Election E-Voting Protocol.November 2022
  HALback to text

Scientific popularization

• 39 bookV.Véronique Cortier and P.Pierrick Gaudry. Le vote électronique - les défis du secret et de la transparence.Odile JacobMay 2022
  HALback to textback to text