ProVerif

ProVerif is an open source symbolic, cryptographic protocol verification tool. Security protocols are ubiquitous, and being able to prove their integrity is a necessity. ProVerif allows us to do this for a large range of protocols and properties. For example, we can prove correspondence properties (events which are temporally dependent on one another) and equivalence properties (ensuring that adversaries cannot distinguish between two distinct events).

We formulate the security protocols and properties we wish to prove are in ProVerif's own version of the applied pi-calculus. ProVerif then translates them into a set of Horn clauses and repeatedly applies saturation in order to try and verify the property. This verification problem is known to be undecidable, so while ProVerif has been proved to be sound, it is by no means complete.

While working well, ProVerif often uses up a significant amount of memory in these computations, making it hard for users to run on standard hardware. For my 3rd year dissertation at the University of Oxford, I aimed to tackle this - please feel free to download my write up from the link above.

We aimed to make use of hash consing techniques - allowing us to share structurally equal objects in memory, reducing our memory consumption. Explained in detail in the document (above), our terms are essentially split into sets called clauses. Terms are made up of a combination of function, constant and variable symbols. We changed their representation from trees to Directed Acyclic Graphs (DAGs), so that we could share common subterms. While this gives some memory compression, we can do better. We are allowed to rename variables, so long as the renaming is 1-1 with respect to each clause (this is due to the clauses actually being a conjunction of disjunctions, and the 'for all' logical operator distributing over the former but not the latter). We quickly show that different renamings give different levels of compression.

Searching for the optimal renaming, we rigorously formulate the compression problem, and then are able to successfully prove that it is NP-Hard - this is done via a neat reduction from k-CLIQUE to the decision version of the compression problem. Despite this, we wanted to try and solve it optimally, so formulated it as a Binary Linear Program. While this worked in theory, it was totally intractable. This is particularly problematic as it has been shown in previous works that the verification problem that ProVerif tackles is undecidable, hence we don't want to fool the users into thinking it hasn't terminated when in reality it is just being slow (just to check that it was really intractable, we built our own BLP solver that exploited the specific structure of our constraints).

In search of a better solution, we developed 5 approximation algorithms, increasing in complexity, that exploited the new DAG structure of the terms. These had varying degrees of success, but after some rigorous benchmarking (Chapter 4), we were able to achieve a 70,000 times lossless improvement on the memory usage. This was a huge success, and we hope to merge these new algorithms into the production version of ProVerif soon, as well as publish this work.

This project was an enormous amount of fun, and I would like to thank my tutor and supervisor Dr Vincent Cheval. Also, ProVerif is written in OCaml, so I had a really fun time wrestling with such an interesting language. Despite its steep learning curve, it really started to click for me, and has heavily influenced how I write code in other languages ever since. Please see the code and the write up linked above.