Description
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
Prochains exposés
-
What you never wanted to know about vulnerability databases
Orateur : Henrik Plate - Endor Labs
Vulnerability databases play a crucial role in modern software security, serving as the backbone for Application Security (AppSec) and Software Composition Analysis (SCA) tools. However, the accuracy and reliability of these databases vary significantly, often leading to misinformed security decisions. This talk explores the challenges associated with vulnerability databases, including incomplete[…]-
Risk Assessment
-
SoSysec
-
Vulnerability management
-
-
CHERIoT RTOS: An OS for Fine-Grained Memory-Safe Compartments on Low-Cost Embedded Devices
Orateur : Hugo Lefeuvre - The University of British Columbia
Embedded systems do not benefit from strong memory protection, because they are designed to minimize cost. At the same time, there is increasing pressure to connect embedded devices to the internet, where their vulnerable nature makes them routinely subject to compromise. This fundamental tension leads to the current status-quo where exploitable devices put individuals and critical infrastructure[…]-
SoSysec
-
Compartmentalization
-
Operating system and virtualization
-
Hardware/software co-design
-
Hardware architecture
-