Table of contents

  • This session has been presented January 06, 2006.

Description

  • Speaker

    Bruno Blanchet - ENS

We present a technique for the verification of cryptographic protocols, based on an abstract representation of the protocol by a set of Horn clauses, and on a resolution algorithm on these clauses. This technique allows a flexible encoding of many cryptographic primitives. It can verify a wide range of security properties of the protocols, such as secrecy, authenticity, and limited cases of process equivalences, in a fully automatic way. Furthermore, the obtained security proofs are valid for an unbounded number of sessions of the protocol, in parallel or not.

Next sessions

  • Séminaire C2 à INRIA Paris

    • January 16, 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

    • January 23, 2026 (13:45 - 14:45)

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

    Speaker : 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

Show previous sessions
Page top