Description
Providing security proofs instead of arguing lack of existing relevant attacks is a quite new approach when it comes to cryptography. In the last thirty years, a lot of work has been done to formalize security of systems and prove of the achievement of security criteria. It has resulted in the design of a great number of proofs under various hypotheses. Though a step in the right direction, these pencil-and-paper proofs are so numerous, involved and technical that the community has difficulty to carefully check them. The well-known example of the encryption scheme OAEP whose security proof, apparently correct, was corrected seven years after its publication illustrates that security-dedicated verification tools need to be designed. Our work takes place in the so-called computational model, where messages are considered to be bitstrings, and system adversaries are probabilistic Turing machines. A proof of security is then a complexity-theoretic reduction argument: the probability of success of an adversary in solving a security challenge is reduced to its ability to solve a known difficult problem (given a fixed amount of resources). Firstly, we provide some intuition on usual security requirements, and common sketches of security proofs. Then, we present a semantics and a logic to formalize security proofs. One could say there are several levels in automatic proving: computer-aided verification of proofs, computer-aided design of proofs, and automatic generation of proofs. We show how our inference rules can be used to derive proofs and verify them automatically, or sometimes perform a proof search using some additional inputs.
Next sessions
-
Cyclotomic Cosets: Hidden Subgroup and Quantum Sieving Algorithm for Prime-Power Moduli
Speaker : 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
Speaker : 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[…] -
Post-quantum day of the cryptography seminar
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. -
Chiffrement homomorphe à l'aide des groupes après Nuida
Speaker : 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
-
-
Post-Quantum Signatures from Symmetric-Key-Friendly Techniques: From MPC-in-the-Head to VOLE-in-the-Head
Speaker : Dung Bui - Northwestern University
The MPC-in-the-Head (MPCitH) paradigm turns a secure multiparty computation protocol into a zero-knowledge proof and, via Fiat–Shamir, into a signature scheme whose security relies only on symmetric-key primitives. The framework of Katz, Kolesnikov and Wang (KKW, CCS18), which moves most of the MPC work into a committed preprocessing phase that the verifier checks by opening all-but-one of the[…] -
Nouveaux doctorants
Exposés courts des nouveaux doctorants (Elouan, Quentin, Eliot)