Formal methods have been successfully applied to security protocols, offering very good tool 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. Even the highly popular tool ProVerif fails to analyse such protocols, due to its internal abstraction.
Instead of designing a new ad-hoc procedure, 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 including adeployed voting and a payment protocol.
01/01/2022: Modified the website as the lastest version of ProVerif includes feature that does not require our modified version of GSVerif.
30/06/2020: The code of GSVerif is now available on GitLab publicly: https://gitlab.inria.fr/chevalvi/gsverif/-/tree/master
11/08/2018 : Fixing a bug in GSVerif that would generate unsound files when cells would have multiples natural number as content.
Our front-end GSVerif takes as input a Proverif file and returns a new ProVerif file on which we applied the transformation described in our research paper. Note that the official release of ProVerif does not include our new features (e.g. natural numbers and improved query verification). Therefore, to fully use GSVerif, it is recommended to also install our modified version of ProVerif. Note that GSVerif requires Ocaml 4.03 to work. It is highly recommended to install Ocaml through opam instead of apt-get (the latest version on apt-get may not be the latest release of Ocaml)
Upgrading Ocaml using OPAM
Run opam switch list
Run opam switch 4.05.0 (or more recent official release)
Follow the instructions
Installation of ProVerif
See https://bblanche.gitlabpages.inria.fr/proverif/ to retreive the latest official release.
Note that the source code is also available on Git: https://gitlab.inria.fr/bblanche/proverif
Installation of GSVerif
Inside the directory GSVerif, run ./build
The executable program gsverif has been built.
The input file of GSVerif have the same syntax as input files of ProVerif. However to help GSVerif applying our transformations, users are allowed to specify some options when declaring channel names and tables. Take for instance the file [ProVerif]toy-one-dec.pv in our example folder.
free c:channel.
free s:bitstring [private].
fun enc(bitstring,bitstring):bitstring.
reduc forall x:bitstring, y:bitstring; dec(enc(x,y),y)=x.
query attacker(s).
let A(k:bitstring) =
new n: bitstring; new k1: bitstring; new k2: bitstring;
out(c, enc((n,k1),k));
out(c, enc((n,k2),k));
out(c, enc(s,(k1,k2)));
in(c,y:bitstring);
let (=n,z:bitstring)=dec(y,k) in
out(c,z).
process
new k: bitstring;
! A(k)
This process cannot be proved by ProVerif (even with our improvements) but GSVerif is able to help ProVerif provided that the user specify on which channel our transformations must be applied. In our example, we only need to add the option precise when declaring the channel c.
free c:channel [precise].
The rest of the file stays the same. With this new file as input (see the file [GSVerif]toy-one-dec.pv in our example folder), GSVerif will automatically generate the following file output.pv (note that the name of the output can be changed with the option -o <filename>) :
free c:channel.
free s:bitstring [private].
fun enc(bitstring,bitstring):bitstring.
reduc forall x:bitstring,y:bitstring; dec(enc(x,y),y) = x.
type stamp.
event UAction_bitstring(stamp,bitstring).
query st:stamp,x:bitstring,x1:bitstring;
attacker(s) ==>
event(UAction_bitstring(st,x1)) && event(UAction_bitstring(st,x)) && x1 <> x.
process
new k:bitstring;
!
new n:bitstring; (* Application of the process A *)
new k1:bitstring;
new k2:bitstring;
out(c,enc((n,k1),k));
out(c,enc((n,k2),k));
out(c,enc(s,(k1,k2)));
in(c,y:bitstring);
new st[]:stamp;
event UAction_bitstring(st,y);
let (= n,z:bitstring) = dec(y,k) in
out(c,z);
0
This new file output.pv can be directly given and proved by ProVerif (run proverif output.pv).
Note that if the option precise was not introduced in the original file, output.pv would be similar to the ProVerif file. In fact a ProVerif file can be provided to GSVerif without any modification. Moreover, note that not all the features of ProVerif are handled by GSVerif. For instance, equivalence properties, strong secrecy, phases, synchronisation, process macros with fail, etc are not handle by GSVerif.
Options available in GSVerif
Channels declared at top level can take the options precise, cell, counter, uniqueAction and uniqueComm. Note that the option precise will automatically search for the best option. As such, precise cannot be used at the same time as other options. Note that the options counter, uniqueAction and uniqueComm cannot be declared without the option private. Some examples:
free c:channel [precise].
free c:channel [private,precise].
free c:channel [private,uniqueAction,cell].
free c:channel [private, cell,counter].
Similarly, channels declared inside processes can have the same options as channels declared at top level. Note that the option private is not required as these names are by default private. Some examples:
in(d,x:bitstring); new c:channel [precise]; out(d,u).
in(d,x:bitstring); new c:channel [uniqueAction,cell]; out(d,u).
Tables can be declared with the options precise, lockedInsert, lockedRound and value.
table tbl(bitstring,bitstring) [value].
V. Cheval, V. Cortier and M. Turuani. A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. In Proceedings of the 31th IEEE Computer Security Foundations Symposium (CSF'18), IEEE Computer Society Press, 2018. [PDF]