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

  • Un protocole SMPC de curation de données d'entrainement et sa fragilité aux hypothèses de sécurité...

    • 06 décembre 2024 (11:00 - 12:00)

    • Inria Center of the University of Rennes - Métiviers room

    Orateur : Marc-Olivier Killijian - Université du Québec à Montréal

    ... ou "Sécurité et insécurité - dans quel état j’erre, ai-je bien rangé mon modèle de sécurité ?" De nos jours, les sources de données, et leurs curateurs, sont répartis à travers le monde. Il arrive que les propriétaires de ces données souhaitent collaborer entre eux afin d’augmenter la qualité de ces données, particulièrement avant d’entrainer des modèles d’apprentissage machine.Dans cet exposé[…]

    • SoSysec

    • Respect de la vie privée

    • Apprentissage machine

    • Systèmes distribués

  • Safety-Security Convergence of Industrial Control Systems

    • 13 décembre 2024 (11:00 - 12:00)

    • Inria Center of the University of Rennes - Room Aurigny

    Orateur : Maxime Puys - Université Clermont Auvergne - IUT de Clermont-Ferrand

    Industrial Control Systems (ICS) are designed to provide a service, such as power generation or water treatment, while protecting people, assets, and the environment against hazards. However, ICS now integrate Information Technology (IT) and are interconnected with the outside world such as the Internet, thereby exposing their infrastructures to cyberattacks. Cyberattacks have thus become new[…]

    • SoSysec

    • Détection d'intrusion

Voir les exposés passés
Haut de page