@inproceedings{CCT-csf18,
   author = {Cheval, Vincent and Cortier, V{\'e}ronique and Turuani, Mathieu},
   title = {A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif},
   booktitle = {{P}roceedings of the 30th {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'18)},
   year = {2018},
   editor = {Chong, Steve and Delaune, St{\'e}phanie},
   publisher = {{IEEE} Computer Society Press},
   address = {Oxford, UK},
   month = jul,
   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.},
}