Automated Reasoning for Equivalences in the Applied Pi Calculus with Barriers

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 and Lee et al., and in the vehicular ad-hoc network by Freudiger et al.
Type de document :
Communication dans un congrès
29th IEEE Computer Security Foundations Symposium (CSF'16), Jun 2016, Lisboa, Portugal. pp.310 - 324, 2016, 〈10.1109/CSF.2016.29〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01423742
Contributeur : Bruno Blanchet <>
Soumis le : samedi 31 décembre 2016 - 12:57:53
Dernière modification le : mardi 21 novembre 2017 - 16:30:02
Document(s) archivé(s) le : samedi 1 avril 2017 - 12:04:13

Fichier

BlanchetSmythCSF16.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Bruno Blanchet, Ben Smyth. Automated Reasoning for Equivalences in the Applied Pi Calculus with Barriers. 29th IEEE Computer Security Foundations Symposium (CSF'16), Jun 2016, Lisboa, Portugal. pp.310 - 324, 2016, 〈10.1109/CSF.2016.29〉. 〈hal-01423742〉

Partager

Métriques

Consultations de la notice

149

Téléchargements de fichiers

21