Sommaire

  • Cet exposé a été présenté le 16 avril 2021.

Description

  • Orateur

    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.

Infos pratiques

Prochains exposés

  • [CANCELLED] Black-Box Collision Attacks on Widely Deployed Perceptual Hash Functions and Their Consequences

    • 13 juin 2025 (11:00 - 12:00)

    • Inria Center of the University of Rennes - Aurigny room

    Orateur : Diane Leblanc-Albarel - KU Leuven

    [CANCELLED] Perceptual hash functions identify multimedia content by mapping similar inputs to similar outputs. They are widely used for detecting copyright violations and illegal content but lack transparency, as their design details are typically kept secret. Governments are considering extending the application of these functions to Client-Side Scanning (CSS) for end-to-end encrypted services:[…]

    • Cryptography

    • SoSysec

    • Protocols

  • A non-comparison oblivious sort and its application to private k-NN

    • 20 juin 2025 (11:00 - 12:00)

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

    Orateur : Sofiane Azogagh - UQÀM

    Sorting is a fundamental subroutine of many algorithms and as such has been studied for decades. A well-known result is the Lower Bound Theorem, which states that no comparison-based sorting algorithm can do better than O(nlog(n)) in the worst case. However, in the fifties, new sorting algorithms that do not rely on comparisons were introduced such as counting sort, which can run in linear time[…]

    • Cryptography

    • SoSysec

    • Privacy

    • Databases

    • Secure storage

Voir les exposés passés
Haut de page