Cheval, Vincent, Blanchet, Bruno (2013) Proving More Observational Equivalences with ProVerif. In: Basin, David and Mitchell, John C., eds. Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in Computer Science , 7796. pp. 226-246. Springer-Verlag Berlin, Roma, Italy ISBN 978-3-642-36829-5. E-ISBN 978-3-642-36830-1. (doi:10.1007/978-3-642-36830-1_12) (KAR id:46727)
PDF
Publisher pdf
Language: English |
||
Download (295kB)
Preview
|
|
|
This file may not be suitable for user of assistive technology. Request an accessible format. |
||
PDF (The long version of the paper)
Supplemental Material
Language: English |
||
Download (657kB)
Preview
|
|
|
This file may not be suitable for user of assistive technology. Request an accessible format. |
||
Official URL http://dx.doi.org/10.1007/978-3-642-36830-1_12 |
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 in- side terms, to allow ProVerif to prove the desired equivalence. These extensions have been implemented in ProVerif and allow us to au- tomatically prove anonymity in the private authentication protocol by Abadi and Fournet.
Item Type: | Conference or workshop item (Paper) |
---|---|
DOI/Identification number: | 10.1007/978-3-642-36830-1_12 |
Uncontrolled keywords: | Cryptographic protocols, Formal verification, Symbolic model, Automatic, Equivalence properties, Horn clauses |
Subjects: |
Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics |
Divisions: | Faculties > Sciences > School of Computing > Security Group |
Depositing User: | Vincent Cheval |
Date Deposited: | 16 Jan 2015 14:36 UTC |
Last Modified: | 29 May 2019 14:05 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/46727 (The current URI for this page, for reference purposes) |
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):