Get the paper

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., P | Q and P' | Q', diff-equivalence requires that P is equivalent to P' and Q is equivalent to Q'.
To relax this constraint, Delaune, Ryan & Smyth introduced the idea of swapping
data between parallel processes P' and Q' 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 & Ohta, Lee et al., and Juels, Catalano & Jakobsson,
and in the vehicular ad-hoc network by Freudiger et al.