Automated reasoning for equivalences in the applied pi calculus with barriers - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2016

Automated reasoning for equivalences in the applied pi calculus with barriers

Preuve automatique d'équivalences dans le pi calcul appliqué avec barrières

(1) , (2)
1
2

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.
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.
Fichier principal
Vignette du fichier
RR-8906.pdf (1.09 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01306440 , version 1 (23-04-2016)

Identifiers

  • HAL Id : hal-01306440 , version 1

Cite

Bruno Blanchet, Ben Smyth. Automated reasoning for equivalences in the applied pi calculus with barriers. [Research Report] RR-8906, Inria Paris. 2016, pp.54. ⟨hal-01306440⟩
512 View
298 Download

Share

Gmail Facebook Twitter LinkedIn More