Proving More Observational Equivalences with ProVerif

Abstract : This paper presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. ProVerif can prove observational equivalence between processes that have the same structure but differ by the messages they contain. In order to extend the class of equivalences that ProVerif handles, we extend the language of terms by defining more functions (destructors) by rewrite rules. In particular, we allow rewrite rules with inequalities as side-conditions, so that we can express tests ''if then else'' inside terms. Finally, we provide an automatic procedure that translates a process into an equivalent process that performs as many actions as possible inside terms, to allow ProVerif to prove the desired equivalence. These extensions have been implemented in ProVerif and allow us to automatically prove anonymity in the private authentication protocol by Abadi and Fournet.
Type de document :
Communication dans un congrès
David Basin and John Mitchell. POST 2013 - 2nd Conference on Principles of Security and Trust, Mar 2013, Rome, Italy. Springer, LNCS, 7796, pp.226-246, 2013, POST 2013: Principles of Security and Trust. 〈10.1007/978-3-642-36830-1_12〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00863377
Contributeur : Ben Smyth <>
Soumis le : mercredi 18 septembre 2013 - 17:37:09
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Lien texte intégral

Identifiants

Collections

Citation

Vincent Cheval, Bruno Blanchet. Proving More Observational Equivalences with ProVerif. David Basin and John Mitchell. POST 2013 - 2nd Conference on Principles of Security and Trust, Mar 2013, Rome, Italy. Springer, LNCS, 7796, pp.226-246, 2013, POST 2013: Principles of Security and Trust. 〈10.1007/978-3-642-36830-1_12〉. 〈hal-00863377〉

Partager

Métriques

Consultations de la notice

130