Automated reasoning for equivalences in the applied pi calculus with barriers

Résumé : 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.
Type de document :
Rapport
[Research Report] RR-8906, Inria Paris. 2016, pp.54
Liste complète des métadonnées

https://hal.inria.fr/hal-01306440
Contributeur : Bruno Blanchet <>
Soumis le : samedi 23 avril 2016 - 19:55:31
Dernière modification le : vendredi 16 septembre 2016 - 15:06:58
Document(s) archivé(s) le : dimanche 24 juillet 2016 - 10:51:51

Fichier

RR-8906.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01306440, version 1

Collections

Citation

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>

Partager

Métriques

Consultations de
la notice

243

Téléchargements du document

132