A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif

Vincent Cheval 1 Véronique Cortier 1 Mathieu Turuani 1
1 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : ProVerif is a popular tool for the fully automatic analysis of security protocols, offering very good support to detect flaws or prove security. One exception is the case of protocols with global states such as counters, tables, or more generally, memory cells. ProVerif fails to analyse such protocols, due to its internal abstraction. Our key idea is to devise a generic transformation of the security properties queried to ProVerif. We prove the soundness of our transformation and implement it into a front-end GSVerif. Our experiments show that our front-end (combined with ProVerif) outperforms the few existing tools, both in terms of efficiency and protocol coverage. We successfully apply our tool to a dozen of protocols of the literature, yielding the first fully automatic proof of a security API and a payment protocol of the literature.
Document type :
Reports
Complete list of metadatas

Cited literature [32 references]  Display  Hide  Download

https://hal.inria.fr/hal-01774803
Contributor : Vincent Cheval <>
Submitted on : Sunday, April 29, 2018 - 1:01:55 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Long-term archiving on : Tuesday, September 25, 2018 - 4:24:46 AM

File

CCT-CSF18-Technical Report.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01774803, version 2

Collections

Citation

Vincent Cheval, Véronique Cortier, Mathieu Turuani. A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. [Research Report] Inria Nancy - Grand Est; LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2018. ⟨hal-01774803v2⟩

Share

Metrics

Record views

189

Files downloads

254