@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@inproceedings{CCK-csf22,
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 to require randomized
schedulers-indeed we exhibit a counterexample to one
of the main results 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. 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. Finally, we consider fully
probabilistic protocols and show that trace
equivalence corresponds to a notion of may testing
with purely probabilistic attackers. We also briefly
discuss complexity and automation for these
subclasses when the number of sessions is bounded. },
address = {Haifa, Israel},
author = {Cheval, Vincent and Crubill{\'{e}}, Rapha{\"{e}}lle and Kremer,
Steve},
booktitle = {{P}roceedings of the 35th IEEE Computer Security
Foundations Symposium (CSF'22)},
doi = {10.1109/CSF54842.2022.00020},
month = aug,
pages = {303-318},
publisher = {{IEEE} Computer Society Press},
title = {Symbolic protocol verification with dice: process equivalences in the presence of probabilities},
year = 2022,
acronym = {{CSF}'22},
nmonth = 8,
}