Description
A scientific day devoted to post-quantum cryptography, held in the wake of the European Cyber Week, with talks more technical than those presented at the ECW.
The talks will take place at Amphi E in building 02A. To register for lunch, please do so before oct 30th using this link.
The Program
-
9:00 - 9:30
Welcome
-
9:30 -10:15
TBD
Gustavo Banegas (Inria)
-
10:15 - 10:45
Coffee break
-
10:45 - 11:30
A Scalable Fault Countermeasure for SLH-DSA: Trade-offs Between Memory, Performance, and Fault Resilience
Melissa Azouaoui (NXP)
Fault attacks against SLH-DSA can enable grafting tree attacks and accordingly signature forgery. This talk presents compressed caching, a scalable and configurable countermeasure that significantly reduces memory requirements while maintaining strong fault-detection capabilities. We discuss the security, performance, and memory trade-offs of compressed and standard caching, and show how compressed caching is particularly well-suited for resource-constrained devices.
-
11:30 - 12:15
RAM and CPU efficient techniques for Falcon implementation
Thomas Pornin (NCC Group)
We present various techniques to help software implementations of the Falcon signature scheme achieve both RAM and CPU efficiency, with a particular focus on small embedded systems (Arm Cortex M4 micrcontrollers). Some of the methods allow replacing operations on floating-point (or fixed-point) values with smaller and faster operations on modular integers; moving the addition of the target vector to a later point in the processing removes the need for some FFT transforms. For the FFT itself, a novel variant is presented, which halves the number of operations, and should be generally applicable to other algorithms that use the FFT or the NTT. All the techniques are compatible with a replacement of floating-point values and operations with a fixed-point format; in total, on Arm Cortex M4, we can halve both the RAM usage and the CPU cost of signature generation.
-
12:15 - 13:30
Lunch (on site)
-
13:30 - 14:20
Cryptanalysis of the signature scheme Hawk
Alice Pellet-Mary (CNRS, Univ. Bordeaux)
In this talk, I will present an algorithm solving the lattice isomorphism problem in modules of rank 2 (module-LIP) over a cyclotomic number field. This algorithm reduces the underlying lattice dimension by a factor 3/4, which improves the complexity of the best known attack to solve module-LIP in these lattices (the algorithm still runs in exponential time, but with a smaller constant in the exponent).
This impacts the signature scheme Hawk, making its concrete security fall short of the NIST requirement for all security levels considered (I and V).
Finally, I will also discuss and compare with the two concurrent attacks on Hawk (by anthropic and Luo at al.). This is a joint work with Guilhem Mureau and Ludo Pulles. -
14:20 - 15:10
From Toy to Instrument: Seven Years of Verifpal
Nadim Kobeissi (Symbolic Software)
Protocol verification tools have grown more expressive with every paper, and harder to pick up with every release. Most end up used by the group that built them and almost nobody else. Verifpal goes the other way: it is built around the person writing the model, with a small language you can read out loud, an active attacker, and output that names the attack instead of leaving you to reconstruct it. When I published it in 2019, that choice was expensive: Its paper called its own soundness argument "an incomplete, semi-formal, in-progress set of results," and the fair verdict was that Verifpal was a teaching aid resembling a verification tool. That verdict was correct. People used it anyway, on Signal, TLS 1.3, MTProto, ProtonMail, and during the design of Zoom's end-to-end encryption.
Seven years later, Verifpal has matured from toy to instrument. While the 2019 engine searched forward, the current engine starts from an unresolved query and searches backward through the conditions needed to violate it. Before reporting an attack, a separate validator checks that the attacker controls every modified slot and can derive every injected term, re-executes the protocol, and evaluates the query again. We prove that every reported attack is reachable in the bounded sequential-replay semantics defined here, independently of solver correctness. Because this semantics reuses a clone's fresh values across sequential replays, it can admit witnesses that replication would exclude; the output labels such witnesses.
The language now supports key encapsulation (allowing it to express post-quantum style primitives) explicit weakening assumptions (allowing it to better express hybrid protocols and harvest now, decrypt later attacks), concurrent sessions, and multiple peer configurations. We compare Verifpal's results and counterexamples with those of ProVerif, Tamarin, and Scyther on a corpus of classical protocols.
This talk will also cover a critique against the entire field of protocol modeling and analysis tools, Verifpal included: symbolic verifiers are exploratory instruments, much closer to an interactive notebook for reasoning about a protocol than to any real assurance or proof tool, and reading a verdict from Tamarin, ProVerif or Verifpal as more than that has always been presumptuous. In order to truly advance the field of protocol modeling, it must be reframed for what it really is. Only then will we be able to realign our incentives on priorities to focus on who it can really benefit: real-world industry practitioners, not academics.
Infos pratiques
Prochains exposés
-
Cyclotomic Cosets: Hidden Subgroup and Quantum Sieving Algorithm for Prime-Power Moduli
Orateur : Mathias Boucher - Université de Rennes
The Dihedral Coset Problem (DCP), also known as the hidden shift problem, plays a fundamental role in post-quantum public-key cryptography, since the Learning-With-Error problem reduces to DCP. The “Simon meets Kuperberg” quantum algorithm by Bonnetain and Naya-Plasencia solves the DCP in quasi-polynomial time when the modulus is a power of two. We provide a generalization of this algorithm for[…] -
Adelic reduction of module lattices
Orateur : Henry Bambury - DGA-MI et Inria Rennes
We give a strict generalisation of the LLL algorithm over number fields, based on the reduction theory of $GL(n)$ over the adele ring of a number field. Our algorithm is free of heuristics, with rigorous bounds on output quality and complexity. -- based on joint work with Seungki Kim, Changmin Lee and Phong Nguyen ---
Cryptography
-
-
European Cyber Week: atelier cryptographie post-quantique
Dans la continuité des éditions 2021, 2022 et 2024, la DGA — en partenariat avec CREACH LABS et avec le soutien de l'ANSSI, de l'IRISA, de l'IRMAR et du Pôle d'Excellence Cyber — organise la 4e édition de l'atelier consacré à la cryptographie post-quantique dans le cadre de l'European Cyber Week 2026. Attention, il faut s'inscrire (gratuitement) au préalable — s'inscrire à la conférence Les[…] -
Chiffrement homomorphe à l'aide des groupes après Nuida
Orateur : Pierre Guillot - Ravel Technologies/Université de strasbourg
Nuida et d'autres ont montré comment on peut obtenir un protocole de chiffrement pleinement homomorphe si l'on sait chiffrer les éléments d'un groupe G convenable, tout en sachant faire l'opération de G "en homomorphe". Les exemples étaient jusqu'à présent limités au chiffrement d'un bit à la fois, avec beaucoup d'opérations à effectuer pour "simuler" les portes logiques usuelles. Je vais[…]-
Cryptography
-