Sommaire

  • Cet exposé a été présenté le 28 novembre 2025 (13:45 - 14:45).

Description

  • Orateur

    Bruno Blanchet - Inria

CryptoVerif is a security protocol verifier sound in the computational model of cryptography. It produces proofs by sequences of games, like those done manually by cryptographers. It has an automatic proof strategy and can also be guided by the user. It provides a generic method for specifying security assumptions on many cryptographic primitives, and can prove secrecy, authentication, and indistinguishability properties. A successful proof guarantees asymptotic security, in the presence of polynomial-time adversaries, and also provides an exact security bound of the probability of success of an attack as a function of the probability of breaking the primitives.

After a general introduction to CryptoVerif, we will focus on recent extensions introduced for dealing with key compromise. We will also briefly mention a few other recent results: post-quantum CryptoVerif, CV2EC, CV2F*.
 

Infos pratiques

Prochains exposés

  • Predicting Module-Lattice Reduction

    • 19 décembre 2025 (13:45 - 14:45)

    • Batiment 22-23 salle 16 (en face de l'amphi Lebesgue)

    Orateur : Paola de Perthuis - CWI

    Is module-lattice reduction better than unstructured lattice reduction? This question was highlighted as `Q8' in the Kyber NIST standardization submission (Avanzi et al., 2021), as potentially affecting the concrete security of Kyber and other module-lattice-based schemes. Foundational works on module-lattice reduction (Lee, Pellet-Mary, Stehlé, and Wallet, ASIACRYPT 2019; Mukherjee and Stephens[…]
    • Cryptography

  • Séminaire C2 à INRIA Paris

    • 16 janvier 2026 (10:00 - 17:00)

    • INRIA Paris

    Emmanuel Thomé et Pierrick Gaudry Rachelle Heim Boissier Épiphane Nouetowa Dung Bui Plus d'infos sur https://seminaire-c2.inria.fr/ 
  • Attacking the Supersingular Isogeny Problem: From the Delfs–Galbraith algorithm to oriented graphs

    • 23 janvier 2026 (13:45 - 14:45)

    • IRMAR - Université de Rennes - Campus Beaulieu Bat. 22, RDC, Rennes - Amphi Lebesgue

    Orateur : Arthur Herlédan Le Merdy - COSIC, KU Leuven

    The threat of quantum computers motivates the introduction of new hard problems for cryptography.One promising candidate is the Isogeny problem: given two elliptic curves, compute a “nice’’ map between them, called an isogeny.In this talk, we study classical attacks on this problem, specialised to supersingular elliptic curves, on which the security of current isogeny-based cryptography relies. In[…]
    • Cryptography

Voir les exposés passés