# Automatic verification of privacy properties in the applied pi calculus [^2] Stéphanie Delaune, Mark Ryan, Ben Smyth # Introduction Security protocols are small distributed programs that aim to provide some security related objective over a public communications network like the Internet. Considering the increasing size of networks and their dependence on cryptographic protocols, a high level of assurance is needed in the correctness of such protocols. It is difficult to ascertain whether or not a cryptographic protocol satisfies its security requirements. Numerous protocols have appeared in literature and have subsequently been found to be flawed (Lowe 1995; Mukhamedov and Ryan 2007; Chadha, Kremer, and Scedrov 2004). Typically, cryptographic protocols are expected to achieve their objectives in the presence of an attacker that is assumed to have full control of the network (sometimes called the Dolev-Yao attacker). He can eavesdrop, replay, inject and block messages. The attacker can also modify them by performing cryptographic operations when in possession of the required keys. Furthermore the attacker may be in control of one or more of the protocol’s participants. With no more than the abilities listed, and irrespective of the underlying cryptographic algorithms, numerous protocols have been found to be vulnerable to attack. Formal verification of cryptographic protocols is therefore required to ensure that cryptographic protocols can be deployed without the risk of damage. Traditionally cryptographic protocols have been required to satisfy secrecy and authentication properties (Clark and Jacob 1997). These requirements have been successfully verified by modelling them as reachability problems. Current research into applications such as electronic voting, fair exchange and trusted computing has resulted in a plethora of new requirements which protocols must satisfy (e.g. (Hirt and Sako 2000; Brickell, Camenisch, and Chen 2004)). Some of these properties cannot easily be expressed using traditional reachability techniques but can be written as equivalences. For example, the privacy, receipt-freeness and coercion-resistance properties of electronic voting protocols can be expressed using equivalences (see (Kremer and Ryan 2005; Stephanie Delaune, Kremer, and Ryan 2006)). We focus on proving equivalences of the kind ${P \sim Q}$, where the processes $P$ and $Q$ have the same structure and differ only in the choice of terms. For example, the secret ballot (privacy) property of an electronic voting protocol can be expressed as
$P(skva,v_1) \mid P(skvb,v_2) \;\sim\; P(skva,v_2) \mid P(skvb,v_1)$
where $P$ is the voter process with two parameters: its secret key ($skva$, $skvb$) and the candidate for whom he wish to cast their vote (here $v_1$, $v_2$). Historically many applications of equivalences to prove security requirements of cryptographic protocols have relied upon hand written proofs (Kremer and Ryan 2005; Stephanie Delaune, Kremer, and Ryan 2006). Such proofs are time consuming and error prone. Accordingly, we direct our attention to automated techniques. The calculus developed by Blanchet *et al.* makes some progress in this direction (Blanchet, Abadi, and Fournet 2008). However, the method developed for proving observational equivalence is not complete and is unable to prove certain interesting equivalences. We build upon (Blanchet, Abadi, and Fournet 2008) to provide reasoning about further equivalences (see Section 2). We also extend the syntax to allow the modelling of a new class of processes which require global synchronisation. Finally we develop an algorithm to enable automated reasoning about security requirements. The focus of our work is to model the privacy properties increasingly found in cryptographic protocols (Section 3). We demonstrate the practical application of our contribution with case studies (Sections 4 and 5). Using our approach we provide the first automated proof that the electronic voting protocol due to Fujioka, Okamoto & Ohta (FOO) (Fujioka, Okamoto, and Ohta 1993) satisfies privacy. As a second case study we provide a formal methods proof that the Direct Anonymous Attestation (DAA) (Brickell, Camenisch, and Chen 2004) protocol also satisfies privacy (the DAA authors provided a provable security proof). An extended version of this paper (S. Delaune, Ryan, and Smyth 2008) and our ProVerif source code are available at http://www.cs.bham.ac.uk/\char126bas/. Kremer & Ryan (Kremer and Ryan 2005) have previously demonstrated the electronic voting protocol FOO satisfies fairness, eligibility and privacy. The first two properties were verified automatically using ProVerif, and the third relied on a hand proof. Backes *et al.* (Backes, Maffei, and Unruh 2008) model a variant of DAA and provide some proofs. We observe that their model is not accurate with regards to DAA due to some subtleties in their formalisation. Nevertheless their idea of modelling synchronisation by private channel communication influenced the design of our translator. # Calculus of ProVerif The process calculi of Blanchet *et al.* (Blanchet, Abadi, and Fournet 2008), used by the tool ProVerif, is a variant of the applied pi calculus (Abadi and Fournet 2001), a process calculi for formally modelling concurrent systems and their interactions. In this paper we use the phrase *calculus of ProVerif* to mean the calculus defined in (Blanchet, Abadi, and Fournet 2008), and *ProVerif software tool* to refer to the software tool developed in accompaniment of (Blanchet, Abadi, and Fournet 2008). ## Syntax and informal semantics The calculus assumes an infinite set of *names* and an infinite set of *variables*. It also assumes a *signature* $\Sigma$, i.e. a finite set of *function symbols* each with an associated arity. A function symbol with arity $0$ is also called a *constant*. We distinguish two categories of function symbols: *constructors* $f$ and *destructors* $g$ and we use $h$ to range over both. We use standard notation for function application, i.e. ${h(M_1,\ldots,M_n)}$. Destructors are partial, non-deterministic operations, that processes can apply to terms. They represent primitives that can visibly succeed or fail, while constructors and the associated equational theory apply to primitives that always succeed but may return “junk". The grammar for terms/term evaluations is given below. $$\begin{array}{llllllll} M,N &::= &\;& \mbox{term} &D & ::=& \; & \mbox{term evaluation}\\ &a,b,c && \mbox{name} & &M && \mbox{term}\\ &x,y,z && \mbox{variable} & &\textrm{choice}[D,D'] && \mbox{choice term eval.}\\ &\textrm{choice}[M,M']&&\mbox{choice term} \;\;\;\;\;&& h(D_1, \ldots, D_n) && \mbox{function eval.}\\ & f(M_1,\ldots,M_n) && \mbox{constructor} & \end{array}$$ We equip the signature $\Sigma$ with an *equational theory*, say $\mathsf{E}$, i.e. a finite set of equations of the form $M_i = N_i$, where $M_i$ and $N_i$ are terms without names. The equational theory is then obtained from this set of equations by reflexive, symmetric and transitive closure, closure by substitution of terms for variables and closure by context application. We write $M=_\mathsf{E}N$ (resp. $M \not=_\mathsf{E}N$) for equality (resp. inequality) modulo $\mathsf{E}$. Processes are built up in a similar way to processes in the pi calculus, except that messages can contain terms/term evaluations (rather than just names). In the grammar described below, $M$ and $N$ are terms, $D$ is a term evaluation, $a$ is a name, $x$ a variable and $t$ an integer.
XX̄$\textrm{if } M=N \textrm{ then } P \textrm{ else } Q$X̄XX̄ $P,Q,R ::=$ processes $null$ null process $P \mid Q$ parallel composition $!P$ replication $\textrm{new }a;P$ name restriction $\textrm{let } x=D \textrm{ in } P \textrm{ else } Q$ term evaluation $\textrm{in}(M,x);P$ message input $\textrm{out}(M,N);P$ message output $\textrm{phase }t;P$ weak phase
We note that the ProVerif software tool allows the definition of a single main process which in turn may refer to subprocesss of the form “$\textrm{let } P = Q$." The tool also permits the use of comments in the form $\emph{(* comment *)}$. The choice operator allows us to model a pair of processes which have the same structure and differ only in the choice of terms and terms evaluations. We call such a pair of processes a *biprocess*. Given a biprocess $P$, we define two processes $\mathsf{fst}({P})$ and $\mathsf{snd}({P})$ as follows: $\mathsf{fst}({P})$ is obtained by replacing all occurrences of $\textrm{choice}[M,M']$ with $M$ and $\textrm{choice}[D,D']$ with $D$ in $P$. Similarly, $\mathsf{snd}({P})$ is obtained by replacing $\textrm{choice}[M,M']$ with $M'$ and $\textrm{choice}[D,D']$ with $D'$ in $P$. We define $\mathsf{fst}({D})$, $\mathsf{fst}({M})$, $\mathsf{snd}({D})$ and $\mathsf{snd}({M})$ similarly. As usual, names and variables have scopes, which are delimited by restrictions and by inputs. We write $\mathit{fv}({P})$, $\mathit{bv}({P})$ (resp. $\mathit{fn}({P})$ and $\mathit{bn}({P})$) for the sets of free and bound variables (resp. names) in $P$. A process is *closed* if it has no free variables (but it may contain free names). A *context* $C[\_]$ is a process with a hole. We obtain $C[P]$ as the result of filling $C[\_]$’s hole with $P$. An *evaluation context* $C$ is a closed context built from $[\_]$, ${C \mid P}$, ${P \mid C}$ and ${\textrm{new }a;C}$. We sometimes refer to contexts without $\textrm{choice}$ as *plain contexts*. The major difference between the syntax of the applied pi calculus and the calculus of ProVerif, is the introduction of the $\textrm{choice}$ operator. In addition there are some minor changes. For instance, communication is permitted on arbitrary terms, not just names. Function symbols are supplemented with destructors. Active substitutions are removed in favour of term evaluations. The syntax does not include the conditional “$\textrm{if } M=N \textrm{ then } P \textrm{ else } Q$”, which can be defined as “$\textrm{let } x=equals(M,N) \textrm{ in } P \textrm{ else } Q$” where ${x \not\in \mathit{fv}({P})}$ and $equals$ is a destructor with the equation $equals(x,x) = x$. We omit “$\textrm{else }Q$” when the process $Q$ is $null$. Finally the calculus of ProVerif does not rely on a sort system. We believe that processes written in the calculus of ProVerif, can be mapped to semantically equivalent processes in the applied pi calculus and vice-versa, although proving this remains an open problem. This can easily be extended to biprocesses. ## Operational semantics The operational semantics of processes in the calculus of ProVerif, are defined by three relations, namely *term evaluation* $\Downarrow$, *structural equivalence* $\equiv$ and *reduction* $\xrightarrow{}$. Structural equivalence and reductions are only defined on closed processes. We write $\xrightarrow{}^*$ for the reflexive and transitive closure of $\xrightarrow{}$, and $\xrightarrow{}^*\equiv$ for its union with $\equiv$. The operational semantics for the calculus of ProVerif differ in minor ways from the semantics of the applied pi calculus. *Structural equivalence* is the smallest equivalence relation on processes that is closed under application of evaluation contexts and some other standard rules such as associativity and commutativity of the parallel operator. *Reduction* is the smallest relation on biprocesses closed under structural equivalence and application of evaluation contexts such that $$\begin{minipage}{\linewidth} \begin{tabbing} {\sc Red Fun} 2XX\=X\=XXXXXXXXXXXXXX\=RED FUN 2XX\=\kill %Set tab sizes % {\sc Red I/O} \> $\textrm{out}(N,M);Q \mid \textrm{in}(N',x);P \xrightarrow{}Q \mid P\{{}^{M}/{}_{x}\}$ \\ \> \> \hspace{2.5cm}if $\mathsf{fst}({N}) = \mathsf{fst}({N'})$ and $\mathsf{snd}({N}) = \mathsf{snd}({N'})$ \\ {\sc Red Fun 1} \> $\textrm{let } x=D \textrm{ in } P \textrm{ else } Q \xrightarrow{}P\{{}^{\textrm{choice}[M_1,M_2]}/{}_{x}\}$ \\ \>\> \hspace{3.8cm} if $\mathsf{fst}({D}) \Downarrow M_1$ and $\mathsf{snd}({D}) \Downarrow M_2$ \\ {\sc Red Fun 2} \> $\textrm{let } x=D \textrm{ in } P \textrm{ else } Q \xrightarrow{}Q$ \\ \>\> \hspace{2.cm} if there is no $M_1$ such that $\mathsf{fst}({D}) \Downarrow M_1$ and \\ \>\> \hspace{2.9cm} there is no $M_2$ such that $\mathsf{snd}({D}) \Downarrow M_2$ \\ {\sc Red Repl} \> $!P \xrightarrow{}P \mid !P$ %Rules for processes without diff % RED I/O \> $\Out[N]{M}.Q|\In[N']{x}.P \reduc Q|P\activesubst{M}{x}$ \\ % \>\> if $\Sigma \vdash N = N'$ \\ %\\ % RED FUN 1 \> $\Letinelse{x}{D}{P}{Q} \reduc P\activesubst{M}{x}$ \\ % \>\> if $D \Downarrow M$ \\ % RED FUN 2 \> $\Letinelse{x}{D}{P}{Q} \reduc Q$ \\ % \>\> if there is no $M$ such that $D \Downarrow M$ \\ %\\ \end{tabbing} %\caption{Reductions rules} \end{minipage}$$ ## Extension to processes with weak phases Many protocols can be broken into phases, and their security properties can be formulated in terms of these phases. Typically, for instance, if a protocol discloses a session key after the conclusion of a session, then the secrecy of the data exchanged during the session may be compromised but not its authenticity. To enable modelling of protocols with several phases the calculus of ProVerif is extended (Blanchet, Abadi, and Fournet 2008). The syntax of processes is supplemented with a phase prefix “$\textrm{phase }t;P$”, where $t$ is a non-negative integer. Intuitively, $t$ represents a global clock, and the process “$\textrm{phase }t;P$” is active only during phase $t$. However, it is possible that *not* all instructions of a particular phase are executed prior to a phase transition. Moreover, parallel processes may only communicate if they are under the same phase.
Let $P = \textrm{phase }1;\textrm{out}(c,a) \mid \textrm{phase }2;\textrm{out}(c,b)$. The process $P$ can output $b$ without having first output $a$.
The semantics of processes are extended to deal with weak phases (see (Blanchet, Abadi, and Fournet 2008)). ## Observational equivalence The notion of observational equivalence was introduced by Abadi & Fournet (Abadi and Fournet 2001), subsequently Blanchet, Abadi & Fournet (Blanchet, Abadi, and Fournet 2008) defined strong observational equivalence. This paper will use strong observational equivalence, henceforth we shall use observational equivalence to mean strong observational equivalence. We first recall the standard definition of observational equivalence. We write $P \downarrow_M$ when $P$ emits a message on the channel $M$, that is, when $P \equiv C[\textrm{out}(M',N);R]$ for some evaluation context $C[\_]$ that does not bind $\mathit{fn}({M})$ and $M =_\mathsf{E}M'$.
*Observational equivalence* $\sim$ is the largest symmetric relation $\mathcal{R}$ on closed processes such that $P \mathrel{\mathcal{R}} Q$ implies: 1. if $P \downarrow_M$ then $Q \downarrow_M$; 2. if $P \rightarrow P'$ then there exists $Q'$ such that $Q \rightarrow Q'$ and $P' \mathrel{\mathcal{R}} Q'$; 3. $C[P] \mathrel{\mathcal{R}} C[Q]$ for all evaluation contexts $C$.
Intuitively, a context may represent an attacker, and two processes are observationally equivalent if they cannot be distinguished by any attacker. Given a biprocess $P$, we say that $P$ satisfies observational equivalence when we have that ${\mathsf{fst}({P})\sim\mathsf{snd}({P})}$. A reduction $P \xrightarrow{}Q$ for a biprocess $P$ implies the corresponding processes have reductions $\mathsf{fst}({P}) \xrightarrow{}\mathsf{fst}({Q})$ and $\mathsf{snd}({P}) \xrightarrow{} \mathsf{snd}({Q})$. However, reductions in $\mathsf{fst}({P})$ and $\mathsf{snd}({P})$ do not necessarily correspond to any biprocess reduction. When such a corresponding reduction does exist the processes $\mathsf{fst}({P})$ and $\mathsf{snd}({P})$ satisfy uniformity under reduction (UUR):
A biprocess $P$ satisfies *uniformity under reduction* if: 1. $\mathsf{fst}({P}) \xrightarrow{}Q_1$ implies that $P \xrightarrow{}Q$ for some biprocess $Q$ with $\mathsf{fst}({Q}) \equiv Q_1$, and symmetrically for $\mathsf{snd}({P}) \xrightarrow{}Q_2$; 2. for all plain evaluation contexts $C$, for all biprocess $Q$, $C[P] \rightarrow Q$ implies that $Q$ satisfies UUR.
Blanchet *et al.* (Blanchet, Abadi, and Fournet 2008) have shown that if a biprocess $P$ satisfies uniformity under reductions then $P$ satisfies observational equivalence. The ProVerif  software automatically verifies whether its input satisfies uniformity under reduction and thus enables us to prove observational equivalence in some cases. ## Limitations of the calculus There are trivial equivalences (see Example [ex:limit] described below) which the calculus of ProVerif is unable to prove since the definition of observational equivalence by uniformity under reductions is too strong. We overcome this problem with *data swapping*.
The equivalence $\textrm{out}(c,a) \mid \textrm{out}(c,b) \sim \textrm{out}(c,b) \mid \textrm{out}(c,a)$ holds trivially since the processes are in fact structurally equivalent. But the corresponding biprocess $\textrm{out}(c,\textrm{choice}[a,b]) \mid \textrm{out}(c,\textrm{choice}[b,a])$ does not satisfy uniformity under reductions and therefore the equivalence cannot be proved by ProVerif.
Moreover, the phase semantics introduced by the calculus of ProVerif (Blanchet, Abadi, and Fournet 2008) are insufficient to model protocols which require synchronisation, as the phase semantics do not enforce that all instances of a phase must be completed prior to phase progression. We solve this problem with the introduction of *strong phases*. Both of these problems are encountered when modelling cryptographic protocols from literature. As case studies we demonstrate the suitability of our approach by modelling the privacy properties of the electronic voting protocol FOO (Fujioka, Okamoto, and Ohta 1993) and Direct Anonymous Attestation (DAA) (Brickell, Camenisch, and Chen 2004). # Extending the calculus To overcome the limitations stated in the previous section, we extend the calculus with strong phases and data swapping. ## Extension to processes with strong phases Similarly to weak phases the syntax of processes is supplemented with a strong phase prefix “$\textrm{strong phase }t;P$", where $t$ is a non-negative integer. A strong phase represents a global synchronisation and $t$ represents the global clock. The process $\textrm{strong phase }t;P$ is active only during strong phase $t$ and a strong phase progression may only occur once all the instructions under the previous phase have been executed.
Consider our earlier example (Example [ex:weakstage]) with the use of strong phase. Now, the process $$\textrm{strong phase }1;\textrm{out}(c,a) \mid \textrm{strong phase }2;\textrm{out}(c,b)$$ cannot output $b$ without having previously output $a$.
## Extension to processes with data swapping Let us first consider the background to our approach. Referring back to Example [ex:limit] we recall the biprocess $Q = \textrm{out}(c,\textrm{choice}[a,b]) \mid \textrm{out}(c,\textrm{choice}[b,a])$ which does not satisfy UUR. We note that ${\mathsf{fst}({Q}) = \textrm{out}(c,a) \mid \textrm{out}(c,b)}$ and ${\mathsf{snd}({Q}) = \textrm{out}(c,b) \mid \textrm{out}(c,a)}$. Since $\textrm{out}(c,b) \mid \textrm{out}(c,a) \equiv \textrm{out}(c,a) \mid \textrm{out}(c,b)$ it seems reasonable to rewrite $\mathsf{snd}({Q})$ as $\textrm{out}(c,a) \mid \textrm{out}(c,b)$, enabling us to write $Q$ as ${\textrm{out}(c,\textrm{choice}[a,a]) \mid \textrm{out}(c,\textrm{choice}[b,b])}$ which is semantically equivalent to $\textrm{out}(c,a) \mid \textrm{out}(c,b)$. Our new biprocess satisfies uniformity under reduction, and thus observational equivalence. It therefore seems possible (under certain circumstances) to *swap* values from the left to the right side of the parallel operator. Sometimes the swap is not done initially but instead immediately after a strong phase. To specify data swapping we introduce the special comment $\emph{(**swap*)}$ in process descriptions, which can be seen as a *proof hint*. Returning to our example, we would rewrite $Q$ as $$\begin{array}{rcl} Q' &\;=\;& \emph{(**swap*)}\;\textrm{out}(c,\textrm{choice}[a,b]) \mid \emph{(**swap*)}\;\textrm{out}(c,\textrm{choice}[b,a]) \\ &=& \textrm{out}(c,\textrm{choice}[a,a]) \mid \textrm{out}(c,\textrm{choice}[b,b]). \end{array}$$ ## Automated reasoning with ProVerif To allow automated reasoning we describe a translator which accepts as input processes written in our extended language. It will also include a single main process and subprocesses of the form “$\textrm{let } P = Q$”, subject to the following restrictions. 1. The commands $\textrm{strong phase }t;$ and $\emph{(**swap*)}$ can only appear in a single subprocess defined using the let keyword (not in the main process); 2. The subprocess defined using the let keyword that contain strong phases and data swapping must be instantiated precisely twice in the main process. Moreover, it must be of the form $\textrm{let } P = \alpha$, where $\alpha$ is a process that is sequential until its last strong phase, at which point it is an arbitrary process. Formally $\alpha$ is given by the grammar below: $$\alpha := R \big| \textrm{new }a;\alpha \big| \textrm{in}(M,x);\alpha \big| \textrm{out}(M,N);\alpha \big| \textrm{let } x=D \textrm{ in }\alpha \big| \textrm{strong phase }t;\alpha$$ where $R$ is an arbitrary processes without data swapping and strong phases; 3. We further require that $\emph{(**swap*)}$ may only occur at the start of a subprocess definition or immediately after a strong phase. The translator outputs processes in the standard language of ProVerif, which can be automatically reasoned about by the software tool. The pseudocode of our algorithm is presented in Figure 1. Step one of our translator makes the necessary modifications to subprocesses. It defines each strong phase as an individual subprocess. Step two handles the main process which combines the subprocesses defined in step one in such a way that preserves notion of strong phases. The other parts of the translator’s input are copied to the output verbatim. We demonstrate its application with several toy examples (see Section 3.4) and two case studies (see Sections 4 & 5).
Translator algorithm
## Examples
We begin by returning to our trivial observational equivalence: $$\textrm{out}(c,a) \mid \textrm{out}(c,b) \sim \textrm{out}(c,b) \mid \textrm{out}(c,a).$$ As the definition of observational equivalence by UUR is too strong, the calculus, and therefore the software tool, are unable to reason about such an equivalence. Using our data swapping syntax, the biprocess encoding the previous equivalence is given below. ``` let P = (**swap*) out(c,x). process let x = choice[a,b] in P|let x = choice[b,a] in P ``` Our translator gives us the following biprocess, which ProVerif can successfully prove. ``` let P = out(c,x). process let x = choice[choice[a,b],choice[b,a]] in P| let x = choice[choice[b,a],choice[a,b]] in P ```
We consider the observational equivalence shown below: $$\begin{gathered} \textrm{out}(c,a);\textrm{strong phase }1;\textrm{out}(c,d) \mid \textrm{out}(c,b);\textrm{strong phase }1;null\\ \qquad \sim \quad \textrm{out}(c,a);\textrm{strong phase }1;null\mid \textrm{out}(c,b);\textrm{strong phase }1;\textrm{out}(c,d) \end{gathered}$$ The pair of processes are both able to output $a$ and $b$. We then have a synchronisation and obtain the process $\textrm{out}(c,d) \mid null\sim null \mid \textrm{out}(c,d)$. To allow ProVerif to prove such an equivalence we provide our translator with the following input: ``` let P =out(c,x);strong phase 1;(**swap*)if y=ok then out(c,d). process let x = a in let y = choice[ok,ko] in P| let x = b in let y = choice[ko,ok] in P ``` Our translator produces the biprocess described below. ``` let P1 = out(c,x);out(pc,y). let P2 = if y = ok then out(c,c). process new pc0;new pc1;( let x = a in let y = choice[ok,ko] in let pc = pc0 in P1| let x = b in let y = choice[ko,ok] in let pc = pc1 in P1| in(pc0,y0);in(pc1,y1);( let y = choice[y0,y1] in P2| let y = choice[y1,y0] in P2)) ```
As our final example we consider the following equivalence: $$\begin{array}{ll} & \textrm{out}(c,a_1);\textrm{strong phase }1;\textrm{out}(c,a_2) \mid \textrm{out}(c,b_1);\textrm{strong phase }1;\textrm{out}(c,b_2) \\ \sim \;\; & \textrm{out}(c,a_1);\textrm{strong phase }1;\textrm{out}(c,b_2) \mid \textrm{out}(c,b_1);\textrm{strong phase }1;\textrm{out}(c,a_2) \end{array}$$ This is similar to Example [ex:second] with two outputs after the strong phase. Again, thanks to our translator, we are able to conclude on such an example. We recall Example [ex:third]. Our aim is to provide a proof of the following equivalence. $$\begin{array}{ll} & \textrm{out}(c,a_1);\textrm{strong phase }1;\textrm{out}(c,a_2) \mid \textrm{out}(c,b_1);\textrm{strong phase }1;\textrm{out}(c,b_2) \\ \sim \;\; & \textrm{out}(c,a_1);\textrm{strong phase }1;\textrm{out}(c,b_2) \mid \textrm{out}(c,b_1);\textrm{strong phase }1;\textrm{out}(c,a_2) \end{array}$$ The input to our translator is shown below: ``` let P = out(c,x);strong phase 1;(**swap*)out(c,z). process let (x,z) = (a1,choice[a2,b2]) in P| let (x,z) = (b1,choice[b2,a2]) in P ``` Our translator produces the following description. ``` let P1 = out(c,x);out(pc,z). let P2 = out(c,z). process new pc1;new pc2;( let (x,z) = (a1,choice[a2,b2]) in let pc = pc1 in P1| let (x,z) = (b1,choice[b2,a2]) in let pc = pc2 in P1| in(pc1,z1);in(pc2,z2);( let z = choice[z1,z2] in P2| let z = choice[z2,z1] in P2)) ``` ProVerif is able to successfully prove equivalence.
# E-voting protocol due to Fujioka *et al.* In this section, we study the privacy property of the e-voting protocol due to Fujioka *et al.* (Fujioka, Okamoto, and Ohta 1993). In (Kremer and Ryan 2005), it is shown that this protocol provides fairness, eligibility and privacy. However, the proof of privacy given in (Kremer and Ryan 2005) is manual: ProVerif is unable to prove it directly. ## Description The protocol involves voters, an administrator and a collector. The administrator is responsible for verifying that only eligible voters can cast votes and the collector handles the collecting and publishing of votes. The protocol requires three strong phases. In the first phase, the voter gets a signature on a commitment to his vote from the administrator, i.e. $m = sign(blind(commit(v,k),r),ska)$ where $k$ is a random key, $r$ is a blinding factor and $ska$ is the private key of the administrator. At the end of this first phase, the voter unblinds $m$ and obtains $y = sign(commit(v,k),ska)$, i.e. the signature of his commitment. The second phase of the protocol is the actual voting phase. The voter sends $y$ to the collector who checks correctness of the signature and, if the test succeeds, enters $(\ell,x,y)$ onto a list as an $\ell$-th item. The last phase of the voting protocol starts, once the collector decides that he received all votes, e.g. after a fixed deadline. In this phase the voters reveal the random key $k$ which allows the collector to open the votes and publish them. The voter verifies that his commitment is in the list and sends $\ell, r$ to the collector. Hence, the collector opens the ballots. ## Modelling privacy in applied pi Privacy properties have been successfully studied using equivalences. In the context of voting protocols, the definition of privacy is rather subtle. We recall the definition of privacy for electronic voting protocols given in (Kremer and Ryan 2005). A voting protocol guarantees ballot secrecy (privacy) whenever a process where Alice votes for candidate $v_1$ and Bob votes for candidate $v_2$ is observationally equivalent to a process where their votes are swapped, i.e. Alice votes $v_2$ and Bob votes $v_1$. We denote their secret keys $skva$ and $skvb$ respectively. In (Kremer and Ryan 2005), they rely on hand proof techniques to show privacy on FOO. Our modelling of FOO in the applied pi is similar to the one given in (Stéphanie Delaune, Kremer, and Ryan 2008). The underlying equational theory is the same as in (Kremer and Ryan 2005). The main process given in Process [pro:foo] models the environment and specifies how the other processes are combined. To establish privacy, we do not require that the authorities are honest, so we do not need to model them and we only consider two voter processes in parallel. First, fresh private keys for the voters and the administrator are generated. The corresponding public keys are then made available to the attacker. We also output the secret key of the administrator. This allows the environment to simulate the administrator (even a corrupted one) and hence we show that the privacy property holds even in the presence of a corrupt administrator. ``` let V = new k;new r; let x = commit(v,k) in out(c,(pk(skv),sign(blind(x,r),skv))); in(c,m2); let y = unblind(m2,r) in if checksign(y,pka) = x then strong phase 1; (**swap*) out(c,y); strong phase 2; in(c,(l,yprime)); if yprime = y then out(c,(l,k)). process new ska;new skva;new skvb; let pka = pk(ska) in out(c,(ska,pka,pk(skva),pk(skvb)));( (let (skv,v) = (skva,choice[v1,v2]) in V)| (let (skv,v) = (skvb,choice[v2,v1]) in V)) ``` The process V given in Process [pro:foo] models the role of a voter. The specification follows directly from our informal description. Note that we use the strong phase command to enforce the synchronisation of the voter processes. As mentioned initially in (Kremer and Ryan 2005), the separation of the protocol into strong phases is crucial for privacy to hold. We also provide a data swapping hint to allow our translator to produce an output suitable for automatic verification using ProVerif.   ## Analysis We use our translator to remove all instances of strong phases and handle data swapping. Our translator produces Process [pro:foo2], which is suitable for automatic verification using ProVerif. Hence, using our approach, we provide the first automatic and complete proof that this protocol satisfies privacy. ``` let V1 = new k;new r; let x = commit(v,k) in out(c,(pk(skv),sign(blind(x,r),skv))); in(c,m2); let y = unblind(m2,r) in if checksign(y,pka) = x then out(pc,(y,k)). let V2 = out(c,y); out(pc,(y,k)). let V3 = in(c,(l,yprime)); if yprime = y then out(c,(l,k)). process new ska;new skva;new skvb; let pka = pk(ska) in out(c,(ska,pka,pk(skva),pk(skvb))); new pc1;new pc2;new pc3;new pc4;( (let (skv,v)=(skva,choice[v1,v2]) in let pc=pc1 in V1)| (let (skv,v)=(skvb,choice[v2,v1]) in let pc=pc2 in V1)| (in(pc1,(y1,k1));in(pc2,(y2,k2));(*strong phase 1*)(*swap*)( (let (y,k)=choice[(y1,k1),(y2,k2)] in let pc=pc3 in V2)| (let (y,k)=choice[(y2,k2),(y1,k1)] in let pc=pc4 in V2)))| (in(pc3,(y3,k3));in(pc4,(y4,k4));(*strong phase 2*)( (let (y,k)=(y3,k3) in V3)| (let (y,k)=(y4,k4) in V3)))) ``` # Direct Anonymous Attestation (DAA) The Direct Anonymous Attestation (DAA) scheme provides a means for remotely authenticating a trusted platform whilst preserving the user’s privacy (Brickell, Camenisch, and Chen 2004). In (Smyth, Ryan, and Chen 2007), two of the authors have shown that corrupt administrators are able to violate the privacy of the host. Using our extended calculus we are now able to provide a formal and automatic proof that the rectified protocol proposed in (Smyth, Ryan, and Chen 2007) satisfies its privacy requirements. We start with a short description of the protocol (for a more complete description, see (Brickell, Camenisch, and Chen 2004; Smyth, Ryan, and Chen 2007)). ## Description The protocol can be seen as a group signature scheme without the ability to revoke anonymity and an additional mechanism to detect rogue members. In broad terms the *host* contacts an *issuer* and requests membership to a group. If the issuer wishes to accept the request, it grants the host/TPM an *attestation identity credential*. The host is now able to anonymously authenticate itself as a group member to a *verifier* with respect its credential. The protocol is initiated when a host wishes to obtain a credential. This is known as the join protocol. The TPM creates a secret $f$ value and a blinding factor $v'$, where $f = hash(hash(\texttt{DAASeed}\|hash(PK'_I))\|\texttt{cnt}\|0)$. The value $\texttt{DAASeed}$ is a secret known only to the TPM, $\texttt{cnt}$ is a counter used by the TPM to keep track of how many times the Join protocol has been run and $PK'_I$ is the long term public key of the issuer. The inclusion of $PK'_I$ prevents cross issuer linkability (Smyth, Ryan, and Chen 2007). The TPM then constructs the blind message $U := blind(f,v')$ and $N_I := \zeta_I^f$, where $\zeta_I := hash(0 \|bsn_I)$ and $bsn_I$ is the basename of the issuer (see (Smyth, Ryan, and Chen 2007) for further discussion on DAA basenames). The $U$ and $N_I$ values are submitted to the issuer $I$. The issuer creates a random nonce value $n_e$, encrypts it with the public key $PK_{EK}$ of the host’s TPM and returns the encrypted value. The TPM decrypts the message, revealing $n_e$, and returns $hash(U \| n_e)$. The issuer confirms that the hash is correctly formed. The issuer generates a nonce $n_i$ and sends it to the host. The host/TPM constructs a signature proof of knowledge that the messages $U$ and $N_I$ are correctly formed. The issuer verifies the proof and generates a blind signature on the message $U$. It returns the signature along with a proof that a covert channel has not been used. The host verifies the signature and proof and the TPM unblinds the signature revealing a secret credential $v$ (the signed $f$). Once the host has obtained an anonymous attestation credential from the issuer it is able to produce a signature proof of knowledge of attestation on a message $m$. This is known as the sign/verify protocol. The verifier sends nonce $n_v$ to the host. The host/TPM produce a signature proof of knowledge of attestation on the message $(n_t\|n_v\|b\|m)$, where $n_t$ is a nonce defined by the TPM and $b$ is a parameter. In addition the host computes $N_V := \zeta^f$, where $\zeta := hash(1 \| bsn_V)$ and $bsn_V$ is the basename of the verifier. Intuitively if a verifier is presented with such a proof it is convinced that it is communicating with a trusted platform and the message is genuine.   ## Modelling privacy in applied pi The DAA protocol satisfies privacy whenever a process where Alice interacts with the verifier is observationally equivalent to when Bob interacts with the verifier. For privacy we require that both Alice and Bob have completed the join protocol. The DAA protocol makes extensive use of signature proofs of knowledge (SPK) to prove knowledge of and relations among discrete logarithms. We will discuss our formalism with an example. The signature proof of knowledge $\textrm{SPK}\{(\alpha,\beta): x = g^\alpha \wedge y = h^\beta\}(m)$ denotes a signature proof of knowledge on the message $m$ that $x,y$ were constructed correctly. This leads us to define function `spk/3` to construct an SPK. The first argument contains a tuple of secret values known to the prover $\alpha,\beta$. The second argument consists of a tuple of the values on which the prover is claiming to have constructed correctly $x,y$, such that $x = g^\alpha$ and $y = h^\beta$. Finally the third argument is the message $m$ on which the prover produces a signature on. Verifying the correctness of a SPK is specific to its construction, thus we must require a function `checkspk` for each SPK that the protocol uses. To verify the SPK produced in the aforementioned example the verifier must be in possession of the SPK itself and $x,y,g,h,m$. We define the equation: $checkspk(spk((\alpha,\beta),(g^\alpha,h^\beta),m),g^\alpha,h^\beta,g,h,m) = ok.$ A verifier can now check a SPK using an `if` statement. As in FOO, the main process (see (S. Delaune, Ryan, and Smyth 2008)) models the environment and specifies how the other processes are combined. First, fresh secret keys for the TPMs, the issuer and the verifier are generated using the restriction operator. We also generate two `DAASeed` values. The public keys are then sent on a public channel, i.e. they are made available to the intruder. We also output the secret key of the verifier and issuer since the privacy property should be preserved even if they are corrupt. Next we input the basenames $bsn_I,bsn_V$ of the issuer and verifier. Then we instantiate two instances of the DAA protocol with the necessary parameters. Our encoding of the DAA protocol (see (S. Delaune, Ryan, and Smyth 2008)) follows directly from our informal description. Note that we use the strong phase and data swapping commands introduced by our extension to the calculus to ensure synchronisation. The two instances of the DAA processes must first execute all instructions of DAAJoin before moving onto DAASign. The separation of the protocol into strong phases is crucial for privacy to hold.   ## Analysis We use our translator to remove all instances of strong phases from our encoding and produce code suitable for input to ProVerif. Our translator produces a process (see (S. Delaune, Ryan, and Smyth 2008)) which permits the automatic verification of the privacy property using ProVerif. We are also able to detect the vulnerability in the original DAA protocol and prove the optimisation presented in (Smyth, Ryan, and Chen 2007). # Conclusion In this paper we have extended the class of equivalences which ProVerif is able to automatically verify. More specifically we are able to reason about processes which require data swapping and/or strong phases. Using the approach developed we are able to automatically verify the privacy properties of the electronic voting protocol FOO and the Direct Anonymous Attestation scheme. In future work, we would like to generalise our translation algorithm and provide a formal proof of the correctness of our translator. Moreover we plan to automate the swapping procedure.   # References
Abadi, Martı́n, and Cédric Fournet. 2001. “Mobile values, new names, and secure communication.” In *POPL’01: Proc. 28th ACM Symposium on Principles of Programming Languages*, 104–15. New York, USA: ACM Press.
Backes, Michael, Matteo Maffei, and Dominique Unruh. 2008. “Zero-Knowledge in the Applied Pi-Calculus and Automated Verification of the Direct Anonymous Attestation Protocol.” In *IEEE Symposium on Security and Privacy, Proceedings of SSP’08*.
Blanchet, Bruno, Martı́n Abadi, and Cédric Fournet. 2008. “Automated Verification of Selected Equivalences for Security Protocols.” *Journal of Logic and Algebraic Programming* 75 (1): 3–51.
Brickell, Ernie, Jan Camenisch, and Liqun Chen. 2004. “Direct Anonymous Attestation.” In *CCS ’04: 11th ACM Conference on Computer and Communications Security*, 132–45. New York, USA: ACM Press.
Chadha, Rohit, Steve Kremer, and Andre Scedrov. 2004. “Formal Analysis of Multi-Party Fair Exchange Protocols.” In *17th IEEE Computer Security Foundations Workshop*, edited by Riccardo Focardi, 266–79. Asilomar, USA: IEEE.
Clark, J., and J. Jacob. 1997. “A Survey of Authentication Protocol Literature.” [http://www.cs.york.ac.uk/\char126jac/papers/drareviewps.ps](http://www.cs.york.ac.uk/\char126jac/papers/drareviewps.ps).
Delaune, S., M. Ryan, and B. Smyth. 2008. “Automatic verification of privacy properties in the applied pi calculus (extended version).” University of Birmingham, School of Computer Science. [http://www.cs.bham.ac.uk/\char126bas/](http://www.cs.bham.ac.uk/\char126bas/).
Delaune, Stephanie, Steve Kremer, and Mark Ryan. 2006. “Coercion-Resistance and Receipt-Freeness in Electronic Voting.” In *CSFW ’06: Proc. 19th IEEE Workshop on Computer Security Foundations*, 28–42. IEEE.
Delaune, Stéphanie, Steve Kremer, and Mark D. Ryan. 2008. “Verifying Privacy-Type Properties of Electronic Voting Protocols.” Research Report. Laboratoire Spécification et Vérification, ENS Cachan, France.
Fujioka, Atsushi, Tatsuaki Okamoto, and Kazuo Ohta. 1993. “A Practical Secret Voting Scheme for Large Scale Elections.” In *ASIACRYPT ’92: Proceedings of the Workshop on the Theory and Application of Cryptographic Techniques*, 244–51. London: Springer.
Hirt, Martin, and Kazue Sako. 2000. “Efficient Receipt-Free Voting Based on Homomorphic Encryption.” In *Eurocrypt*, 1807:539–56. LNCS.
Kremer, Steve, and Mark D. Ryan. 2005. “Analysis of an Electronic Voting Protocol in the Applied Pi Calculus.” In *ESOP’05: Proc. Of the European Symposium on Programming*, 3444:186–200. LNCS.
Lowe, Gavin. 1995. “An attack on the Needham-Schroeder public-key authentication protocol.” *Information Processing Letters* 56 (3): 131–33.
Mukhamedov, A., and M. D. Ryan. 2007. “Fair Multi-party Contract Signing using Private Contract Signatures.” *Information & Computation*.
Smyth, Ben, Mark Ryan, and Liqun Chen. 2007. “Direct Anonymous Attestation (DAA): Ensuring privacy with corrupt administrators.” In *ESAS’07: 4th European Workshop on Security and Privacy in Ad Hoc and Sensor Networks*, 4572:218–31. LNCS.
[^1]: This work has been partly supported by the ARA SESUR project AVOTÉ and the EPSRC projects *Verifying anonymity and privacy properties* (EP/E040829/1) & *UbiVal* (EP/D076625/1). [^2]: This work has been partly supported by the ARA SESUR project AVOTÉ and the EPSRC projects *Verifying anonymity and privacy properties* (EP/E040829/1) & *UbiVal* (EP/D076625/1).