key: 2017-verifying-observational-equivalence
type: article
title: Automated reasoning for equivalences in the applied pi calculus with barriers
authors:
  - Bruno Blanchet
  - Ben Smyth
year: 2018
journal: Journal of Computer Security
volume: "26"
number: "3"
pages: 367--422
doi: 10.3233/JCS-171013
description: This article 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, Lee <i>et al.</i>, and Juels, Catalano &amp; Jakobsson, and in the vehicular
  ad-hoc network by Freudiger <i>et al.</i>
links:
  - file: Smyth17-verifying-observational-equivalence.pdf
    text: Journal article
  - url: http://proverif.inria.fr
    text: ProVerif
  - url: http://proverif.inria.fr
    text: ProVerif
  - url: https://doi.org/10.3233/JCS-171013
    text: Official version