A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif
Vincent Cheval, Véronique Cortier, and Mathieu Turuani. A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18), pp. 344–358, IEEE Computer Society Press, July 2018.
doi:10.1109/CSF.2018.00032
Download
[PDF] [PDF (long version)] [HTML]
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.
BibTeX
@InProceedings{GSVerif-CSF18,
author = {Vincent Cheval and V\'eronique Cortier and Mathieu
Turuani},
title = {A little more conversation, a little less action, a
lot more satisfaction: Global states in ProVerif},
booktitle = {{P}roceedings of the 31st {IEEE} {C}omputer
{S}ecurity {F}oundations {S}ymposium ({CSF}'18)},
year = 2018,
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. \par
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. },
month = jul,
pages = {344--358},
publisher = {{IEEE} Computer Society Press},
year = 2018,
acronym = {{CSF}'18},
nmonth = 7,
={https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=8429316},
={https://hal.archives-ouvertes.fr/hal-01819366/document},
doi = {10.1109/CSF.2018.00032}
}