Table of contents

  • This session has been presented February 08, 2019.

Description

  • Speaker

    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.

Practical infos

  • Presentation documents

Next sessions

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

    • December 06, 2024 (11:00 - 12:00)

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

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

    • Privacy

    • Machine learning

    • Distributed systems

  • Safety-Security Convergence of Industrial Control Systems

    • December 13, 2024 (11:00 - 12:00)

    • Inria Center of the University of Rennes - Room Aurigny

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

    • Intrusion detection

Show previous sessions
Page top