Table of contents

  • This session has been presented April 16, 2021.

Description

  • Speaker

    David Baelde (ENS Cachan)

Formal methods have brought several approaches for proving that security protocols ensure the expected security and privacy properties. Most of the resulting tools analyze protocols in symbolic models, aka. Dolev-Yao-style models. Security in the symbolic model does not imply security in the cryptographer’s standard model, the computational model, where attackers are arbitrary (PPTIME) Turing machines. Computer-assisted verification techniques for the computational model have appeared only recently, and are generally less flexible or less automated than in the symbolic model. In some recent work, several colleagues and myself have proposed a new approach, elaborating on the CCSA logic of Gergei Bana and Hubert Comon. We have implemented it in a new proof assistant, Squirrel, and validated it on a variety of case studies. In this talk, I will present this approach, its benefits, and some of the remaining challenges.This is based on work with Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos and Solène Moreau, which has been accepted at S&P’21.

Practical infos

Next sessions

  • Hardware-Software Co-Designs for Microarchitectural Security

    • December 11, 2025 (11:00 - 12:00)

    • Inria Center of the University of Rennes - Room Petri/Turing

    Speaker : Lesly-Ann Daniel - EURECOM

    Microarchitectural optimizations, such as caches and speculative out-of-order execution, are essential for achieving high performance. However, these same mechanisms also open the door to attacks that can undermine software-enforced security policies. The current gold standard for defending against such attacks is the constant-time programming discipline, which prohibits secret-dependent control[…]

    • SoSysec

    • Hardware/software co-design

    • Micro-architectural vulnerabilities

  • Should I trust or should I go? A deep dive into the (not so reliable) web PKI trust model

    • December 19, 2025 (11:00 - 12:00)

    • Inria Center of the University of Rennes - Room Markov

    Speaker : Romain Laborde - University of Toulouse

    The padlock shown in the URL bar of our favorite web browser indicates that we are connected using a secure HTTPS connection and providing some sense of security. Unfortunately, the reality is slightly more complex. The trust model of the underlying Web PKI is invalid, making TLS a colossus with feet of clay. In this talk, we will dive into the trust model of the web PKI ecosystem to understand[…]

    • SoSysec

    • Protocols

    • Network

Show previous sessions
Page top