Loading Seminars

« All Seminars

  • This seminar has passed.

Symbolic protocol verification with dice: process equivalences in the presence of probabilities

September 21 (2022) @ 3:00 pm - 4:00 pm

Abstract: Symbolic protocol verification generally abstracts probabilities away, considering computations that succeed only with negligible probability, such as guessing random numbers or breaking an encryption scheme, as impossible. This abstraction, sometimes referred to as the perfect cryptography assumption, has shown very useful as it simplifies automation of the analysis. However, probabilities may also appear in the control flow where they are generally not negligible. In this paper we consider a framework for symbolic protocol analysis with a probabilistic choice operator: the probabilistic applied pi calculus. We define and explore the relationships between several behavioral equivalences. In particular we show the need for randomized schedulers and exhibit a counter-example to a result in a previous work that relied on non-randomized ones. As in other frameworks that mix both non-deterministic and probabilistic choices, schedulers may sometimes be unrealistically powerful. We therefore consider two subclasses of processes that avoid this problem. In particular, when considering purely non-deterministic protocols, as is done in classical symbolic verification, we show that a probabilistic adversary has-maybe surprisingly-a strictly superior distinguishing power for may testing, which, when the number of sessions is bounded, we show to coincide with purely possibilistic similarity.

This is joint work with Vincent Cheval and Raphaëlle Crubillé.

Joint seminar with the FM-SEC network.

Attendance via Zoom (ID: 930 9704 3118, Passcode: 493163)

Livestream via YouTube


September 21 (2022)
3:00 pm - 4:00 pm
Seminar Tags:


Steve Kremer (Inria Nancy)

Steve Kremer is research director at Inria Nancy and Université de Lorraine where he leads the PESTO research team on formal methods and security. Steve received his PhD in computer science from Université Libre de Bruxelles in 2003 and his Habilitation in computer science from ENS Cachan in 2011. From 2004 to 2011 He held a tenured research position at ENS Cachan. In 2015 he was awarded an ERC Consolidator grant to work on automated verification of cryptographic protocols.

View Presenter Website

Leave a Reply

Your email address will not be published. Required fields are marked *