Automated reasoning for equivalences in the applied pi calculus with barriers
Preuve automatique d'équivalences dans le pi calcul appliqué avec barrières
Résumé
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 and Lee et al., and in the vehicular ad-hoc network by
Freudiger et al.
L'équivalence observationnelle permet d'étudier des propriétés de
sécurité importantes, comme l'anonymat. Malheureusement,
l'équivalence observationnelle est difficile à prouver, ce qui
entrave l'analyse. Blanchet, Abadi & Fournet simplifient sa preuve
en introduisant une condition suffisante pour l'équivalence
observationnelle, appelée diff-équivalence, qui est une condition
d'accessibilité qui peut être prouvée automatiquement par ProVerif.
Cependant, la diff-équivalence est une condition très forte, qui est
souvent fausse même quand l'équivalence observationnelle est vraie.
En particulier, quand on prouve l'équivalence entre des processus
qui contiennent plusieurs composants en parallèle, par exemple P
| Q et P' | Q', la diff-équivalence requiert que P soit
équivalent à P' et Q à Q'. Pour relâcher cette contrainte,
Delaune, Ryan & Smyth ont introduit l'idée d'échanger des données
entre les processus parallèles P' et Q' à des points de
synchronisation, sans prouver sa correction. Nous étendons leur
travail en formalisant la sémantique de la synchronisation,
formalisant la définition de l'échange, et prouvant sa
correction. Nous relâchons également certaines contraintes qu'ils
avaient sur les processus auxquels l'échange peut être appliqué. De
plus, nous avons implémenté nos résultats dans ProVerif. Nous
étendons donc la classe d'équivalences qui peuvent être prouvées
automatiquement. Nous illustrons nos résultats en analysant des
propriétés de secret (privacy) dans des protocoles de vote
électronique par Fujioka, Okamoto & Ohta et Lee et al., et
dans le réseau ad-hoc de véhicules de Freudiger et al.
Origine : Fichiers produits par l'(les) auteur(s)