key: 2016-verifying-observational-equivalence
type: inproceedings
title: Automated reasoning for equivalences in the applied pi calculus with barriers
authors:
  - Bruno Blanchet
  - Ben Smyth
year: 2016
month: 4
booktitle: "CSF'16: 29th Computer Security Foundations Symposium"
pages: 310--324
publisher: IEEE Computer Society
doi: 10.1109/CSF.2016.29
description: This paper extends ProVerif to enable the automated proof of more observational equivalences.
keywords: >-
  anonymity, applied pi calculus, automated reasoning, ballot secrecy, barrier synchronisation,
  electronic voting, equivalence, e-voting, FOO, formal methods, Lee et al., privacy, ProSwapper,
  ProVerif, security protocols, verification, voting
abstract: >-
  Observational equivalence allows us to study important security properties such as anonymity.
  Unfortunately, the difficulty of proving observational equivalence hinders analysis. Blanchet,
  Abadi & Fournet simplify its proof by introducing a sufficient condition for observational
  equivalence, called diff-equivalence, which is a reachability condition that can be proved
  automatically by ProVerif. However, diff-equivalence is a very strong condition, which often does
  not hold even if observational equivalence does. In particular, when proving equivalence between
  processes that contain several parallel components, e.g., <tt>P|Q</tt> and <tt>P'|Q'</tt>,
  diff-equivalence requires that <tt>P</tt> is equivalent to <tt>P'</tt> and <tt>Q</tt> is
  equivalent to <tt>Q'</tt>. To relax this constraint, Delaune, Ryan &amp; Smyth introduced the idea
  of swapping data between parallel processes <tt>P'</tt> and <tt>Q'</tt> at synchronisation points,
  without proving its soundness. We extend their work by formalising the semantics of
  synchronisation, formalising the definition of swapping, and proving its soundness. We also relax
  some restrictions they had on the processes to which swapping can be applied. Moreover, we have
  implemented our results in ProVerif. Hence, we extend the class of equivalences that can be proved
  automatically. We showcase our results by analysing privacy in election schemes by Fujioka,
  Okamoto &amp; Ohta and Lee <i>et al.</i>, and in the vehicular ad-hoc network by Freudiger <i>et
  al.</i>
supersededby:
  - key: 2017-verifying-observational-equivalence
    text: journal version
links:
  - file: Smyth16-verifying-observational-equivalence.pdf
    text: Conference paper
  - url: http://proverif.inria.fr
    text: ProVerif
  - url: http://proverif.inria.fr
    text: ProVerif
  - url: https://doi.org/10.1109/CSF.2016.29
    text: Official version