Sommaire

  • Cet exposé a été présenté le 08 février 2019.

Description

  • Orateur

    Ross Horne (University of Luxembourg)

The pi-calculus was introduced for verifying cryptographic protocols by Abadi and Fournet in 2001. They proposed an equivalence technique, called bisimilarity, useful for verify privacy properties. It is widely acknowledged (cf. Paige and Tarjan 1987), that bisimilarity is more efficient to check than trace equivalence; however, surprisingly, tools based on the applied pi-calculus typically still implement trace equivalence. I suggest this may be attributed to two problems:1. Abadi and Fournet did not publish proofs following conference paper from 2001, until a journal version in 2018 with Blanchet. This perhaps reduced the confidence of the community in bisimilarity. Further to providing proofs, the journal version adjusts definitions to avoid some well known limitations in the original presentation.2. To efficiently implement bisimulation for extensions of the pi-calculus, we typically require a bisimilarity congruence, and no bisimilarity congruence has been proposed for the applied pi-calculus.To address the second point above I propose a bisimilarity congruence for the applied pi-calculus. I argue that the definition I provide is optimal; and show that it is sufficiently strong to verify privacy properties. The definition makes use of recent advances in concurrency theory that were not available prior to LICS 2018. Furthermore, these results lead us to the first sound and complete modal logic for the applied pi-calculus, that can specify attacks if and only if an attack exists.

Infos pratiques

  • Presentation documents

Prochains exposés

  • The Battle Against Bots: Current Threats and New Directions to Counter Automated Attacks

    • 22 novembre 2024 (11:00 - 12:00)

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

    Orateur : Elisa Chiapponi - Amadeus IT Group

    In today's digital landscape, the battle between industry and automated bots is an ever-evolving challenge. Attackers are leveraging advanced techniques such as residential proxies, CAPTCHA farms, and AI-enhanced fingerprint rotations to evade detection and execute functional abuse attacks, including web scraping, denial of inventory, and SMS pumping.  This talk will explore ongoing efforts[…]
    • SoSysec

    • Détection d'intrusion

  • 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