Symbolic protocol verification with dice: process equivalences in the presence of probabilities
Vincent Cheval, Raphaëlle Crubillé, and Steve Kremer. Symbolic protocol verification with dice: process equivalences in the presence of probabilities. In Proceedings of the 35th IEEE Computer Security Foundations Symposium (CSF'22), pp. 303–318, IEEE Computer Society Press, Haifa, Israel, August 2022.
doi:10.1109/CSF54842.2022.00020
Download
[PDF] [PDF (long version)] [HTML]
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.
BibTeX
@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,
}