by Petr Klus, Ben Smyth and Mark D. Ryan
ProSwapper is an extension to ProVerif -- the automatic cryptographic protocol verifier by Bruno Blanchet -- which extends the class of equivalences that can be automatically verified. In particular, ProSwapper is designed to consider cryptographic protocols that require barrier synchronisation to achieve security objectives. For example, privacy preserving protocols typically require the existence of at least two honest participants whom synchronise prior to performing critical actions. This particular pre-requisite can be observed in domains including electronic voting, vehicular ad-hoc networks and anonymity networks.
Equivalence in ProVerif. ProVerif focuses on equivalences P ∼ Q in which processes P and Q share the same structure and differ only in the choice of terms. Unfortunately, however, ProVerif is unsuited to analysing the privacy preserving protocols we consider here, as a simple example will demonstrate. Consider the equivalence P ∼ Q where
P = out(c,m) | out(c,n)
and
This equivalence can be written as the biprocess R = out(c,choice[m,n]) | out(c,choice[n,m]). We have P ∼ Q, but ProVerif cannot prove this result. These troublesome equivalences arise when studying privacy in application domains including electronic voting, vehicular ad-hoc networks and anonymity networks.
Modelling barriers. To model barrier synchronisation the syntax of ProVerif is extended with barriers. Barriers are written sync t and may appear before a process P, where t is an integer. Intuitively, sync t;P blocks P if there exists another process running in parallel which has not reached barrier t. For example, the process
(sync 1;out(c,k);sync 2;out(c,m)) | (sync 2;out(c,n))
can only output n after synchronisation at sync 2. It follows that the process cannot output n without having previously output k. (Note that, this is in direct contrast with the phase t command in ProVerif which would permit the output of n without having previously observed an output k.)
Formally, the number of barriers which must be reached is computed statically, in advance of execution, and thus branching behaviour may cause blocking. For example, the process
(in(c,x);if x=k then sync 1;out(c,m) else out(c,n))) | (sync 1;out(c,s))
may evolve to out(c,n) | (sync 1;out(c,s)) which can never output s because synchronisation at barrier t=1 requires two processes to synchronise.
Barriers are assumed to be ordered, that is, given sync t;P the process P is blocked if there are any barriers sync t' where t' < t. In addition, the occurrence of barriers under replication is explicitly forbidden; this restriction is made for technical convenience, although the loss of generality is minimal since such a process would deadlock. ProSwapper can compile processes containing barriers sync t to processes defined over the standard ProVerif syntax. Although our characterisation of barriers is just an encoding, we find it useful in practice.
New algorithm for analysing equivalence. Resolving the difficulties apparent in aforementioned ProVerif example is relatively straightforward. The biprocess R' = out(c,choice[m,m]) | out(c,choice[n,n]) can be used to trivially show P ∼ out(c,m) | out(c,n), and P ∼ Q follows immediately. However, this technique cannot be applied to more complicated examples in which barriers occur. For example, consider the biprocess
R = (out(c,m);sync 1;out(c,choice[m,n])) | (sync 1;out(c,choice[n,m]))
Intuitively, there is no equivalent biprocess R' for which
ProVerif can prove a result, but nevertheless, barrier synchronisation ensures
ProSwapper is explicitly designed to prove such equivalences.
ProSwapper takes as input processes defined over the ProVerif syntax with the addition of barriers and outputs a process, defined over the standard ProVerif syntax, with possible swapping strategies modelled as process macros. ProSwapper is executed in the following way:
proswapper filename
For convenience, output may be redirected to file, for example, on linux:
This file is immediately suitable for analysis using ProVerif, for example, using the command:
However, to utilise the new algorithm for analysing equivalence the file must be edited. In particular, the occurence of sync_process_0 in the process definition should be modified to sync_process_n where n is an integer and sync_process_n is defined as a process macro introduced by ProSwapper. Proving a result using Prowapper is believed to show equivalence of the original pair of processes.
ProSwapper will be publicly released shortly.
ProSwapper has been used to obtain results in the following case studies:
The ProSwapper tool is based upon the following theoretical research: