@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@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,
  url =          {https://hal.inria.fr/hal-03700492/document},
}