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

  • Vers l’émergence d’un droit européen pour la Blockchain : Une approche sous l’angle de la Privacy et de l’encadrement des crypto-actifs

    • December 05, 2025 (10:00 - 11:00)

    • Inria Center of the University of Rennes - Aurigny room

    Speaker : Damien Franchi - Univ Rennes, IODE

    La Blockchain, technologie derrière Bitcoin, fait l’objet d’un encadrement juridique de plusen plus important, en particulier de la part de l’Union européenne. Curieusement, le mot« Blockchain » n’apparaît pas dans les textes l’encadrant. Les expressions « technologie deregistres distribués » (Distributed ledger technology, DLT), ou, parfois, « registreélectronique » lui sont plutôt privilégiées.[…]

    • SoSysec

    • Law

  • Blockchain and digital currencies: between European regulation and technological challenges

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

    • Inria Center of the University of Rennes - Aurigny room

    Speaker : Loïc Miller - CentraleSupélec

    As the European Union develops a legal framework for crypto-assets and data protection, the technological question underlying the emergence of a genuine digital currency remains open. Blockchain today stands as an interdisciplinary field of study at the crossroads of computer science, economics, and law. This presentation will place the ongoing regulatory framework in perspective with the[…]

    • SoSysec

    • Distributed systems

  • 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

Show previous sessions
Page top