In loving memory of Andrew Cavan Ellis, who sadly died on 11 November 2009, aged 43.
#
For David Hercules Cash Carroll, Megan Naomi Eleanor Lee, and Alyssia Anne Smyth. May the future be good to you.
# Acknowledgements
First, and foremost, I would like to thank my supervisor Mark Ryan. Mark has dedicated a considerable amount of time and energy to the supervision of my research. He has helped me explore ideas, to critically evaluate my work, and to express my results clearly. He has imparted the fundamental skills of our discipline and, more importantly, he has taught me how to further my skills independently. His efforts will be cherished, and memories of my Ph.D. will be held in the highest regard. I look forward to our future collaboration and continued friendship.
I have had the opportunity to work with a number of collaborators and I have learnt a great deal from them all. Liqun Chen taught me the intricacies of cryptography; in particular, Direct Anonymous Attestation. Stéphanie Delaune guided my study of the applied pi calculus. Mounira Kourjieh’s boundless energy drove our research. Steve Kremer explained the subtleties of the applied pi calculus and insisted upon mathematical rigour. Bruno Blanchet helped me understand the theoretical underpinnings of ProVerif, and introduced numerous new ideas. Myrto Arapinis insisted that proofs could not begin with QED and patiently taught their proper construction; in addition, her Sushi is divine. Petr Klus helped implement theoretical results as software. The efforts of my collaborators have developed my research skills, for which I am truly grateful.
Birmingham’s *Formal Verification and Security Group* has been an excellent source of feedback and I am particularly grateful to: Myrto Arapinis, Sergiu Bursuc, Tom Chothia, Dan Ghica, Eike Ritter, Mark Ryan and Guilin Wang. I have also benefited from the wisdom of Martín Escardó and Eike Ritter who provided academic support as members of my *research monitoring group*. Mark Lee has provided an endless source of advice on topics as diverse as academic life and culinary masterpieces; and the occasional unsolicited bout on badgers, morris dancing and other such fields. Academic life at Birmingham has been wonderful and many individuals have influenced my stay: thank you Birmingham.
My experience gained through research visits has been hugely beneficial and the hospitality offered by each institution was superb. I am particularly grateful to my hosts: Liqun Chen at HP Labs; Steve Kremer at LSV, CNRS & ENS de Cachan; and Bruno Blanchet at ENS, CNRS & INRIA.
I will receive all the credit for this thesis – I also accept liability for any criticism – but, in addition to those already mentioned, some credit should be attributed to those whom studied early drafts. I am truly grateful to: Myrto Arapinis, Bruno Blanchet, Gavin Brown, Liqun Chen, Michael Clarkson, Véronique Cortier, Cas Cremers, Morten Dahl, Catherine Harris, Lucie Jíchová, Hugo Jonker, Vivek Nallur, James Nestoruk, Olufunmilola Onolaja, Mark Ryan, Winona Ryder, Matt Smart, Martin Smyth, Sue Smyth and Guilin Wang. In particular, Lucie Jíchová is my favourite *stickler*, Mark Ryan is a thorough technical critic, and my mum, Sue Smyth, read every last word.
Finally, I would like to thank my parents – Martin and Sue – for supporting me in everything I have chosen to do; my siblings – Matthew, Joe and Megan – for providing constant entertainment; and Beth Wells for a great friendship and numerous hours spent in *The Barrels*.
#
**Definition 1** (Observational equivalence). *Observational equivalence $\approx$ is the largest symmetric relation $\mathcal{R}$ between closed extended processes with the same domain such that $A \mathrel{\mathcal{R}}B$ implies:*
1. * if $A\Downarrow c$, then $B\Downarrow c$;*
2. * if $A \xrightarrow{}^* A'$, then $B \xrightarrow{}^* B'$ and $A' \mathrel{\mathcal{R}}B'$ for some $B'$;*
3. * $C[A] \mathrel{\mathcal{R}}C[B]$ for all closing evaluation contexts $C[\_]$.*
# Assumptions and notation
In this thesis, all signatures are tacitly assumed to include the constant $\varnothing$, unary functions $\mathsf{fst}$, $\mathsf{snd}$, and the binary function $\mathsf{pair}$. In addition, equational theories are assumed to include: $$\mathsf{fst}(\mathsf{pair}(x, y)) = x \qquad \mathsf{snd}(\mathsf{pair}(x, y)) = y$$ For convenience, $\mathsf{pair}(M_1, \mathsf{pair}(\dots, \mathsf{pair}(M_n, \varnothing)))$ is occasionally abbreviated as $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}M_1,\dots,\allowbreak M_n \mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ and $\mathsf{fst}(\mathsf{snd}^{i-1}(M))$ is denoted $\pi_{i}(M)$. We also introduce some convenient notation for sequence of names or variables. Given an infinite sequence of names or variables ${\sf u} = u_1,u_2,u_3,u_4,\dots$, the following self-explanatory abbreviations are used: $$\begin{array}{lcl}
\mathsf{head}({\sf u}) &=& u_1\\
\mathsf{tail}({\sf u}) &=& u_2,u_3,u_4,\dots\\
\mathsf{odd}({\sf u}) &=& u_1,u_3,\dots\\
\mathsf{even}({\sf u}) &=& u_2,u_4,\dots
\end{array}$$
**Formalisation of security properties**
**The failure of cryptographic protocols has been directly attributed to the absence of rigorously defined security properties. This part introduces symbolic definitions for security in electronic voting and anonymous attestation.**
# untitled section
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 105, column 1): unexpected \vskip expecting \end{document} \end{overview} ^`
``` latex
\chapter[Election verifiability in electronic voting]
{Election verifiability in electronic voting\symbolfootnotemark}\label{chap:ev}
\symbolfootnotetext{This chapter is an extension of~\cite{Smyth10:ElectionVerifiability,Smyth10:ElectionVerifiabilityA}.}
%In particular, the definition of \emph{election verifiability} is strengthened in a manner desirable for electronic voting protocols based upon homomorphic encryption. \sout{Additionally, the methodology supporting automated reasoning was inspired by~\cite{Smyth10:ElectionVerifiabilityA}.}}
\begin{overview}
A definition of election verifiability is presented in terms of boolean tests which can be performed on the data produced by an election. The definition allows the evaluation of election verifiability in electronic voting protocols. It also allows the identification of hardware and software components that must be trusted for the purpose of verifiability, thereby facilitating the comparison of electronic voting protocols on the basis of trust assumptions. Our definition of election verifiability is compatible with a large class of electronic voting schemes -- including those based upon blind signatures, homomorphic encryption and mixnets -- as will be demonstrated by analysing the FOO, Helios 2.0 and JCJ-Civitas electronic voting protocols.
\end{overview}
\noindent %Electronic voting systems are being introduced, or trialled, in several countries.
% to provide more efficient voting procedures.
Electronic voting systems lack the transparency provided by their paper counterparts. For example, paper-based elections often allow observation of the whole process (that is, from ballot casting to tallying) and rely upon robustness characteristics of the physical world (such as the impossibility of altering the markings on a paper ballot sealed inside a locked ballot box). By comparison, it is not possible to observe the electronic operations performed on bitstrings. As a consequence, computer systems may alter votes in a way that cannot be detected. % by either voters or election observers.
%From a voter's perspective this situation can be described as \emph{voting on Satan's computer}, analogously with \cite{AN95}.
Some electronic voting systems attempt to eliminate the necessity for transparency under the hypothesis that the hardware and software running the election can be trusted. Unsurprisingly, this level of trust is very difficult to achieve and thus deployed systems based upon such assumptions have failed~\cite{GermanyCourt09,Dutch08,DebraBowenCalifornia07,ElectoralCommision07}.
The concept of \emph{election verifiability} (also known as \emph{end-to-end verifiability}) has emerged in the academic literature to address this problem (for example, \cite{JCJ02,ChaumRyanSchneider2005,BenAdidaThesis,DagstuhlAccord07,Adida08}). The notion should allow voters and election observers to verify -- independently of the hardware and software running the election -- that votes have been recorded, tallied and declared correctly. Two aspects of verifiability are generally distinguished.
\begin{itemize}
\item \emph{Individual verifiability:} a voter can check that her own ballot is published on the election's bulletin board.
\item \emph{Universal verifiability:}
anyone can check that all the votes in the election outcome correspond to ballots published on the election's bulletin board.
%\textcolor{red}{anyone can check the ballots published on the election's bulletin board are well-formed and all the votes in the election outcome correspond to those ballots.}
%\textcolor{red}{anyone can check that all the votes in the election outcome correspond to distinct ballots published on the election's bulletin board.}
%anyone can check that the election outcome corresponds to the ballots published on the bulletin board.
\end{itemize}
%
In this thesis, another aspect is also identified.
%
\begin{itemize}
\item \emph{Eligibility verifiability:} anyone can check that each ballot published on the bulletin board was cast by a registered voter and at most one ballot is tallied per voter.
%anyone can check that each vote in the election outcome was cast by a registered voter and there is at most one vote per voter.
\end{itemize}
%
Eligibility verifiability is explicitly distinguished as a distinct property (although it occasionally appears as part of universal verifiability in the literature).
\contribution
A definition of election verifiability which captures individual, universal and eligibility verifiability is presented. Formally, the definition captures verifiability as a triple of boolean tests $\Riv, \Ruv$, and $\Rev$ which are required to satisfy several conditions when parametrised with the data produced by an election protocol, for all possible protocol executions. The test $\Riv$ is intended to be checked by individual voters who instantiate the test with their private information (for example, their vote, and data derived during the execution of the protocol) and public information relating to the election (for example, the contents of the bulletin board). The tests $\Ruv$ and $\Rev$ can be checked by any external observer and hence only rely on public information.
The consideration of eligibility verifiability is particularly interesting, as it provides an assurance that the election outcome corresponds to votes legitimately cast. This property has been largely neglected by existing electronic voting protocols, despite its suitability as a mechanism to detect ballot stuffing.
Our definition of election verifiability dictates that only those parts of the voting system that need to be trusted to achieve verifiability should be modelled; all the remaining parts of the system are controlled by the adversarial environment. This is a further interesting aspect because it allows the clear identification of trust assumptions needed for verifiability, and, therefore, permits comparison of electronic voting protocols. In complementary work, Pieters~\cite{Pieters10:WhatProof} compares voting systems on the basis of the proof techniques used to achieve verifiability.
Tests $\Riv, \Ruv$, and $\Rev$ are assumed to be verified in a trusted environment (if a test is checked by malicious software that always evaluates the test to hold, it is useless). However, the verification of these tests can be repeated on different machines, using software provided by various stakeholders, thereby increasing confidence. Alternatively, this assumption can be eliminated by adopting human-verifiable tests as described by Adida~\cite[Chapter~5]{BenAdidaThesis}.
The application of our election verifiability definition is demonstrated by analysing verifiability in three case studies: the protocol by Fujioka, Okamoto \& Ohta~\cite{FOO} (commonly referred to as the FOO protocol); the Helios 2.0 protocol~\cite{AdidaPereiraMarneffeQuisquater} which was effectively used in
%
the election of board memebers for the International Association of Cryptologic Research, the
presidential election at the Catholic University of Louvain, and the student vice president
at Princeton University; and the protocol by Juels, Catalano \& Jakobsson~\cite{JCJ02,JCJ05,JCJ10} which has been implemented by Clarkson, Chong \& Myers~\cite{CCM08,CCM08b} as Civitas (we occassionally refer to this protocol as JCJ-Civitas). This demonstrates the suitability of the definition for a large class of protocols, including schemes based upon mixnets, homomorphic encryption and blind signatures. The protocols by Fujioka, Okamoto \& Ohta and Helios 2.0 will be shown not to satisfy eligibility verifiability and are vulnerable to ballot stuffing by dishonest administrators. As these protocols do not proclaim to satisfy eligibility verifiability, this is not claimed to be an attack, but simply a clarification of precisely which aspects of verifiability are satisfied.
\structure Section~\ref{sec:ev:prot} formalises electronic voting protocols in the applied pi calculus. Section~\ref{sec:iv} specifies some notational conventions and defines the individual and universal verifiability aspects of our definition (Section~\ref{sec:ev:iv-uv}). The analysis of FOO is presented in Section~\ref{sec:foo}, and Helios is studied in Section~\ref{sec:helios}. Our definition %of election verifiability
is extended to eligibility in Section~\ref{sec:elig}, and JCJ-Civitas is analysed in Section~\ref{sec:jcj}. Finally, a summary is presented in Section~\ref{sec:ev:summary}.
```
# Formalising electronic voting protocols
The framework should permit explicit specification of the trusted parts of an election protocol. Ideally, only the communication channel between voters and voting terminals should be trusted. In particular, the voter should not need to trust the election hardware or software. However, achieving absolute verifiability in this context is difficult and the trustworthiness of some parts of the protocol are often assumed. Such trust assumptions are motivated by the fact that certain components of a protocol can be audited, or can be executed in a distributed manner amongst several different election officials. For instance, in Helios 2.0 (**AdidaPereiraMarneffeQuisquater?**) the ballot construction can be audited using a cast-or-audit mechanism (see Benaloh (**Benaloh06:BallotAudit?**; **Benaloh07:BallotAudit?**) for further details on ballot auditing).
Formally, the trusted parts of the voting protocol can be captured using a voting process specification (Definition
**Definition 1** (Voting process specification). *A *voting process specification* is a tuple $\langle V, A \rangle$, where $V$ is a plain process without replication and $A$ is a closed evaluation context such that $\textnormal{fv}(V)=\{v\}$ and $\textnormal{rv}(V) = \emptyset$.*
Given a voting process specification $\langle V, A \rangle$, integer $n\in\mathbb{N}$, and names $s_1,\dots,s_n$, we can build the voting process $${\sf VP}_n(s_1,\dots,s_n) = A[ V_1 \mid\dots\mid V_n]$$ where $V_i = V \{^{s_i} / _v\}$. Intuitively, ${\sf VP}_n(s_1,\allowbreak\dots,\allowbreak s_n)$ models the protocol with $n$ voters casting votes for candidates $s_1, \ldots, s_n$. Note that the votes $s_1, \ldots, s_n$ are not required to be distinct (several voters may cast votes for the same candidate).
**Example 1** (Raising hands protocol). *Consider the *raising hands* protocol in which every voter outputs her signed vote. Cryptographic primitives are captured by the signature $\Sigma = \{\mathsf{true},\mathsf{getmsg},\mathsf{pk},\mathsf{checksign},\mathsf{sign}\}$, where $\mathsf{true}$ is a constant, $\mathsf{getmsg}$ and $\mathsf{pk}$ are unary functions, and functions $\mathsf{checksign}$ and $\mathsf{sign}$ are binary. The signature is associated with the equations: $$\begin{array}{lcl}
\mathsf{checksign}(\mathsf{pk}(x_{\mathsf{sk }}),\mathsf{sign}(x_{\mathsf{sk }},x_{\mathsf{msg }})) &=& \mathsf{true}\\
\mathsf{getmsg}(\mathsf{sign}(x_{\mathsf{sk }},x_{\mathsf{msg }})) &=& x_{\mathsf{msg }}
\end{array}$$ A trusted administrator, modelled by the context $A_{\sf ex}$, is assumed to distribute keying material to voters and publish each voter’s public key. $$A_{\sf ex}[\_] \; \widehat = \; \nu d. \nu sk_A. ( ! \nu sk_V. \overline{d}\langle sk_V\rangle.\overline{c}\langle\mathsf{sign}(sk_A,\mathsf{pk}(sk_V))\rangle \mid \{ ^{\mathsf{pk}(sk_A)} / _{x_{pk}} \} \mid \_)$$ The channel $d$ is under name restriction to ensure voters’ keys are distributed privately, and the active substitution $\{ ^{\mathsf{pk}(sk_A)} / _{x_{pk}} \}$ models the fact that the administrator’s public key is known (for example, published on the election bulletin board). The voter, who receives her private key and then outputs her signed vote paired with her public key, is modelled by the process: $$V_{\sf ex} \; \widehat = \; d(x_{sk_V}). \overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(x_{sk_V}), \mathsf{sign}(x_{sk_V},v)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} \rangle$$ This protocol satisfies election verifiability, as will be shown later in this chapter.*
For the purposes of individual verifiability, the voter may rely upon some data derived during the protocol execution. To take such data into consideration, we distinguish a subset of variables which we call *record variables* $r$ and extend plain processes with the *record message* ${\sf rec}(r,M).P$ construct. The record message construct permits a voter to privately record some information which she may later use to verify the election. This behaviour is captured by extending internal reduction to include ${\sf rec}(r,M).P \to P \mid \{^M / _r\}$. Record variables are assumed to be unique in each process; that is, a record variable may appear at most once. The type system ensures that the term $M$ and record variable $r$ have the same type in ${\sf rec}(r,M)$; it also enforces that record variables may only be used in the first argument of the ${\sf rec}$ construct or in the domain of an extended process. Definition
**Definition 2**. *Let $\sf rv$ be an infinite sequence of distinct record variables. Given a process $P$ which does not contain replication, we define $\mathsf{R}(P) =\mathsf{R}'({\sf rv}, P)$, where: $$\begin{array}{lcl}
\mathsf{R}'({\sf r},\, 0) & \widehat= & 0 \\
\mathsf{R}'({\sf r},\, P \mid Q) & \widehat= & \mathsf{R}'(\text{odd}({\sf r}), P) \mid \mathsf{R}'(\text{even}({\sf r}),Q)\\
\mathsf{R}'({\sf r},\, \nu\,n.P) & \widehat= & \nu\,n.{\sf rec}(\text{head}({\sf r}), n).\mathsf{R}'(\text{tail}({\sf r}),P)\\
\mathsf{R}'({\sf r},\, u(x).P) & \widehat= & u(x).{\sf rec}(\text{head}({\sf r}), x).\mathsf{R}'(\text{tail}({\sf r}),P)\\
\mathsf{R}'({\sf r},\, \overline{u}\langle M\rangle.P) & \widehat= & \overline{u}\langle M\rangle.\mathsf{R}'({\sf r},P)\\%
\mathsf{R}'({\sf r},\, \textnormal{if } M = N \textnormal{ then } P \textnormal{ else }Q) & \widehat= & \textnormal{if } M = N \textnormal{ then } \mathsf{R}'(\text{odd}({\sf r}),P) \textnormal{ else }\mathsf{R}'(\text{even}({\sf r}),Q)
\end{array}$$*
Given a tuple of record variables $\tilde r$, the tuple of record variables obtained by indexing each record variable in $\tilde r$ with $i$ is denoted $\tilde r_i$. The set of record variables in a process and term are denoted $\textnormal{rv}(A)$ and $\textnormal{rv}(M)$. A voting process can now be constructed such that the voter $V$ records the values constructed and input during execution.
**Definition 3** (Augmented voting process). *Given a voting process specification $\langle V, A \rangle$, integer $n\in \mathbb N$ and names $s_1, \ldots , s_n$, the *augmented voting process* $${\sf VP}_n^+(s_1,\ldots,s_n) = A[V_1^+ \mid\dots\mid V_n^+]$$ where $V_i^+ = \mathsf{R}(V) \{^{s_i}/_v\} \{^{r_i}/_r \mid r \in \textnormal{rv}(\mathsf{R}(V))\}$.*
The augmented voting process ${\sf VP}_n^+(s_1,\ldots,s_n)$ models the voting protocol for $n$ voters casting votes $s_1,\ldots,s_n$, who privately record the data that may be needed for verification using record variables $\tilde r_i$.
**Example 2**. *Given integer $n\in \mathbb N$ and names $s_1, \ldots , s_n$, the augmented voting process associated with our raising hands process specification $\langle V_{\sf ex}, A_{\sf ex} \rangle$ is defined as follows $$\begin{gathered}
A_{\sf ex}[d(x_{sk_V}). {\sf rec}(r_1, x_{sk_V}).\overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(x_{sk_V}), \mathsf{sign}(x_{sk_V},s_1)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} \rangle \mid \dots \\\mid d(x_{sk_V}).{\sf rec}(r_n, x_{sk_V}). \overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(x_{sk_V}), \mathsf{sign}(x_{sk_V},s_n)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} \rangle ]
\end{gathered}$$*
# Election verifiability
Election verifiability is captured using three tests $\Phi^{IV}$, $\Phi^{UV}$, and $\Phi^{EV}$. Formally, a test is built from conjunctions and disjunctions of *atomic tests* of the form $(M = N)$, where $M,N$ are terms. Tests may contain variables, and will need to hold on frames arising from arbitrary protocol executions. We now recall the purpose of each test and assume some naming conventions about variables.
*Individual verifiability:* The test $\Phi^{IV}$ allows a voter to identify her ballot on the bulletin board. The test has:
- a variable $v$ referring to a voter’s vote.
- a variable $w$ referring to a voter’s public credential.
- some variables $x,x',\bar{x},\dots$ expected to refer to global public values pertaining to the election (for example, public keys belonging to election administrators).
- a variable $y$ expected to refer to the voter’s ballot on the bulletin board.
- some record variables $r_1,\dots,r_k$ referring to the voter’s private data.
*Universal verifiability:* The test $\Phi^{UV}$ allows an observer to check that votes in the election outcome correspond to ballots on the bulletin board.
- a variable $\hat{v}$ referring to a tuple representing the election outcome.
- some variables $x,x',\bar{x},\dots$ as above.
- a variable $\hat{y}$ expected to refer to a tuple containing all of the voters’ ballots on the bulletin board.
- some variables $z,z',\bar z,\dots$ expected to refer to outputs generated by the protocol for the purposes of universal and eligibility verification.
*Eligibility verifiability:* The test $\Phi^{EV}$ allows an observer to check that each ballot on the bulletin board was cast by a registered voter and at most one ballot is tallied per voter. The test has:
- a variable $\hat{w}$ referring to a tuple containing public credentials of eligible votes.
- a variable $\hat y$, variables $x,x',\bar{x},\dots$ and variables $z,z',\bar z,\dots$ as above.
The remainder of this section will focus on the individual and universal aspects of our definition; eligibility verifiability will be discussed in Section
**Definition 1** (Individual and universal verifiability). *A voting specification $\langle V, A \rangle$ *satisfies individual and universal verifiability* if there exists a test $\Phi^{IV}$, where for all $m\in\mathbb{N}$ there exists a test $\Phi^{UV}_m$, such that $\textnormal{fn}(\Phi^{IV})=\textnormal{fn}(\Phi^{UV}_m)= \textnormal{rv}(\Phi^{UV}_m)
=\emptyset$ and $\textnormal{rv}(\Phi^{IV}) \subseteq \textnormal{rv}(\mathsf{R}(V))$, and for all names $s_1,\dots,s_n$ the conditions below hold. Let $\tilde r=\textnormal{rv}(\Phi^{IV})$ and $\Phi^{IV}_i = \Phi^{IV}\{^{s_i} /_v,
\textnormal{\raisebox{2pt}{\footnotesize $\tilde r_{i}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $\tilde r$}} \}$.*
#### Soundness.
*For all contexts $C$, such that $C[{\sf VP}_n^+(s_1,\dots,\allowbreak s_n% ,\allowbreak id_1,\dots,\allowbreak id_n
)]\allowbreak
\mathrel{(\xrightarrow{}^* \xrightarrow{\alpha} \xrightarrow{}^*)^*} B$ and $\varphi(B)\equiv\nu\tilde n.\sigma$ for some process $B$, substitution $\sigma$ and names $\tilde n$, we have: $$\label{cond2}
\forall i,j.\quad
\Phi^{IV}_i\sigma
\wedge
\Phi^{IV}_j\sigma
\Rightarrow i = j$$ $$\label{cond3}
\Phi^{UV}_m \sigma \wedge \Phi^{UV}_m \{^{\hat v'}/_{\hat v} \} \sigma \Rightarrow \hat v\sigma \simeq \hat v'\sigma% \wedge |\hat y \sigma | = |\hat v \sigma|}$$ $$\label{cond5}
\bigwedge_{1 \leq i \leq n} \Phi^{IV}_i \{\textnormal{\raisebox{2pt}{\footnotesize $\pi_{i}(\hat{y})$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\} \sigma \wedge \Phi^{UV}_m \sigma \wedge n = m \Rightarrow \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{s_1,\dots,s_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} \simeq \hat v\sigma$$*
#### Effectiveness.
*There exists a context $C$, process $B$, substitution $\sigma$ and names $\tilde n$, such that $C[{\sf VP}_n^+(s_1,\dots,\allowbreak s_n% ,\allowbreak id_1,\dots,\allowbreak id_n
)]\allowbreak
\mathrel{(\to^* \xrightarrow{\alpha} \to^*)^*} B$, $\varphi(B)\equiv\nu\tilde n.\sigma$ and $$\label{cond7}
\bigwedge_{1 \leq i \leq n} \Phi^{IV}_i \{\textnormal{\raisebox{2pt}{\footnotesize $\pi_{i}(\hat{y})$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\} \sigma \wedge \Phi^{UV}_n \sigma$$*
An individual voter should verify that the test $\Phi^{IV}$ holds when instantiated with her vote $s_i$, the information $\tilde r_i\sigma$ recorded during the execution of the protocol and some bulletin board entry $y\sigma$. Condition (
**Definition 2**. *The voting process specification $\langle V_{\sf foo},A_{\sf foo}\rangle$ is defined as $V_{\sf foo} \mathrel{\hat =} \nu \mathit{k}. \overline{c}\langle v\rangle. \overline{c}\langle\mathit{k}\rangle$ and $A_{\sf foo}[\_] \mathrel{\hat =} \_ .$*
We do not assert that the voting terminal uses blind signatures (although this is crucial for privacy properties, it does not contribute to verifiability); accordingly, blinding operations do not appear in our specification and, moreover, no trust assumptions are made about whether blinding is used. Similarly, the voter’s signature on the blinded committed vote and the confidentiality of signing keys are not required for individual and universal verifiability; they are, however, essential for eligibility.
### Analysis: Individual and universal verifiability
Given integer $m\in\mathbb{N}$ let tests $\Phi^{IV}$ and $\Phi^{UV}_m$ be defined as follows: $$\begin{array}{lcl}
\Phi^{IV}&\mathrel{\hat=}& y =_E \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{r,\mathsf{commit}(r,v)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} \\
\Phi^{UV}_m &\mathrel{\hat=}& \hat v =_E
\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{open}(\pi_{1}(\pi_{1}(\hat y)),\pi_{2}(\pi_{1}(\hat y))),\dots,
\mathsf{open}(\pi_{1}(\pi_{m}(\hat y)),\pi_{2}(\pi_{m}(\hat y)))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}%\\
%&& \textcolor{blue}{\mathrel{\wedge} \mathsf{snd}^m(\hat y) =_\EE \Emptytuple}
\end{array}$$ Intuitively, a bulletin board entry should be a pair formed from the voter’s nonce and the associated commitment to her vote. The identifier $\ell$ and the registrar’s signature are not required for the purpose of verifiability, so these details are omitted.
**Theorem 1**. *$\langle V_{\sf foo},A_{\sf foo}\rangle$ satisfies individual and universal verifiability.*
xx̄x̄ $\mathsf{dec}(x_{\mathsf{sk }},\mathsf{penc}(\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{rand }},x_{\mathsf{plain }})) = x_{\mathsf{plain }}$
$\mathsf{dec}({\mathsf{partial}}(x_{\mathsf{sk }},ciph),ciph) = x_{\mathsf{plain }}$
where $ciph=\mathsf{penc}(\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{rand }},x_{\mathsf{plain }})$
$\mathsf{penc}(x_{\mathsf{pk }},y_{\mathsf{rand }},y_{\mathsf{plain }})*\mathsf{penc}(x_{\mathsf{pk }},z_{\mathsf{rand }},z_{\mathsf{plain }}) = \mathsf{penc}(x_{\mathsf{pk }},y_{\mathsf{rand }}\circ z_{\mathsf{rand }},y_{\mathsf{plain }}+z_{\mathsf{plain }})$
$\mathsf{checkBallotPf}(x_{\mathsf{pk }},ballot,\mathsf{ballotPf}(x_{\mathsf{pk }},x_{\mathsf{rand }},s,ballot)) = \mathsf{true}$
where $ballot=\mathsf{penc}(x_{\mathsf{pk }},x_{\mathsf{rand }},s)$
${\mathsf{checkPartialPf}}(\mathsf{pk}(x_{\mathsf{sk }}),ciph,partial,{\mathsf{partialPf}}(x_{\mathsf{sk }},ciph,partial)) = \mathsf{true}$
where $ciph=\mathsf{penc}(\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{rand }},x_{\mathsf{plain }})\text{ and }partial={\mathsf{partial}}(x_{\mathsf{sk }},ciph)$
Note that in the equation for $\mathsf{checkBallotPf}$, $s$ is a name and not a variable. As the equational theory is closed under bijective renaming of names, this equation holds for any name, but fails if one replaces the name by a term, for example, $s + s$. We assume that all names are possible votes but give the possibility to check that a voter does not include a term $s + s$ which would add a vote to the outcome.
### Model in applied pi
The browser script is not verifiable; accordingly, the voter most trust:
- Ballot construction; that is, the script generates a pair consisting of the voter’s encrypted vote and a proof that the ballot represents an allowed vote.
Although the voter cannot be assured that the script behaves correctly, trust is motivated because the voter can audit ballot construction. Accordingly, the browser script is modelled as part of the trusted context $A_{\sf helios}$ in the voting process specification $\langle V_{\sf helios},A_{\sf helios}\rangle$. The voter $V_{\sf helios}$ receives a channel name $y$ on a private channel; this is a technical aspect of our formalisation which allows the voter to privately communicate with her browser script. She sends her vote on this channel to $A_{\sf helios}$, which creates the ballot for her. The voter is sent the constructed ballot $x_{\mathsf{ballot }}$ and forwards it to the bulletin board. We assume that the voter’s inputs $y$ and $x_{\mathsf{ballot }}$ are stored in record variables $r_y$ and $r_{ballot}$. $A_{\sf helios}$ represents the parts of the system that are required to be trusted; it publishes the election key, and includes the ballot creation script $B$ which receives a voter’s vote, generates a random $m$ and returns the ballot (that is, the encrypted vote and a proof) to the voter.
**Definition 3**. *The voting process specification $\langle V_{\sf helios},A_{\sf helios}\rangle$ is defined where $$\begin{array}{r@{\;}c@{\;}l}
V_{\sf helios} &\hat=& d(y).\overline{y}\langle v\rangle. y(x_{\mathsf{ballot }}).\overline{c}\langle x_{\mathsf{ballot }}\rangle\\
A_{\sf helios}[\_] &\hat=& \nu d.\big(\, (! \nu d'.\overline{d}\langle d'\rangle.B) \mid \{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{pk }}$}}\}\mid \_\ \big) \\
B &\hat=& d'(x_{\mathsf{vote} }).\nu m. \overline{d'}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{penc}(x_{\mathsf{pk }},m,x_{\mathsf{vote} }),\mathsf{ballotPf}(x_{\mathsf{pk }},m,x_{\mathsf{vote} },\mathsf{penc}(x_{\mathsf{pk }},m,x_{\mathsf{vote} }))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle
\end{array}$$*
At the end of the election the bulletin board is represented by a frame. The frame is expected to define the trustees’ public key as $x_{pk}$ and the ballots as $\hat y$. It also contains the homomorphic tally $z_{\mathsf{tally} }$ of the encrypted ballots, and the partial decryption $z_{\mathsf{partial} }$, together a proof of correctness $z_{\mathsf{partialPf}}$, obtained from the trustees. When the protocol is honestly executed by $n$ voters, the resulting frame should have a substitution $\sigma$ such that for all $1 \leq i \leq n$ we have $$\begin{array}{lcl}
x_{pk} \sigma&=& \mathsf{pk}(sk) \\
\pi_{i}(\hat y) \sigma &=& \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}\mathsf{penc}(\mathsf{pk}(sk),m_i,s_i), \mathsf{ballotPf}(\mathsf{pk}(sk),m_i,s_i,\mathsf{penc}(\mathsf{pk}(sk),m_i,s_i))\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\\
z_{\mathsf{partial} }\sigma&=& {\mathsf{partial}}(sk,z_{\mathsf{tally} })\sigma \\
z_{\mathsf{partialPf}}\sigma&=& {\mathsf{partialPf}}(sk,z_{\mathsf{tally} },z_{\mathsf{partial} })\sigma \\
z_{\mathsf{tally} }\sigma&=& \pi_{1}(\pi_{1}(\hat y\sigma))*\dots*\pi_{1}(\pi_{n}(\hat y\sigma))
\end{array}$$
### Analysis: Individual and universal verifiability
Given $m\in\mathbb{N}$, the tests $\Phi^{IV}$ and $\Phi^{UV}_m$, defined below, are introduced for verifiability purposes. $$\begin{array}{r@{\;}c@{\;}l}
\Phi^{IV}&\widehat=& y =_Er_{ballot} \\
\Phi^{UV}_m &\widehat=& z_{\mathsf{tally} }=_E\pi_{1}(\pi_{1}(\hat y))*\dots*\pi_{1}(\pi_{m}(\hat y))\\
&& \mathrel{\land} \bigwedge_{i=1}^{m}(\mathsf{checkBallotPf}(x_{\mathsf{pk }},\pi_{1}( \pi_{i}(\hat y)),\pi_{2}(\pi_{i}(\hat y))) =_E\mathsf{true})\\
&& \mathrel{\land} {\mathsf{checkPartialPf}}(x_{\mathsf{pk }},z_{\mathsf{tally} },z_{\mathsf{partial} },z_{\mathsf{partialPf}}) =_E\mathsf{true}\\
&& \mathrel{\land} \pi_{1}(\hat v)+\dots+\pi_{m}(\hat v) =_E\mathsf{dec}(z_{\mathsf{partial} },z_{\mathsf{tally} }) \\
&& \mathrel{\land} %\mathsf{snd}^m(\hat y) =_\EE \Emptytuple \land
\mathsf{snd}^m(\hat v) =_E\varnothing
\end{array}$$ The test $\Phi^{IV}$ checks that the voter’s ballot is recorded on the bulletin board and $\Phi^{UV}_m$ checks that the tally is correctly computed.
**Theorem 2**. *$\langle V_{\sf helios},A_{\sf helios} \rangle$ satisfies individual and universal verifiability.*
**Proposition 1**. *The raising hands protocol $\langle A_{\sf ex},V_{\sf ex}\rangle$ satisfies election verifiability.*
The proof of this result appears in Appendix
**Definition 1**. *The voting process specification $A_{\sf jcj},V_{\sf jcj}$ is defined where: $$\begin{array}{rcl}
A_{\sf jcj} &\mathrel{\hat=}& \nu\,a,ssk_R.({!R} \mid \{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_R)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{pk_R}}$}},\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(ssk_R)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{spk_R}$}},\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_T)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{pk_T}}$}}\} \mid \_)\\
V_{\sf jcj} &\mathrel{\hat=}& \nu\,m,m'.a(x_{cred}).\textnormal{let } ciph=\mathsf{penc}(x_{pk_T},m,v) \textnormal{ in }\\
&&\textnormal{let } ciph'=\mathsf{penc}(x_{pk_R},m',\pi_{1}(x_{cred})) \textnormal{ in }\\
&&\textnormal{let } spk=\mathsf{ballotPf}(x_{pk_T},m,v,x_{pk_R},m',\pi_{1}(x_{cred})) \textnormal{ in }\\
&&\overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{ciph,ciph',spk}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle\\
R &\mathrel{\hat=}& \nu\,d,m''.\,
% &&\Letin{cred}{\Penc{x_{pk_R}}{\rr''}{d}}\\
\textnormal{let } sig=\mathsf{sign}(ssk_R,\mathsf{penc}(x_{pk_R},m'',d)) \textnormal{ in }
\overline{a}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{d,sig}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.\overline{c}\langle sig\rangle
\end{array}$$*
At the end of the election, the bulletin board is represented by a frame. In our formalism, we expect the frame to contain the substitution $\sigma$ which defines the voters’ public credentials as $\hat w$, the registrars’ public keys as $x_{pk_R}$ and $x_{spk_R}$, and talliers’ public key as $x_{pk_T}$. A tuple $\hat y$ containing triples representing each voter’s ciphertexts and signature proofs of knowledge. The mixed re-encryptions of the voter’s ciphertexts $z_{\mathsf{bal},1},\dots,z_{\mathsf{bal},n}$, along with a proof ${z_{\mathsf{mixPairPf}}}$ that the mix was performed correct. For verifiable decryption, we assume $z_{\mathsf{partial},i}$ is defined as a partial decryption associated with the proof $z_{\mathsf{partialPf},i}$. For the purposes of eligibility verifiability, we also expect the mixed re-encryptions of the voter’s public credentials $z_{\mathsf{cred},1}, \dots, z_{\mathsf{cred},1}$, along with a proof of correctness ${z_{\mathsf{mixPf}}}$. For convenience, a reordering ${\bar{z}}_{\mathsf{cred},1},\dots,{\bar{z}}_{\mathsf{cred},n}$ of these re-encryptions is also computed. Finally, we expect PET proofs $z_{\mathsf{petPf},1},\dots,z_{\mathsf{petPf},n}$ for the re-encryptions of the ciphertext constructed by the voter on her private credential (that is, the output of the verifiable mix in Step
$\Phi^{IV}$xx̄$\widehat =$̄ $\Phi^{IV}$ $\widehat =$ $y =_E\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}\mathsf{penc}(x_{\mathsf{pk_T}},r_{m},v),\mathsf{penc}(x_{\mathsf{pk_R}},r_{m'},\pi_{1}(r_{cred})),$
$\qquad\mathsf{ballotPf}(x_{\mathsf{pk_T}},r_{m},v,x_{\mathsf{pk_R}},r_{m'},\pi_{1}(r_{cred})) \mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\wedge w = \pi_{2}(r_{cred})$
$\Phi^{UV}_m$ $\widehat =$ $\mathsf{checkMixPair}({z_{\mathsf{mixPairPf}}},\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(\pi_{1}(\hat y)),\pi_{2}(\pi_{1}(\hat y))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},\ldots,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(\pi_{m}(\hat y)),\pi_{2}(\pi_{m}(\hat y))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},$
$\qquad\qquad z_{\mathsf{bal},1},\ldots,z_{\mathsf{bal},m}) =_E\mathsf{true}$
$\mathrel{\wedge} \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{dec}(z_{\mathsf{partial},1},\pi_{1}(z_{\mathsf{bal},1})),\dots,\mathsf{dec}(z_{\mathsf{partial},m},\pi_{1}(z_{\mathsf{bal},m}))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} =_E\hat v$
$\mathrel{\wedge}\bigwedge_{i=1}^{m} {\mathsf{checkPartialPf}}(x_{\mathsf{pk_T}},\pi_{1}(z_{\mathsf{bal},i}),z_{\mathsf{partial},i},z_{\mathsf{partialPf},i}) =_E\mathsf{true}$
$\Phi^{EV}_m$$\widehat =$ $\bigwedge_{i=1}^{m} \mathsf{checkBallot}(\pi_{3}(\pi_{i}(\hat y)),\pi_{1}(\pi_{i}(\hat y)),\pi_{2}(\pi_{i}(\hat y))) =_E\mathsf{true}$
$\mathrel{\wedge}\mathsf{checkMixPair}({z_{\mathsf{mixPairPf}}},\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(\pi_{1}(\hat y)),\pi_{2}(\pi_{1}(\hat y))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},\ldots,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(\pi_{{m}}(\hat y)),\pi_{2}(\pi_{{m}}(\hat y))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},$
$\qquad\qquad z_{\mathsf{bal},1},\ldots,z_{\mathsf{bal},{m}}) =_E\mathsf{true}$
$\mathrel{\wedge}\bigwedge_{i=1}^{m} \mathsf{pet}(z_{\mathsf{petPf},i},\pi_{2}(z_{\mathsf{bal},i}),{\bar{z}}_{\mathsf{cred},i}) =_E\mathsf{true}$
$\mathrel{\wedge}\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{z_{\mathsf{cred},1},\ldots,z_{\mathsf{cred},{m}}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\simeq\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{{\bar{z}}_{\mathsf{cred},1},\ldots,{\bar{z}}_{\mathsf{cred},{m}}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$
$\mathrel{\wedge}\mathsf{checkMix}({z_{\mathsf{mixPf}}},\mathsf{getmsg}(\pi_{1}(\hat w)),\ldots,\mathsf{getmsg}(\pi_{{m}}(\hat w)),z_{\mathsf{cred},1},\ldots,z_{\mathsf{cred},{m}}) =_E\mathsf{true}$
$\mathrel{\wedge}\bigwedge_{i=1}^{m} \mathsf{checksign}(x_{spk_R},\pi_{i}(\hat w))=_E\mathsf{true}$
$\bigwedge_{i=1}^{m} \pi_{4}(\hat y) =_E{\varnothing}\mathrel{\wedge} \mathsf{snd}^m(\hat w) =_E{\varnothing}\mathrel{\wedge} \mathsf{snd}^m(\hat y) =_E{\varnothing}$
The test $\Phi^{IV}$ checks that the voter’s ballot and public credential are recorded on the bulletin board. The test $\Phi^{UV}_m$ checks that the tally is correctly computed; that is, the mix is checked, the validity of partial decryptions have been verified and the decrypted tally corresponds to the election outcome. Finally, the test $\Phi^{EV}_m$ checks that only eligible ballots are considered; that is, ballots are correctly formed, mixes have been handled in a suitable manner, PETs have been verified and only authentic public voter credentials are considered.
**Theorem 1**. *$\langle A_{\sf jcj}, V_{\sf jcj} \rangle$ satisfies election verifiability.*
The proof of Theorem
**Definition 1** (Observational equivalence). **Observational equivalence* $\sim$ is the largest symmetric relation $\mathcal{R}$ between 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 $Q \rightarrow Q'$ and $P' \mathrel{\mathcal{R}} Q'$ for some $Q'$;*
3. *$C[P]\mathrel{\mathcal{R}}C[Q]$ for all evaluation contexts $C[\_]$.*
We define observational equivalence as a property of biprocesses.
**Definition 2**. *The closed biprocess $P$ *satisfies observational equivalence* if $\textnormal{fst}(P)\sim\textnormal{snd}(P)$.*
It follows from the semantics of biprocess that if $P \xrightarrow{}Q$ for some biprocesses $P,Q$, then $\textnormal{fst}(P) \xrightarrow{}\textnormal{fst}(Q)$ and $\textnormal{snd}(P)\xrightarrow{}\textnormal{snd}(Q)$. However, reductions in $\textnormal{fst}(P)$ or $\textnormal{snd}(P)$ do not necessarily imply biprocess reductions in $P$; that is, there exist biprocesses $P$ such that $\textnormal{fst}(P) \xrightarrow{}\textnormal{fst}(Q)$, but there is no such reduction $P \xrightarrow{}Q$, and symmetrically for $\textnormal{snd}(P)$. For example, consider the biprocess $P = \overline{\textnormal{diff}[a,c]}\langle n\rangle \mid a(x)$, we have $\textnormal{fst}(P) \xrightarrow{}0$, but there is no reduction $P \xrightarrow{}0$. Blanchet, Abadi & Fournet (**Blanchet04?**; **BlanchetJLAP07?**) have shown that a biprocess $P$ satisfies observational equivalence when reductions in $\textnormal{fst}(P)$ or $\textnormal{snd}(P)$ imply reductions in $P$. This proof technique is formalised using the notion of *uniformity*.
**Definition 3** (Uniform). *A biprocess $P$ is *uniform* if for all processes $Q_1$ such that $\textnormal{fst}(P) \xrightarrow{}Q_1$, then $P \xrightarrow{}Q$ for some biprocess $Q$, where $\textnormal{fst}(Q) \equiv Q_1$, and symmetrically for $\textnormal{snd}(P) \xrightarrow{}Q_2$.*
**Definition 4** (Strong uniformity). *A closed biprocess $P$ *satisfies strong uniformity* if for all plain evaluation contexts $C$ and biprocesses $Q$ such that $C[P] \xrightarrow{}^*\equiv Q$, then $Q$ is uniform.*
**Theorem 1** (Strong uniformity implies equivalence (**BlanchetJLAP07?**)). *Given a closed biprocess $P$, if $P$ satisfies strong uniformity, then $P$ satisfies observational equivalence.*
# Formalising DAA protocols
The concept of Direct Anonymous Attestation was defined by Brickell, Camenisch & Chen (**Chen04:RSA-DAA?**), and a historical account of its development is presented in (**Chen04:DAA-in-context?**). A Direct Anonymous Attestation scheme allows remote authentication of trusted platforms, and comprises of five algorithms, each of which will now be discussed.
#### Setup.
The setup algorithm is primarily used by the issuer to construct a public key pair $sk_I,\mathsf{pk}(sk_I)$, and the public part $\mathsf{pk}(sk_I)$ is published. In addition, the setup algorithm may define implementation specific parameters.
#### Join.
The join algorithm is run between a trusted platform and an issuer for the purpose of obtaining group membership. The algorithm assumes that the trusted platform and issuer have established a one-way authenticated channel, that is, the issuer is assured to be communicating with a host and TPM. The definition of DAA does not mandate a particular authentication mechanism, although the Trusted Computing Group recommend encrypting every message sent by the issuer under the TPM’s endorsement key (**TPMspec?**). (Although, as demonstrated by the RSA-based DAA scheme, lighter solutions are possible.) On successful completion of the join algorithm, the issuer grants the trusted platform with an attestation identity credential $\texttt{cre}$ based upon a secret $\texttt{tsk}$ known only by the TPM.
#### Sign.
The sign algorithm is executed by a trusted platform to produce a signature $\sigma$, based upon an attestation identity credential $\texttt{cre}$ and secret $\texttt{tsk}$, which asserts group membership and therefore trusted platform status. The algorithm takes as input a message $m$ and a basename $\texttt{bsn}$ (which is used to control linkability between signatures). If $\texttt{bsn}= {\perp}$, then signatures should be unlinkable; otherwise, signatures produced by the same signer and based upon the same basename can be linked.
#### Verify.
The verification algorithm is used by a verifier to check the validity of a signature. The algorithm takes as input a set of secret keys $\texttt{ROGUE}_{\texttt{tsk}}$, which are known to have been successfully extracted from compromised TPMs (see Tarnovsky (**Tarnovsky10:TPM-extract-key?**) for further details on key extraction), allowing the identification of rogue platforms. The methodology used to build $\texttt{ROGUE}_{\texttt{tsk}}$ is not defined by DAA.
#### Link.
The link algorithm is used by a verifier to check if two valid signatures $\sigma$, $\sigma'$ are linked, that is, signed using the same basename $\texttt{bsn}$ and secret $\texttt{tsk}$.
The inputs and outputs of these algorithms are explicitly summarised in Table
**Definition 1** (Direct Anonymous Attestation process specification). *A *Direct Anonymous Attestation process specification* is a tuple of processes $\langle \sf{Join}, \sf{Sign}\rangle$.*
The signer (or trusted platform) is able to execute arbitrarily many instances of the join, and sign, algorithms, to become a member of a group and subsequently produce signatures as a group member. This behaviour is captured by the $\sf{Signer}$ process modelled below. The join and sign algorithms are modelled by the processes $\sf{Join}$ and $\sf{Sign}$, which are expected to behave like services; that is, they can be called by, and return results to, the $\sf{Signer}$ process. The communication between the $\sf{Signer}$ and $\sf{Join}$/$\sf{Sign}$ processes is achieved using private communication over channels $a_j,a'_j,a_s,a'_s$. In essence, the private channel communication models the internal bus used by computer systems for communication between the host and TPM.
This chapter focuses on user-controlled anonymity and hence it is sufficient to assume the processes $\sf{Join}$ and $\sf{Sign}$ are initiated by input on channels $a_j$ and $a_s$; and similarly, output results on channels $a'_j$ and $a'_s$. Intuitively, it follows that some processes not satisfying these conditions will satisfy our definition of user-controlled anonymity. In fact, the Direct Anonymous Attestation process specification $\langle 0, 0 \rangle$ will satisfy our definition. We tolerate this limitations here, and in future work we will consider a complete definition of the DAA properties, including correctness and user-controlled traceability. The correctness property will exclude degenerate process specifications such as $\langle 0, 0 \rangle$. Similar considerations are made in the literature, for example, in definitions of vote privacy for electronic voting (**KR05:vote-privacy?**; **DKR06?**; **DKR08?**; **DKR10?**) and privacy for vehicular ad-hoc networks (**Delaune10:Vanets?**). $$\begin{array}{lcl}
\sf{Signer}
&=& \nu\,a_j.\nu\,a'_j.\nu\,a_s.\nu\,a'_s\mathrel{.} (\,( {!\sf{Join}} ) \mid ({!\sf{Sign}} ) \mid (\nu\,\texttt{cnt}.\nu\,\texttt{DAASeed}.\nu\,sk_{M}.\overline{c}\langle\mathsf{pk}(sk_M)\rangle.\\
% && \qquad \textrm{\sout{$\new{\DAASeed}.\new{\cnt}.$}}\\
&& \qquad!c(w_{\mathsf{params }}).\overline{a_j}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{w_{\mathsf{params }},\texttt{DAASeed},\texttt{cnt},sk_{M}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.a'_j(x).\\
&& \qquad \textnormal{let } x_{\mathsf{cre }}=\pi_{1}(x) \textnormal{ in }\textnormal{let } x_{\texttt{tsk}}=\pi_{2}(x) \textnormal{ in }(\\
&& \qquad\qquad!c(y).\textnormal{let } y_{\mathsf{bsn }}=\pi_{1}(y) \textnormal{ in }\textnormal{let } y_{\mathsf{msg }}=\pi_{2}(y) \textnormal{ in }\\
&& \qquad\qquad\overline{a_s}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{w_{\mathsf{params }},y_{\mathsf{bsn }},y_{\mathsf{msg }},x_{\mathsf{cre }},x_{\texttt{tsk}}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.a'_s(z).\overline{c}\langle z\rangle\\
% && \qquad\qquad\textrm{\sout{$\Ifthen{\ybsn}{\perp}$}}\\
% && \qquad\qquad\qquad\textrm{\sout{$\new{\bsn}.\Out[a_s]{\tuple{\wparams,\bsn,\ymsg,\xcre,\xtsk}}.\In[a'_s]{z}.\Out{z}$}}\\
% && \qquad\qquad\textrm{\sout{$\Else$}}\\
% && \qquad\qquad\qquad\textrm{\sout{$\Out[a_s]{\tuple{\wparams,\ybsn,\ymsg,\xcre,\xtsk}}.\In[a'_s]{z}.\Out{z}$}}\\
&& \qquad)\\
&& ))
\end{array}$$ The process $\sf{Signer}$ instantiates arbitrarily many instances of the $\sf{Join}$ and $\sf{Sign}$ processes. The restricted channel names $a_j$, $a'_j$ are introduced to ensure communication between the $\sf{Signer}$ and $\sf{Join}$ processes is private; similarly, names $a_s$, $a'_s$ ensure private communication between the $\sf{Signer}$ and $\sf{Sign}$ processes. The bound name $\texttt{cnt}$ is a counter value selected by the host. The bound name $\texttt{DAASeed}$ represents the TPM’s internal secret and $sk_{M}$ represents the TPM’s endorsement key (these values are defined during manufacture (**TPMspec?**)). The public part of the endorsement key is published by the $\sf{Signer}$ process. The remainder of the $\sf{Signer}$ process models a signer’s ability to execute arbitrarily many instances of the join and sign algorithms. The $\sf{Signer}$ process must first input system parameters $w_{\mathsf{params }}$, provided by the issuer. The $\sf{Join}$ process is assumed to act like a service and listens for input on channel $a_j$. It follows, that the $\sf{Signer}$ process can invoke the service by message output $\overline{a_j}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{w_{\mathsf{params }},\texttt{DAASeed},\texttt{cnt},w_{\mathsf{ek }}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle$, where $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{w_{\mathsf{params }},\texttt{DAASeed},\texttt{cnt},w_{\mathsf{ek }}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ models the join algorithm’s parameters. The $\sf{Join}$ process is assumed to output results on channel $a'_j$, and this response can be received by the $\sf{Signer}$ process using message input $a'_j(x)$; the result is bound to the variable $x$, and is expected to consist of a pair $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{x_{\mathsf{cre }},x_{\texttt{tsk}}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ representing the attestation identity credential and TPM’s secret. The interaction between the $\sf{Sign}$ and $\sf{Signer}$ processes is similar. The $\sf{Signer}$ process first inputs a variable $y$ which is expected to be a pair representing the verifier’s basename $y_{\mathsf{bsn }}$ and a message $y_{\mathsf{msg }}$. The invocation of the sign algorithm by the signer is modelled by the message output $\overline{a_s}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{w_{\mathsf{params }},y_{\mathsf{bsn }},y_{\mathsf{msg }},x_{\mathsf{cre }},x_{\texttt{tsk}}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle$, where $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{w_{\mathsf{params }},y_{\mathsf{bsn }},y_{\mathsf{msg }},x_{\mathsf{cre }},x_{\texttt{tsk}}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ represents the algorithm’s parameters. The sign algorithm is expected to output a signature which can be sent to a verifier, in the $\sf{Signer}$ process this signature is received from the $\sf{Sign}$ process by message input $a'_s(z)$ and the variable $z$ representing the signature is immediately output.
# Security definition: User-controlled anonymity
Informally, the notion of user-controlled anonymity asserts that given two honest signers $\mathcal{A}$ and $\mathcal{B}$, an adversary cannot distinguish between a situation in which $\mathcal{A}$ signs a message, from another one in which $\mathcal{B}$ signs a message. Based upon Brickell, Chen & Li (**Chen08:DAA-security-preprint?**; **Chen09:DAA-security?**) we present the following security definition.
#### Initial:
The adversary constructs the public key pair $sk_I,\mathsf{pk}(sk_I)$ and publishes the public part $\mathsf{pk}(sk_I)$ for the signers. The adversary also publishes any additional parameters.
#### Phase 1:
The adversary makes the following requests to signers $\mathcal{A}$ and $\mathcal{B}$:
- Join. The signer executes the join algorithm to create $\texttt{cre}$ and $\texttt{tsk}$. The adversary, as the issuer, learns $\texttt{cre}$ but typically not $\texttt{tsk}$.
- Sign. The adversary submits a basename $\texttt{bsn}$ and a message $m$. The signer runs the sign algorithm and returns the signature to the adversary.
At the end of phase 1, both signers are required to have run the join algorithm at least once.
#### Phase 2 (Challenge):
The adversary submits a message $m$ and a basename `bsn` to the signers, with the restriction that the basename has not been previously used if $\texttt{bsn}\not= {\perp}$. Each signer produces a signature on the message and returns it to the adversary.
#### Phase 3:
The adversary continues to probe the signers with join and sign requests, but is explicitly forbidden to use the basename used in phase 2 if $\texttt{bsn}\not= {\perp}$.
#### Result:
The protocol satisfies user-controlled anonymity if the adversary cannot distinguish between the two signatures output during the challenge.
Formally, this definition can be modelled as an observational equivalence (Definition
**Definition 1** (User-controlled anonymity). *Given a Direct Anonymous Attestation process specification $\langle \sf{Join}, \sf{Sign}\rangle$, *user-controlled anonymity* is satisfied if the augmented Direct Anonymous Attestation biprocess ${\sf DAA}$ satisfies observational equivalence.*
The definition has been used to analyse user-controlled anonymity in RSA-based DAA.
# Case study: RSA-based DAA
The first concrete Direct Anonymous Attestation scheme was introduced by Brickell, Camenisch & Chen (**Chen04:RSA-DAA?**) and is based on RSA.
## Primitives and building blocks
We first recall the details of Camenisch-Lysyanskaya (CL) signatures (**CamenischLysyanskaya03?**; **Lysyanskaya02?**), which form the foundations of RSA-based DAA, and introduce some notational conventions.
#### Signature scheme.
A CL signature is denoted $\mathsf{clsign}(x_{\mathsf{sk }},x_{\mathsf{prime }},x_{\mathsf{rand }},x_{\mathsf{msg }})$, where $x_{\mathsf{sk }}$ is the secret key, $x_{\mathsf{prime }}$ is a random prime, $x_{\mathsf{rand }}$ is a nonce, and $x_{\mathsf{msg }}$ is a message. The prime and nonce components can be derived from a signature. Verification is standard given a signature, message, and public key, that is, $\mathsf{checkclsign}(\allowbreak\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{msg }},\mathsf{clsign}(x_{\mathsf{sk }},x_{\mathsf{prime }},x_{\mathsf{rand }},\allowbreak x_{\mathsf{msg }})) = \mathsf{accept}$.
#### Signature scheme for committed values.
The scheme supports signatures on committed values. Given the public part of a signing key $\mathsf{pk}(x_{\mathsf{sk }})$, a message $x_{\mathsf{csk }}$, and commitment factor $x_{\mathsf{cf }}$, the committed value is $U = \mathsf{clcommit}(\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{cf }},x_{\mathsf{csk }})$ and the associated signature is $\mathsf{clsign}(x_{\mathsf{sk }},y_{\mathsf{prime }},y_{\mathsf{rand }},U)$ for some prime $y_{\mathsf{prime }}$ and random $y_{\mathsf{rand }}$. This signature can be opened to recover $\sigma = \mathsf{clopen}(\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{cf }},\mathsf{clsign}(x_{\mathsf{sk }},y_{\mathsf{prime }},y_{\mathsf{rand }},U)) = \mathsf{clsign}(x_{\mathsf{sk }},y_{\mathsf{prime }},y_{\mathsf{rand }}\circ x_{\mathsf{cf }},x_{\mathsf{csk }})$, that is, the signature on $x_{\mathsf{csk }}$. (A proof should also be provided to demonstrate that $\sigma$ does not contain a covert channel – such details will be omitted from the model presented here – see Appendix
xx̄xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx̄x̄ $\mathsf{dec}(x_{\mathsf{sk }},\mathsf{penc}(\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{rand }},x_{\mathsf{plain }})) = x_{\mathsf{plain }}$
$\mathsf{clgetprime}(\mathsf{clsign}(x_{\mathsf{sk }},x_{\mathsf{prime }},x_{\mathsf{rand }},x_{\mathsf{msg }})) = x_{\mathsf{prime }}$
$\mathsf{clgetnonce}(\mathsf{clsign}(x_{\mathsf{sk }},x_{\mathsf{prime }},x_{\mathsf{rand }},x_{\mathsf{msg }})) = x_{\mathsf{rand }}$
$\mathsf{checkclsign}(\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{msg }},\mathsf{clsign}(x_{\mathsf{sk }},x_{\mathsf{prime }},x_{\mathsf{rand }},x_{\mathsf{msg }})) = \mathsf{accept}$
$\mathsf{open}(x_{\mathsf{rand }},\mathsf{commit}(x_{\mathsf{rand }},x_{\mathsf{plain }})) = x_{\mathsf{plain }}$
$\mathsf{clopen}(x,x_{\mathsf{rand }},\mathsf{clcommit}(x,x_{\mathsf{rand }},x_{\mathsf{plain }})) = x_{\mathsf{plain }}$
$\mathsf{clopen}(\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{rand }},\mathsf{clsign}(x_{\mathsf{sk }},y_{\mathsf{prime }},y_{\mathsf{rand }},\mathsf{clcommit}(\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{rand }},x_{\mathsf{msg }})))$
$\mathrel{=}\mathsf{clsign}(x_{\mathsf{sk }},y_{\mathsf{prime }},y_{\mathsf{rand }}\circ x_{\mathsf{rand }},x_{\mathsf{msg }})$
A signature proof of knowledge is encoded in the form $\mathsf{spk}(F,U,V)$, where $F$ is a constant declaring the particular proof in use, $U$ denotes the witness (or private component) of a signature of knowledge, and $V$ defines the public parameters and message being signed. The function $\mathsf{checkspk}$ is used to verify a signature and we define the following equations.
xx̄x̄ $\mathsf{checkspk}(\mathsf{F}_{\mathsf{join}},V,\mathsf{spk}(\mathsf{F}_{\mathsf{join}},(x_{\texttt{tsk}},x_{\mathsf{cf }}),V)) = \mathsf{accept}$
where $V = (x_{\mathsf{\zeta_I }},x_{\mathsf{pk }},\mathsf{commit}(x_{\texttt{tsk}},x_{\mathsf{\zeta_I }}),\mathsf{clcommit}(x_{\mathsf{pk }},x_{\mathsf{cf }},x_{\texttt{tsk}}) ,x_{\mathsf{msg }})$
$\mathsf{checkspk}(\mathsf{F}_{\mathsf{sign}},V,\mathsf{spk}(\mathsf{F}_{\mathsf{sign}},(x_{\texttt{tsk}},x_{\mathsf{cf }}),V)) = \mathsf{accept}$
where $V = (x_{\mathsf{\zeta }}, \mathsf{pk}(x_{\mathsf{sk }}), \mathsf{commit}(x_{\texttt{tsk}},x_{\mathsf{\zeta }}),$
$\mathsf{clcommit}(\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{cf }},\mathsf{clsign}(x_{\mathsf{sk }},x_{\mathsf{prime }},x_{\mathsf{rand }},x_{\texttt{tsk}})), x_{\mathsf{msg }})$
The first equation is used to verify the signature proof of knowledge produced by the trusted platform during the join algorithm and the second is used by a trusted platform during the sign algorithm to assert group membership.
## Model in applied pi
The RSA-based DAA process specification is presented in Definition
**Theorem 1**. *The RSA-based Direct Anonymous Attestation process specification $\langle \sf{Join}_{RSA}, \sf{Sign}_{RSA} \rangle$ does not satisfy user-controlled anonymity.*
Formally, Theorem
**The lack of formal security analysis prior to system deployment can be partially attributed to the absence of suitable tools. This part develops new procedures for the automated analysis of observational equivalence.**
# untitled section
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 137, column 1): unexpected \vskip expecting \end{document} \end{overview} ^`
``` latex
\chapter[Observational equivalence and barriers]
{Observational equivalence and barriers\symbolfootnotemark}\label{chap:obs}
\symbolfootnotetext{This chapter is partly based upon~\cite{Smyth08:Obs} which introduces the
fundamental notion of swapping at synchronisation points and considered a preliminary analysis of privacy in FOO. The software associated with this chapter is available online: \url{http://www.bensmyth.com/proswapper.php}.}
%\symbolfootnotetext{This chapter is partly based upon~\cite{Smyth08:Obs,Smyth10:Obs,Smyth10:ObsA}. The
%fundamental notion of swapping at synchronisation points was introduced in~\cite{Smyth08:Obs}.
%This result was refined and generalised in~\cite{Smyth10:Obs}, a preliminary version of which appears
%in Sections~\ref{sec:obs:sync} and~\ref{sec:obs:auto}. The analysis of privacy in FOO (Section~\ref{sec:obs:FOO}) was first considered
%in~\cite{Smyth08:Obs}, and automated support was provided by~\cite{Smyth10:ObsA}. The software associated with this chapter is available online: \url{http://www.bensmyth.com/proswapper.php}.}
%The notion of \emph{barrier synchronisation} is formalised with
%respect to processes and a methodology for automatically verifying
%equivalence properties is introduced. The study of barrier
%synchronisation in relation to equivalence is particularly
%interesting because certain equivalence properties can only be
%realised under specific synchronisation assumptions. For example,
%privacy preserving protocols typically require
%the existence of at least two honest participants whom synchronise
%prior to performing certain actions. This particular pre-requisite
%can be observed in domains including: electronic voting, Direct
%Anonymous Attestation, and anonymity networks.
\begin{overview}
A procedure for the automated analysis of observational equivalence is delivered.
In addition, the notion of barrier synchronisation is characterised for
processes. The study of barrier
synchronisation in relation to equivalence is particularly
interesting because certain equivalence properties can only be
realised under specific synchronisation assumptions.
In particular, privacy preserving protocols -- including electronic
voting schemes, vehicular ad-hoc networking protocols, and
anonymity networks -- make such assumptions.
The results have been implemented in the tool \emph{ProSwapper},
an extension to ProVerif, and the applicability of this research is demonstrated by
analysing vote privacy in electronic voting protocols
and privacy in vehicular ad-hoc networks.
\end{overview}
%Barrier synchronisation is
%an important building block for protocol analysis because certain
%equivalence properties can only be realised if processes
%synchronise their actions in a specific manner. For example,
%privacy preserving protocols typically require
%the existence of at least two honest participants whom synchronise
%prior to performing certain actions. This particular pre-requisite
%can be observed in domains including: electronic voting, Direct
%Anonymous Attestation, and anonymity networks.
\noindent Blanchet, Abadi \& Fournet~\cite{Blanchet04,BlanchetJLAP07}
%have developed automatic reasoning techniques which
focus on
equivalences $P \sim Q$ in which processes $P$ and $Q$ share the same
structure and differ only in the choice of terms.
Their work introduces the notion of \emph{strong uniformity} (see Section~\ref{sec:obs:proverif}),
a sufficient condition for observational equivalence, that has been implemented in
ProVerif, an automatic analysis tool for protocols written in the applied
pi calculus. Strong uniformity is a sufficient condition for observational equivalence, but it is not necessary.
This precludes the automated analysis of certain equivalence properties, as a simple example will demonstrate.
\begin{example}\label{ex:obs}
The biprocess $P = \Out{\diff{m}{n}}\mid\Out{\diff{n}{m}}$ is observationally equivalent because $\fst{P}\equiv\snd{P}$. However, the plain evaluation context
\[
C[\_] = \_ \mid \In{x}.\Letinelse{y}{\Eq{x}{m}}{0}0
\]
is such that $C[P] \reduc Q$, where $Q = \Out{\diff{n}{m}}\mid\Letinelse{y}{\Eq{\diff{m}{n}}{m}}{0}0$ and $\fst{Q} \reduc \Out{n}$; but, there is no biprocess $R$ such that $Q \reduc R$ and $\fst{R} \equiv \Out{n}$, because $\fst{\Eq{\diff{m}{n}}{m}}\Downarrow m$, but there is no term $M_2$ such that $\snd{\Eq{\allowbreak\diff{m}{n}}{m}}\Downarrow M_2$. It follows immediately that $P$ does not satisfy Definition~\ref{def:proverif:strong-uniformity}, that is, it cannot be shown to satisfy observational equivalence using Theorem~\ref{theorem:Bruno}. Similarly, the biprocess $(\Ifthenelse{a}{\diff{a}{c}}{\Out{c}}\nill) \mid (\Ifthenelse{b}{\diff{c}{b}}{\Out{c}}\nill)$ satisfies observational equivalence but does not satisfy strong uniformity.
\end{example}
Barrier synchronisation~\cite{Brooks86:Barriers, Hensgen88:Barriers, Arenstorf89:Barriers, Lubachevsky89:Barriers} is a concept to coordinate the actions
performed by concurrently executing processes. More precisely,
the mechanism ensures that a process will block, when a barrier
is encountered, until all other processes executing in parallel
reach this barrier. Capturing such synchronisation is an important
building block
for protocol analysis because certain security properties can
only be realised if processes synchronise their actions in a
specific manner. For example, privacy preserving protocols
typically require the existence of at least two honest
participants that synchronise prior to performing critical actions.
This particular prerequisite can be observed in domains including:
electronic voting~\cite{DKR08,Backes08:Voting},
%Direct Anonymous Attestation~\cite{Chen04:RSA-DAA,Chen09:DAA-security} (see also Chapter~\ref{chap:DAA}),
vehicular ad-hoc networks~\cite{Delaune10:Vanets},
and anonymity networks~\cite{RR98,Pfitzmann01,Chothia06:Mute}.
Resolving the difficulties apparent in Example~\ref{ex:obs}
is relatively straightforward: the biprocess $P' = \Out{\diff{m}{m}}\mid\Out{\diff{n}{n}}$
can trivially be shown to satisfy observational equivalence using
strong uniformity as a proof technique, and since
$\fst{P} \equiv \fst{P'}$ and $\snd{P} \equiv \snd{P'}$, it
follows that $P$ satisfies observational equivalence because
observational equivalence is closed under structural equivalence.
However, this technique cannot be applied to more complicated examples
in which barriers occur.
\begin{example} \label{ex:newExample}
Consider the biprocess
$$
P = \Out{m}.\sstage{1}\Out{\diff{m}{n}} \mid \sstage{1}\Out{\diff{n}{m}}
$$
in which $\sstage{1}$ represents a barrier synchronisation. Intuitively,
there is no structurally equivalent biprocess $P'$ satisfying strong
uniformity, but nevertheless, barrier synchronisation ensures
indistinguishability between $\fst{P}$ and $\snd{P}$. (This example
will be elaborated upon once we formalise barrier synchronisation.)
\end{example}
This chapter introduces a strictly weaker notion of uniformity which can be used to automatically
reason with observational equivalence between processes containing barriers.
%\textcolor{red}{\bf They also study a different notion of synchronisation called
%\emph{stages}~\cite[\S8]{BlanchetJLAP07}.}
\contribution
The contribution of this chapter is threefold. Firstly,
the process syntax (Section~\ref{sec:obs:proverif}) is extended
to capture barriers and it is shown
how the semantic behaviour of barriers can be encoded in the
standard ProVerif model. Although the formalisation of barriers is only
an encoding, it considerably simplifies the modelling process and, moreover,
forms the foundation for our automated analysis technique.
Secondly, a methodology for automatic analysis of equivalence properties
is developed, based upon~\cite{Blanchet04,BlanchetJLAP07}. This approach avoids the
limitations of~\cite{Blanchet04,BlanchetJLAP07} by \emph{swapping}
data at synchronisation points. For example, in Example~\ref{ex:newExample}
swapping data between the two
sides of the parallel composition is permitted at synchronisation;
in essence, it is therefore sufficient to prove the equivalence of the biprocess
$P' = \Out{m}.\sstage{1}.\Out{\diff{m}{m}}\mid\sstage{1}\Out{\diff{n}{n}}$,
which is trivially true because $\fst{P'}=\snd{P'}$.
Finally, automated support is provided by defining a static
compiler which encodes barrier synchronisation and swapping
using private channel communication. The compiler is designed to compute
an approximation of a process's observable behaviour, and hence,
if ProVerif can show observational equivalence between a pair of
compiled processes,
then the original pair of processes satisfies observational
equivalence. The compiler has been implemented as a tool called \emph{ProSwapper}. Furthermore, the analysis of vote privacy in electronic voting protocols
and privacy in vehicular ad-hoc networks demonstrate the applicability of this work.
\limitations
Proving soundness of the proof technique is ongoing work. Although some confidence may be provided by the tool's adoption within the research community (for example, \cite{Backes08:Voting,Delaune10:Vanets}), this is no substitute for a thorough proof.
%...... will be discussed in Section~\ref{sec:further:obs}.
\structure %\sout{Section~\ref{sec:obs:proverif} recalls the variant of the applied pi calculus introduced by~XX.}
Section~\ref{sec:obs:sync} extends the process syntax of Section~\ref{sec:obs:proverif} to capture barrier
synchronisation and provides mechanical reasoning techniques
for such processes. Section~\ref{sec:obs:auto} defines a methodology
for automatic analysis of equivalence properties.
In Section~\ref{sec:obs:example} the applicability of this work
is demonstrated by presenting an automated analysis of
privacy in the electronic voting protocol FOO and in
Appendix~\ref{app:obs:src} privacy in vehicular ad-hoc networks is considered;
the technique's adoption by the research community will also be discussed.
%The applicability of this work is demonstrated in Section~\ref{sec:obs:example}
%by presenting the first automated analysis of privacy in the
%electronic voting protocol FOO and highlighting the techniques
%adoption by the academic community.
%In addition, barrier synchronisation
%is used in Chapter~\ref{chap:DAA} to .......
%Limitations of the approach
%are discussed in Section~\ref{sec:further:obs}.
Finally, a summary is presented
in Section~\ref{sec:obs:summary}.
%The notion of \emph{barrier synchronisation} is formalised with
%respect to processes
%A methology for capturing barrier synchronisation is introduced. This is a particularly important mechanism for privacy preserving protocols, because
%Reasoning with equivalence properties has proven to be
%This chapter explicitly focuses on
%equivalence properties that can only be realised if participants synchronise
%their actions in a specific manner.
%Some equivalence properties can only be realised if processes %synchronise their actions in a specific manner. For example,
%\input{obs-prelims}
\newcommand{\ch}{{\sf c}}
\newcommand{\Ch}{{\sf a}}
```
# Processes with barriers
A notion of synchronisation, called *stages*, has previously been studied in the applied pi calculus by Blanchet, Abadi & Fournet (**BlanchetJLAP07?**); however, stages are insufficient for our purposes. In the spirit of (**BlanchetEquiv07?**; **DRS08?**)(**BlanchetJLAP07?**), we proceed by allowing processes to be annotated with *barriers*. Barriers are written $t\textnormal{::}\,$ and may appear before a process $P$, where $t\in\mathbb{N}$. Intuitively, $t\textnormal{::}\,P$ blocks $P$ until all processes running in parallel are ready to synchronise at barrier $t$. For example, the process $1\textnormal{::}\,\overline{c}\langle k\rangle.2\textnormal{::}\,\overline{c}\langle m\rangle\mid2\textnormal{::}\,\overline{c}\langle n\rangle$ can only output $n$ after synchronisation at barrier $t=2$. It follows that the process cannot output $n$ without having previously output $k$; this is in direct contrast with (**BlanchetJLAP07?**), which permits the output of $n$ without having previously observed an output of $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 $c(x).\textnormal{if } x=k \textnormal{ then } 1\textnormal{::}\,\overline{c}\langle m\rangle \textnormal{ else }\overline{c}\langle n\rangle\mid1\textnormal{::}\,\overline{c}\langle s\rangle$ may evolve to $\overline{c}\langle n\rangle\mid1\textnormal{::}\,\overline{c}\langle s\rangle$ 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 $t\textnormal{::}\,P$ the process $P$ also blocks if there are any barriers $t'$ such that $t'[sec:obs:auto].
The *barrier elimination function* (Definition 1) takes processes containing barriers and replaces each barrier with a message output followed by a message input[^2]. By ensuring that the communication channels are fresh private names and through the introduction of a *synchronisation process*, the semantics of SECTION BLAHbarriers can be captured in the standard ProVerif model.
**Definition 1** (Barrier elimination function). *The *barrier elimination function* $\delta$ maps an infinite sequence of channel names ${\Ch}$ and a process $P$ to another process, the function is recursively defined as follows: $$\begin{array}{lcl}
\delta(\ch,\;0) &=& 0\\
\delta(\ch,\;!Q) &=& !Q \\
\delta(\ch,\;\nu\,n.Q) &=& \nu\,n.\delta(\ch,\;Q)\\
\delta(\ch,\;M(x).Q) &=& M(x).\delta(\ch,\;Q)\\
\delta(\ch,\;\overline{M}\langle N\rangle.Q) &=& \overline{M}\langle N\rangle.\delta(\ch,\;Q)\\
\delta(\ch,\;t\textnormal{::}\,Q) &=& \overline{a'}\langle a'\rangle.a''(y).\delta(\mathsf{tail}(\mathsf{tail}(\ch)),\;Q)\\
&&\textrm{where $a' = \mathsf{head}(\ch)$, $a'' = \mathsf{head}(\mathsf{tail}(\ch))$ and $y\not\in\textnormal{fv}(Q)$}\\
\delta(\ch,\;\textnormal{let } x=D \textnormal{ in } Q \textnormal{ else }R) &=& \textnormal{let } x=D \textnormal{ in } \delta(\mathsf{odd}(\ch),\;Q) \textnormal{ else }\delta(\mathsf{even}(\ch),\;R)\\
% && \qquad\quad\;\; \Else \compFuncI{\even{\ch}}{R}\\
\delta(\ch,\;Q \mid R) &=& \delta(\mathsf{odd}(\ch),\;Q) \mid \delta(\mathsf{even}(\ch),\;R)
\end{array}$$*
Intuitively, processes which synchronise at a particular barrier all output a message on a private channel and these messages are received by the synchronisation process; once all messages have been sent/received, the synchronisation process sends replies to each of the processes and hence processes may proceed. For example, in the case where there are $n$ processes containing a barrier $t$, the synchronisation process will receive precisely $n$ inputs and will then send exactly $n$ responses; prior to the responses being sent, the processes are awaiting input on a private channel and hence block. The application of the barrier elimination function will be demonstrated in Example 1; first, we study how to control the synchronisation. To ensure that the correct pair of channel names are used for synchronisation we first define the function $\omega$ which captures the set of channel names introduced for synchronisation (Definition 2).
The functions $\omega$, $\delta$ are logically similar and separation has only been introduced for readability. The function $\omega$ builds a set of triples $(t,a',a'')$, where $t\in\mathbb{N}$ represents a barrier synchronisation and $a'$ (respectively $a''$) are the output (respectively input) channels used by $\delta$ for synchronisation at barrier $t$.
**Definition 2** (Synchronisation channels). *Given a process $P$ and an infinite sequence of channel names ${\Ch}$, the set of *synchronisation channels* is $\omega({\Ch},\;P)$, where: $$\begin{array}{lcl}
\omega(\ch,\;0) &=& \emptyset\\
\omega(\ch,\;!Q) &=& \emptyset\\
\omega(\ch,\;\nu\,n.Q) &=& \omega(\ch,\;Q)\\
\omega(\ch,\;M(x).Q) &=& \omega(\ch,\;Q)\\
\omega(\ch,\;\overline{M}\langle N\rangle.Q) &=& \omega(\ch,\;Q)\\
\omega(\ch,\;t\textnormal{::}\,Q) &=& \{(t,a',a'')\} \cup \omega(\mathsf{tail}(\mathsf{tail}(\ch)),\;Q)\\
&& \textrm{where $a' = \mathsf{head}(\ch)$ and $a'' = \mathsf{head}(\mathsf{tail}(\ch))$}\\
\omega(\ch,\;\textnormal{let } x=D \textnormal{ in } Q \textnormal{ else }R) &=& \omega(\mathsf{odd}(\ch),\;Q) \cup \omega(\mathsf{even}(\ch),\;R)\\
\omega(\ch,\;Q \mid R) &=& \omega(\mathsf{odd}(\ch),\;Q) \cup \omega(\mathsf{even}(\ch),\;R)
\end{array}$$*
We introduce *communication* processes, defined by the grammar $R ::= \epsilon \mid u(x) \mid \overline{u}\langle M\rangle \mid R.R'$, such that $\epsilon.R = R$. We omit $R$ in $u(x).R$ and $\overline{u}\langle M\rangle.R$ when it is $\epsilon$. Given communication processes, synchronisation is controlled by a synchronisation process.
**Definition 3** (Synchronisation process). *Given a process $P$ and an infinite sequence of channel names ${\Ch}$, the *synchronisation process* is $\chi({\Ch},P) = \hat{\chi}(0,\;\epsilon,\;\omega({\Ch},\;P))$, where for all integers $t$, communication processes $R$ and sets of triples $S$, we have: $$\hat{\chi}(t,\;R,\;S) =
\left\{\begin{array}{lcl}
R.0 &\quad& \textrm{if $S = \emptyset$}\\[1em]
a'(x).\hat{\chi}(t,\;R.\overline{a''}\langle x\rangle,\;S\backslash\{(t,a',a'')\}) && \textrm{if $(t,a',a'') \in S$}\\
\;\textrm{where $x$ is a fresh variable}\\[1em]
R.\hat{\chi}(t+1,\;\epsilon,\;S) && \textrm{otherwise}
\end{array}\right.$$*
Although communication processes are not standard processes (that is, defined by the grammar in Figure [fig:obs:grammar]), the function $\chi$ always returns a standard process; this process is intended to control synchronisation of a process $P$ in which barriers have been eliminated. Accordingly, $\hat\chi$ is parametrised with $S = \omega({\Ch},\;P)$, that is, the set of triples $(t,a',a'')$ defining the input and output channels used by $\delta$ to eliminate barriers. For each barrier $t$, an input $a'(x)$ is appended to the output, and the function is recursively called with $R.\overline{a''}\langle x\rangle$ and $S\backslash\{(t,a',a'')\}$. Once all barriers under a particular barrier $t$ have been exhausted, the process $R$ is appended to the output and the barriers under the next barrier $t+1$ are processed. It follows, for example, given $n$ processes in parallel all containing a barrier $t$ (and no other barriers), that the synchronisation process is $a_1(x_1).\dots.a_n(x_n).\overline{b_1}\langle x_1\rangle.\dots.\overline{b_n}\langle x_n\rangle$ for some channel names $a_1,\dots,a_n,b_1,\dots,b_n$ and variables $x_1,\dots,x_n$. A more complex example will be considered in Example 1.
Finally, a process defined in the standard ProVerif language can be derived using our compiler (Definition 4) and ProVerif can then be used to automatically reason with processes containing barriers.
**Definition 4** (Synchrony compiler). *The *synchrony compiler* $\Delta$ maps a process $P$ to another process, as follows: $\Delta(P) = \nu\,\tilde{a}.(\delta({\Ch},\;P) \mid \chi({\Ch},P))$, where ${\Ch}$ is an infinite sequence of distinct channel names such that ${\Ch} \cap (\textnormal{fn}(P)\cup\textnormal{bn}(P)) = \emptyset$ and $\tilde{a} = \textnormal{fn}(\delta({\Ch},\;P)) \mathrel{\cap} {\Ch}$.*
The application of our compiler is demonstrated in Example 1.
**Example 1**. *Consider the process $1\textnormal{::}\,\overline{c}\langle k\rangle.2\textnormal{::}\,\overline{c}\langle m\rangle\mid2\textnormal{::}\,\overline{c}\langle n\rangle\mid3\textnormal{::}\,\overline{c}\langle s\rangle$ and let ${\Ch} = (a_1,a_2,\dots)$. We have:*
*XXXXXxX̄XxX̄X̄ $\delta({\Ch},\;P)$$=$$\delta((a_1,a_3,\dots),\;1\textnormal{::}\,\overline{c}\langle k\rangle.2\textnormal{::}\,\overline{c}\langle m\rangle) \mid \delta((a_2,a_4,\dots),\;2\textnormal{::}\,\overline{c}\langle n\rangle\mid3\textnormal{::}\,\overline{c}\langle s\rangle)$
$=$ $\overline{a_1}\langle a_1\rangle.a_3(x).\delta((a_5,a_7,\dots),\;\overline{c}\langle k\rangle.2\textnormal{::}\,\overline{c}\langle m\rangle) \mid$
$\qquad \delta((a_2,a_6,\dots),\;2\textnormal{::}\,\overline{c}\langle n\rangle) \mid \delta((a_4,a_8,\dots),\;3\textnormal{::}\,\overline{c}\langle s\rangle)$
$=$ $\overline{a_1}\langle a_1\rangle.a_3(x).\overline{c}\langle k\rangle.\delta((a_5,a_7,\dots),\;2\textnormal{::}\,\overline{c}\langle m\rangle) \mid$
$\qquad \overline{a_2}\langle a_2\rangle.a_6(y).\delta((a_{10},a_{14},\dots),\;\overline{c}\langle n\rangle) \mid \overline{a_4}\langle a_4\rangle.a_8(z).\delta((a_{12},a_{16},\dots),\;\overline{c}\langle s\rangle)$
$=$ $\overline{a_1}\langle a_1\rangle.a_3(x).\overline{c}\langle k\rangle.\overline{a_5}\langle a_5\rangle.a_7(x').\delta((a_9,a_{11},\dots),\;\overline{c}\langle m\rangle) \mid$
$\qquad \overline{a_2}\langle a_2\rangle.a_6(y).\overline{c}\langle n\rangle\mid\overline{a_4}\langle a_4\rangle.a_8(z).\overline{c}\langle s\rangle$
$=$ $\overline{a_1}\langle a_1\rangle.a_3(x).\overline{c}\langle k\rangle.\overline{a_5}\langle a_5\rangle.a_7(x').\overline{c}\langle m\rangle\mid \overline{a_2}\langle a_2\rangle.a_6(y).\overline{c}\langle n\rangle\mid\overline{a_4}\langle a_4\rangle.a_8(z).\overline{c}\langle s\rangle$*
*XXXXXxX̄XxX̄X̄ $\omega({\Ch},\;P)$ $=$ $\omega((a_1,a_3,\dots),\;1\textnormal{::}\,\overline{c}\langle k\rangle.2\textnormal{::}\,\overline{c}\langle m\rangle) \cup \omega((a_2,a_4,\dots),\;2\textnormal{::}\,\overline{c}\langle n\rangle\mid3\textnormal{::}\,\overline{c}\langle s\rangle)$
$=$ $\{(1,a_1,a_3)\} \cup \omega((a_5,a_7,\dots),\;\overline{c}\langle k\rangle.2\textnormal{::}\,\overline{c}\langle m\rangle) \mathrel{\cup}$
$\qquad \omega((a_2,a_6,\dots),\;2\textnormal{::}\,\overline{c}\langle n\rangle) \cup \omega((a_4,a_8,\dots),\;3\textnormal{::}\,\overline{c}\langle s\rangle)$
$=$ $\{(1,a_1,a_3),(2,a_2,a_6),(3,a_4,a_8)\} \cup \omega((a_5,a_7,\dots),\;2\textnormal{::}\,\overline{c}\langle m\rangle) \mathrel{\cup}$
$\qquad \omega((a_{10},a_{14},\dots),\;\overline{c}\langle n\rangle) \cup\omega((a_{12},a_{16},\dots),\;\overline{c}\langle s\rangle)$
$=$ $\{(1,a_1,a_3),(2,a_5,a_7),(2,a_2,a_6),(3,a_4,a_8)\} \cup \omega((a_9,a_{11},\dots),\;\overline{c}\langle m\rangle)$
$=$ $\{(1,a_1,a_3),(2,a_5,a_7),(2,a_2,a_6),(3,a_4,a_8)\}$*
*XXXXXxX̄XxX̄X̄ $\chi({\Ch},P)$ $=$$\hat{\chi}(1,\;\epsilon,\;\{(1,a_1,a_3),(2,a_5,a_7),(2,a_2,a_6),(3,a_4,a_8)\})$
$=$ $a_1(x).\hat{\chi}(1,\;\overline{a_3}\langle x\rangle,\;\{(2,a_5,a_7),(2,a_2,a_6),(3,a_4,a_8)\})$
$=$ $a_1(x).\overline{a_3}\langle x\rangle.\hat{\chi}(2,\;\epsilon,\;\{(2,a_5,a_7),(2,a_2,a_6),(3,a_4,a_8)\})$
$=$ $a_1(x).\overline{a_3}\langle x\rangle.a_5(x').\hat{\chi}(2,\;\overline{a_7}\langle x'\rangle,\;\{(2,a_2,a_6),(3,a_4,a_8)\})$
$=$ $a_1(x).\overline{a_3}\langle x\rangle.a_5(x').a_2(y).\hat{\chi}(2,\;\overline{a_7}\langle x'\rangle.\overline{a_6}\langle y\rangle,\;\{(3,a_4,a_8)\})$
$=$ $a_1(x).\overline{a_3}\langle x\rangle.a_5(x').a_2(y).\overline{a_7}\langle x'\rangle.\overline{a_6}\langle y\rangle.\hat{\chi}(3,\;\epsilon,\;\{(3,a_4,a_8)\})$
$=$ $a_1(x).\overline{a_3}\langle x\rangle.a_5(x').a_2(y).\overline{a_7}\langle x'\rangle.\overline{a_6}\langle y\rangle.a_4(z).\hat{\chi}(3,\;\overline{a_8}\langle z\rangle,\;\emptyset)$
$=$ $a_1(x).\overline{a_3}\langle x\rangle.a_5(x').a_2(y).\overline{a_7}\langle x'\rangle.\overline{a_6}\langle y\rangle.a_4(z).\overline{a_8}\langle z\rangle$*
*Observe ${\Ch} \cap (\textnormal{fn}(P)\cup\textnormal{bn}(P)) = \emptyset$, $\tilde{a} = a_1,\dots,a_8$ and hence it follows that $\Delta(P)$ is defined as the process: $$\begin{gathered}
\nu\,\tilde{a}.(\overline{a_1}\langle a_1\rangle.a_3(x).\overline{c}\langle k\rangle.\overline{a_5}\langle a_5\rangle.a_7(x').\overline{c}\langle m\rangle\mid \overline{a_2}\langle a_2\rangle.a_6(y).\overline{c}\langle n\rangle\mid\overline{a_4}\langle a_4\rangle.a_8(z).\overline{c}\langle s\rangle \mid \\ a_1(x).\overline{a_3}\langle x\rangle.a_5(x').a_2(y).\overline{a_7}\langle x'\rangle.\overline{a_6}\langle y\rangle.a_4(z).\overline{a_8}\langle z\rangle)
\end{gathered}$$ By inspection we can observe that the process enforces the expected behaviour; that is, the name $k$ must be output before $m$, $n$ and $s$. This can be witnessed by annotating the process with events and analysing using ProVerif (see Appendix
[app:obs:src2]).*
**Theorem 1**. *Given a process $P$, if $\Delta(P)$ is strongly uniform, then $P$ satisfies synchronous observational equivalence.*
The proof of Theorem 1 follows immediately from Theorem [thm:stageElimSwap].
We will now revisit Example [ex:newExample] to show why uniformity is an insufficient proof technique to prove observational equivalence of certain biprocesses containing barriers.
**Example 2**. *Recall the biprocess $P = \overline{c}\langle m\rangle.1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[m,n]\rangle \mid 1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[n,m]\rangle$ from Example
[ex:newExample]. The process $\Delta(P)$ is uniform, but $\Delta(P) \xrightarrow{}^* Q$ where $Q = \overline{c}\langle\textnormal{diff}[m,n]\rangle \mid \overline{c}\langle\textnormal{diff}[n,m]\rangle$, and $Q$ is not uniform.*
**Lemma 1**. *Given biprocess $P$, we have $\textnormal{fst}(P) \sim_T \textnormal{fst}(\Delta(P))$ and $\textnormal{snd}(P) \sim_T \textnormal{snd}(\Delta(P))$.*
**Theorem 2**. *Given biprocess $P$, we have $P$ satisfies synchronous observational equivalence iff $\Delta(P)$ satisfies observational equivalence.*
(1,0)350
# Automated reasoning for equivalence
In this section, the compiler (Section [sec:obs:sync]) is extended to overcome the limitations of strong uniformity as a proof technique. This can be achieved in a static manner by *swapping* data between processes which share the same structure, as will now be demonstrated.
**Example 1**. *Recall the biprocess $P = \overline{c}\langle\textnormal{diff}[m,n]\rangle\mid\overline{c}\langle\textnormal{diff}[n,m]\rangle$ from Example
[ex:obs] and observe that $P = R\sigma \mid R\tau$, where $R = \overline{c}\langle x\rangle$, $\sigma = \{\textnormal{\raisebox{2pt}{\footnotesize $\textnormal{diff}[m,n]$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ and $\tau = \{\textnormal{\raisebox{2pt}{\footnotesize $\textnormal{diff}[n,m]$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$. By extending $\textnormal{diff}$ to substitutions, the process $Q = R\, \textnormal{diff}[\sigma,\tau] \mid R\,\textnormal{diff}[\tau,\sigma]$ is such that $\textnormal{fst}(P) \equiv \textnormal{fst}(Q)$ and $\textnormal{snd}(P) \equiv \textnormal{snd}(Q)$; that is, the biprocess $Q$ preserves the underlying structure of $P$. It follows immediately that $\textnormal{fst}(P) \sim \textnormal{fst}(Q)$ and $\textnormal{snd}(P) \sim \textnormal{snd}(Q)$. Furthermore, $Q$ satisfies strong uniformity and hence $P$ satisfies observational equivalence by transitivity.*
**Example 2**. *Recall the biprocess $P = \overline{c}\langle m\rangle.1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[m,n]\rangle \mid 1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[n,m]\rangle$ from Example
[ex:newExample]~~Intuitively, $P$ can only reduce to $R = 1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[m,n]\rangle \mid 1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[n,m]\rangle$ in one step.~~
and observe that for all biprocesses $R$ such that $P\xrightarrow{}R$, we have $R = 1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[m,n]\rangle \mid 1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[n,m]\rangle$.. Intuitively, $P$ can only reduce to $R = 1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[m,n]\rangle \mid 1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[n,m]\rangle$ in one step. Now consider the biprocess $Q = \overline{c}\langle m\rangle.1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[m,m]\rangle \mid 1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[n,n]\rangle$ which is obtained from $P$ by swapping the second components of the $\textnormal{diff}$ operator. It follows that $\textnormal{fst}(\Delta(P)) \sim \textnormal{fst}(\Delta(Q))$ and $\textnormal{snd}(\Delta(P)) \sim \textnormal{snd}(\Delta(Q))$. Now since $\Delta(Q)$ trivially satisfies strong uniformity, $\Delta(P)$ satisfies observational equivalence by transitivity.
Need to clarify exactly what result we get – we want $P$ satisfies observational equivalence*
**Example 3**. *Recall the process $\Delta(P)$ from Example
[ex:compiler], where $P = 1\textnormal{::}\,\overline{c}\langle k\rangle.2\textnormal{::}\,\overline{c}\langle m\rangle\mid2\textnormal{::}\,\overline{c}\langle n\rangle\mid3\textnormal{::}\,\overline{c}\langle s\rangle$. Let ${\Ch} = (a_1,a_2,\dots)$ and consider the process $Q = \nu\,a_1,\dots,a_8.(\delta'({\Ch},P) \mid \chi({\Ch},P))$. We have $\delta'({\Ch},P)$ defined as follows: $$\begin{gathered}
\overline{a_1}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{c,k,m}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.a_3(x).\overline{\pi_{1}(x)}\langle\pi_{2}(x)\rangle.\overline{a_5}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(x),\pi_{3}(x)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.a_7(x').\overline{\pi_{1}(x')}\langle\pi_{2}(x')\rangle\mathrel{\mid}\\
\overline{a_2}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{c,n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.a_6(y).\overline{\pi_{1}(y)}\langle\pi_{2}(y)\rangle\mid\overline{a_4}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{c,s}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.a_8(z).\overline{\pi_{1}(z)}\langle\pi_{2}(z)\rangle
\end{gathered}$$ In this instance, observe $\Delta(P) \sim Q$, which can be witnessed using ProVerif (see Appendix
[app:obs:src2]).*
**Definition 1** (Barrier elimination function with swapping). *The *barrier elimination function with swapping* $\delta'$ maps an infinite sequence of channel names ${\Ch}$ and a process $P$ to another process, as follows, $\delta'({\Ch},P) = \hat{\delta'}({\Ch},\;\tau,\;P)$ for the substitution $\tau = \{\}$ (that is, the empty substitution), where: $$\begin{array}{lcl}
\hat{\delta'}(\ch,\;\sigma,\;0) &=& 0\\
\hat{\delta'}(\ch,\;\sigma,\;!Q) &=& !Q\sigma \\
\hat{\delta'}(\ch,\;\sigma,\;\nu\,n.Q) &=& \nu\,n.\hat{\delta'}(\ch,\;\{ \textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}} \mid \{\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}}\} \in \sigma \textrm{ and } u \not= n\},\;Q)\\
\hat{\delta'}(\ch,\;\sigma,\;M(x).Q) &=& M\sigma(x).\hat{\delta'}(\ch,\;\{ \textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}} \mid \{\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}}\} \in \sigma \textrm{ and } u \not= x\},\;Q)\\
\hat{\delta'}(\ch,\;\sigma,\;\overline{M}\langle N\rangle.Q) &=& \overline{M}\langle N\rangle\sigma.\hat{\delta'}(\ch,\;\sigma,\;Q)\\
\hat{\delta'}(\ch,\;\sigma,\;t\textnormal{::}\,Q) &=& \overline{a'}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{u_1,\dots,u_l}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma\rangle.a''(y).\hat{\delta'}(\mathsf{tail}(\mathsf{tail}(\ch)),\;\tau,\;Q)\\
&&\textrm{where $a' = \mathsf{head}(\ch)$, $a'' = \mathsf{head}(\mathsf{tail}(\ch))$ and} \\
&& \tau = \{\textnormal{\raisebox{2pt}{\footnotesize $\pi_{1}(y)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u_1$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $\pi_{l}(y)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u_l$}}\} \textrm{ for some names}\\
&& \textrm{and variables $u_1,\dots,u_l$, $y$ such that}\\
&& \textnormal{fn}(Q) \cup \textnormal{fv}(Q) = u_1,\dots,u_l \textrm{ and } y\not\in\textnormal{fv}(Q)\\
%
% Note in- and else-branches have different substitutions
%
\hat{\delta'}(\ch,\;\sigma,\;\textnormal{let } x=D \textnormal{ in } Q \textnormal{ else }R) &=& \textnormal{let } x=D\sigma \textnormal{ in }\hat{\delta'}(\mathsf{odd}(\ch),\;\tau,\;Q)\\
&& \qquad \qquad \textnormal{ else }\hat{\delta'}(\mathsf{even}(\ch),\;\sigma,\;R)\\
&& \textrm{where $\tau = \{ \textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}} \mid \{\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}}\} \in \sigma \textrm{ and } u \not= x\}$}\\
\hat{\delta'}(\ch,\;\sigma,\;Q \mid R) &=& \hat{\delta'}(\mathsf{odd}(\ch),\;\sigma,\;Q) \mid \hat{\delta'}(\mathsf{even}(\ch),\;\sigma,\;R)
\end{array}$$*
By definition of the barrier elimination function, at the start of each barrier synchronisation a process outputs all of the free names and variables under that barrier. The synchronisation process (Definition [def:syncFunc]) would simply return these values, as demonstrated in Example 3. Intuitively, however, it is possible to swap values between sub-processes which share the same structure under a particular barrier. Since this preserves the underlying structure of the biprocesses, it is useful for proofs of observational equivalence. In order to track which processes may swap data, the function $\omega$ is modified: $$\begin{array}{lcl}
\omega(\ch,\;t\textnormal{::}\,Q) &=& \{(t,\;a',\;a'',\;\hat{\delta'}(\hat\ch,\;\sigma,\;Q))\} \cup \omega(\hat\ch,\;Q)
\end{array}$$ where $a' = \mathsf{head}(\ch)$, $a'' = \mathsf{head}(\mathsf{tail}(\ch))$, $\hat\ch = \mathsf{tail}(\mathsf{tail}(\ch))$ and $\sigma = \{\textnormal{\raisebox{2pt}{\footnotesize $\pi_{1}(y)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u_1$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $\pi_{l}(y)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u_l$}}\}$ for some names and variables $u_1,\dots,u_l,y$ such that $\textnormal{fn}(Q) \cup \textnormal{fv}(Q) = u_1,\dots,u_l$ and $y\not\in\textnormal{fv}(Q)$. For simplicity, this definition, and Definition 1, assume there is exactly one tuple of names and variables $u_1,\dots,u_l,y$ such that $\textnormal{fn}(Q) \cup \textnormal{fv}(Q) = u_1,\dots,u_l$ and $y\not\in\textnormal{fv}(Q)$; that is, the same names and variables are used by the functions $\omega$ and $\delta'$.
The *swapping process* (Definition 2) is similar to the synchronisation process, but considers all possible swapping strategies in addition to synchronisation. In particular, the function $\bar{\chi}$ is introduced for this purpose. More precisely, sub-processes under a particular barrier are permitted to swap if they are syntactically equal. The consideration of the bijection $f \in \mathcal{F}$ ensures all swapping strategies are considered.
**Definition 2** (Swapping process). *Given a process $P$ and an infinite sequence of channel names ${\Ch}$, the set of *swapping processes* is $\chi'({\Ch},P) = \hat{\chi}'(1,\;\epsilon,\;\epsilon,\;\omega({\Ch},\;P))$, where for all integers $t$, communication processes $R$, $R'$ and sets $S$, we have: $$\hat{\chi}'(t,\;R,\;R',\;S) =
\left\{\begin{array}{lcl}
\{R.R'.0\} &\quad& \textrm{if $S = \emptyset$}\\[1em]
\bar{\chi}(t,\;R,\;R',\;S,\;Q) && \textrm{if $(t,a,b,Q) \in S$}\\[1em]
\hat{\chi}'(t+1,\;R.R',\;\epsilon,\;S) && \textrm{otherwise}
\end{array}\right.$$ such that $\bar{\chi}(t,R, R', S,Q)$ is defined as $$\begin{gathered}
\bigcup_{f\in\mathcal{F}}
\hat{\chi}'(t,\;R.a_1(y_1).\cdots.a_n(y_n),\;R'.\overline{b_1}\langle\textnormal{diff}[y_1,y_{f(1)}]\rangle.\cdots.\overline{b_n}\langle\textnormal{diff}[y_{f(n)},y_n]\rangle,\;\\S\backslash\{(t,a_1,b_1,Q),\dots,(t,a_n,b_n,Q)\})
\end{gathered}$$ where $(t,a_1,b_1,Q),\dots,(t,a_n,b_n,Q)\in S$, $\mathcal{F}$ is the set of bijections on $\{1,\dots,n\}$, and variables $y_1,\dots,y_n$ are fresh.*
Correctness of barrier ordering follows as before, and moreover, the notion of swapping is intuitively sound because it occurs between syntactically equal processes.
Finally, a set of processes in the standard ProVerif language, which consider all possible swapping strategies, can be derived.
**Definition 3** (Swapping compiler).
*The *swapping compiler* $\Delta'$ maps a process $P$ to a set of process, as follows: $\Delta'(P) = \{\nu\,\tilde{a}.(\delta'({\Ch},P) \mid R) \;\mid\; R\in\chi'({\Ch},P)\}$, where ${\Ch}$ is an infinite sequence of distinct channel names such that ${\Ch} \cap (\textnormal{fn}(P)\cup\textnormal{bn}(P)) = \emptyset$ and $\tilde{a} = \textnormal{fn}(\delta'({\Ch},P)) \cap {\Ch}$.*
Intuitively, if there exists a swapping strategy such that the compiled process satisfies observational equivalence, then the original process satisfies observational equivalence. The application of Definition 3 is demonstrated by Example 4 and has been implemented as a tool called ProSwapper (**Smyth10:ObsA?**).
**Example 4**. *Recall the process $P = \overline{c}\langle m\rangle.1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[m,n]\rangle \mid 1\textnormal{::}\,\overline{c}\langle\textnormal{diff}[n,m]\rangle$ from Example
[ex:newExample] and assume ${\Ch} = (a_1,a_2,\dots)$. We have: $$\begin{array}{rcl}
\delta'({\Ch},P) &=& \overline{c}\langle m\rangle.\overline{a_1}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{c,m,n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$})\rangle.a_3(x).\overline{\pi_{1}(x)}\langle\textnormal{diff}[\pi_{2}(x),\pi_{3}(x)]\rangle \mathrel{\mid}\\
&&\qquad\overline{a_2}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{c,n,m}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.a_4(x).\overline{\pi_{1}(x)}\langle\textnormal{diff}[\pi_{2}(x),\pi_{3}(x)]\rangle\\
\omega({\Ch},\;P) &=& \{(1,a_1,a_3,\overline{\pi_{1}(x)}\langle\textnormal{diff}[\pi_{2}(x),\pi_{3}(x)]\rangle),(1,a_2,a_4,\overline{\pi_{1}(x)}\langle\textnormal{diff}[\pi_{2}(x),\pi_{3}(x)]\rangle)\}\\
\chi'({\Ch},P) &=& \{a_1(y).a_2(z).\overline{a_3}\langle\textnormal{diff}[y,y]\rangle.\overline{a_4}\langle\textnormal{diff}[z,z]\rangle,\\
&&\qquad a_1(y).a_2(z).\overline{a_3}\langle\textnormal{diff}[y,z]\rangle.\overline{a_4}\langle\textnormal{diff}[z,y]\rangle\}
\end{array}$$ By Definition
3 we derive the set of processes which represent all possible swapping strategies: $$\begin{gathered}
\{ \nu\,a_1,a_2,a_3,a_4.(\delta'({\Ch},P) \mid a_1(y).a_2(z).\overline{a_3}\langle\textnormal{diff}[y,y]\rangle.\overline{a_4}\langle\textnormal{diff}[z,z]\rangle), \\
\nu\,a_1,a_2,a_3,a_4.(\delta'({\Ch},P) \mid a_1(y).a_2(z).\overline{a_3}\langle\textnormal{diff}[y,z]\rangle.\overline{a_4}\langle\textnormal{diff}[z,y]\rangle)\}
\end{gathered}$$ and since the latter process satisfies strong uniformity (see Appendix
[app:obs:src]), we believe the process $\Delta(P)$ satisfies observational equivalence. (Note that, in order to express results about $P$, rather than $\Delta(P)$, a formal semantics for barriers must be considered; for further discussion, see Section
[sec:further-work].)*
**Definition 1**. *The process $P_{\sf foo}$ modelling a voter in FOO is defined as follows $$\begin{array}{lcl}
P_{\sf foo} & = & \nu\,k.\nu\,k'.\\
&& \textnormal{let } M=\mathsf{commit}(k,x_{\mathsf{vote} }) \textnormal{ in } \\
&& \textnormal{let } \hat{M}=\mathsf{blind}(k',M) \textnormal{ in } \\
&& \overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(x_{\mathsf{sk }}),\mathsf{sign}(x_{\mathsf{sk }},\hat{M})}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.c(y).\\
&& \textnormal{if } \mathsf{checksign}(\mathsf{pk}(sk_R),y)=\mathsf{true} \textnormal{ then }\\
&& \textnormal{if } \mathsf{getmsg}(y)=\hat{M} \textnormal{ then }\\
&& \textnormal{let } M'=\mathsf{unblind}(k',y) \textnormal{ in }\\
&& 1\textnormal{::}\, \overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M,M'}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle . 2\textnormal{::}\, c(z).\\
&& \textnormal{if } \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{2}(z),\pi_{3}(z)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}=\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M,M'}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} \textnormal{ then } \\
&& \overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(z),k}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle
\end{array}$$ where $x_{\mathsf{sk }}$ is variable referring to the voter’s signing key and $x_{\mathsf{vote} }$ is a variable referring to voter’s vote.*
### Analysis: Vote privacy
Consider two voters $\mathcal{A}$, $\mathcal{B}$ and two candidates $s$, $s'$. Based upon (**KR05:vote-privacy?**; **DKR06?**; **DKR08?**; **DKR10?**), we formalise vote privacy for two voters with the assertion that an adversary cannot distinguish between a situation in which voter $\mathcal{A}$ votes for candidate $s$ and voter $\mathcal{B}$ votes for candidate $s'$, from another one in which $\mathcal{A}$ votes $s'$ and $\mathcal{B}$ votes $s$. Formally, this is written as the equivalence: $$\begin{gathered}
P_{\sf foo}\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{sk }}$}},\textnormal{\raisebox{2pt}{\footnotesize $s$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}}\}
\mid P_{\sf foo}\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{sk }}$}},\textnormal{\raisebox{2pt}{\footnotesize $s'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}}\}
\sim
P_{\sf foo}\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{sk }}$}},\textnormal{\raisebox{2pt}{\footnotesize $s'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}}\}
\mid P_{\sf foo}\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{sk }}$}},\textnormal{\raisebox{2pt}{\footnotesize $s$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}}\}
\end{gathered}$$ which can be checked using the methodology introduced. To provide further insight into how the swapping compiler works, let us consider how to informally prove this equivalence. Let us call the left hand side $\mbox{{\sc Lhs}}$, and the right hand side $\mbox{{\sc Rhs}}$. By definition of equivalence we must show that the $\mbox{{\sc Lhs}}$ is indistinguishable from the $\mbox{{\sc Rhs}}$. Indeed, as the $\mbox{{\sc Lhs}}$ evolves, the corresponding evolution of the $\mbox{{\sc Rhs}}$ is the one that mimics $\mathcal{A}$ moves on the $\mbox{{\sc Lhs}}$ with $\mathcal{A}$ moves on the $\mbox{{\sc Rhs}}$, and $\mathcal{B}$ moves on the $\mbox{{\sc Lhs}}$ with $\mathcal{B}$ moves on the $\mbox{{\sc Rhs}}$, up to the first barrier. After the first synchronisation, $\mathcal{A}$ moves on the $\mbox{{\sc Lhs}}$ are mimicked by $\mathcal{B}$ moves on the $\mbox{{\sc Rhs}}$, and $\mathcal{B}$ moves on the $\mbox{{\sc Lhs}}$ are mimicked by $\mathcal{A}$ moves on the $\mbox{{\sc Rhs}}$. The reason for the ‘swap’ in mimicking is to ensure that no context can distinguish the actions performed. Before the synchronisation, the output data produced by $\mathcal{A}$ on both the $\mbox{{\sc Lhs}}$ and the $\mbox{{\sc Rhs}}$ are indistinguishable (and similarly for $\mathcal{B}$); observe that on the $\mbox{{\sc Lhs}}$ the output by $\mathcal{A}$ reveals $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(sk_A),\;\mathsf{sign}(sk_A,\mathsf{blind}(k'_a,\mathsf{commit}(k_a,s))),\;\mathsf{blind}(k'_a,\mathsf{commit}(k_a,s))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$$ which can be matched on the $\mbox{{\sc Rhs}}$ by $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(sk_A),\;\mathsf{sign}(sk_A,\mathsf{blind}(k'_a,\mathsf{commit}(k_a,s'))),\;\mathsf{blind}(k'_a,\mathsf{commit}(k_a,s'))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$$ where names $k_a,k'_a$ are under restriction in both the $\mbox{{\sc Lhs}}$ and the $\mbox{{\sc Rhs}}$. (Note that indistinguishability between the $\mbox{{\sc Lhs}}$ and the $\mbox{{\sc Rhs}}$ is due to the properties of blinding.) After the first and second synchronisation, $\mathcal{A}$ will reveal $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{sign}(sk_R,\mathsf{commit}(k_a,s)),\;\mathsf{commit}(k_a,s)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\quad \textrm{ and } \quad \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\ell,\;k_a}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$$ on the $\mbox{{\sc Lhs}}$ and $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{sign}(sk_R,\mathsf{commit}(k_a,s')),\;\mathsf{commit}(k_a,s')}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\quad \textrm{ and } \quad \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\ell,\;k_a}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$$ on the $\mbox{{\sc Rhs}}$, where $\ell$ is chosen by the adversarial environment; that is, $\mathcal{A}$ reveals her vote $s$ on the $\mbox{{\sc Lhs}}$ and her vote $s'$ on the $\mbox{{\sc Rhs}}$ (similarly, $\mathcal{B}$ will reveal $s'$ on the $\mbox{{\sc Lhs}}$ and $s$ on the $\mbox{{\sc Rhs}}$). Hence, after the first synchronisation the actions mimicked are swapped. The compiler manages the swapping, and hence ProSwapper can be used to automatically analyse privacy in FOO (see Appendix [app:obs:src]).
# Summary
This chapter extends the process syntax of ProVerif to include barriers, for the purpose of synchronisation, and defines an automated methodology for proving equivalence. The result has been implemented as ProSwapper and the suitability of the tool is demonstrated by analysing vote privacy in the FOO electronic voting protocol. Furthermore, the fundamental principles of our methodology have been adopted by the wider research community: Dahl, Delaune & Steel (**Delaune10:Vanets?**) use an preliminary version of this chapter (formally presented in (**Smyth08:Obs?**)) to analyse privacy in vehicular ad-hoc networks, and Backes, Hriţcu & Maffei (**Backes08:Voting?**) use the basic concept (presumably based upon (**Smyth07:Obs:Dagstuhl?**)) to show coercion resistance in electronic voting.
**Evaluation**
# Further work and conclusion
In this thesis, we advance the capabilities of the formal verification community by *defining symbolic definitions* of security properties (Part II) and *developing procedures for evaluation* of security properties (Part III). The key contributions are:
- A definition of election verifiability for electronic voting protocols.
- A definition of user-controlled anonymity for Direct Anonymous Attestation schemes.
- An automated analysis technique for observational equivalence.
This final chapter presents future work and a further appraisal of results.
# Further work
We begin by discussing possible future research directions arising from Chapters [chap:ev]–[chap:obs] and identifying open questions that have emerged from this thesis.
## Election verifiability in electronic voting
The definition of election verifiability includes three aspects: individual, universal and eligibility verifiability. The conditions which these properties must satisfy are believed to be necessary, but may not be sufficient. Ultimately, a verifiable election should convince the most sceptic of voters and/or election observers that votes have been recorded, tallied and declared correctly. Establishing whether voting protocols which satisfy our definition, are also considered to achieve this objective, remains an open research problem.
The definition of election verifiability is based upon earlier work (**Smyth10:ElectionVerifiabilityA?**) in which automated reasoning was considered. Extending Chapter 3 to include an automated procedure for evaluating election verifiability would appear to be a logical step; however, this has been precluded by the lack of efficient tools for evaluating our definition in the general case. In particular, the tests must be embedded within processes (cf. (**Smyth10:ElectionVerifiabilityA?**)) and parametrised by an arbitrary number of voters, but such parametrisation is not currently supported by ProVerif. Providing automated tool support for processes which require parametrisation is further work and, moreover, such a tool would be useful for analysing security properties in a variety of cryptographic protocols.
The study of election verifiability identified eligibility verifiability – a property that has been largely neglected by the literature and is only satisfied by a few protocols – as a mechanism to detect ballot stuffing. As an alternative to eligibility verifiability, some electronic voting protocols provide a weaker notion of eligibility – which cannot be checked by voters or observers – under various trust assumptions. For example, such an eligibility property may assert that if the election officials follow the protocol, then each ballot published on the bulletin board was cast by a registered voter and at most one ballot is tallied per voter. Indeed, this assumption was thought to be reasonable in the presidential election at the Catholic University of Louvain which used Helios. However, similar assumptions must not be made about national elections. Accordingly, the study of electronic voting protocols which simultaneously satisfy election verifiability and other desirable properties, such as privacy and usability, remains an open problem.
## Anonymity in Direct Anonymous Attestation
Direct Anonymous Attestation is a relatively new concept and its properties merit further study. In particular, user-controlled traceability and correctness have received limited attention. Furthermore, new properties (for example, *non-frameability* (**Chen10:DAA-security-non-frameability-eprint?**; **Chen09:DAA-security-non-frameability?**)) are emerging. Extending this work to include a complete definition of DAA properties would be an interesting direction for future research. Moreover, establishing a unified definition which includes all properties (that is, correctness, non-frameability, user-controlled anonymity and user-controlled traceability) would be of interest to reduce the verification workload. As a starting point, this could be achieved by suitably developing the notion of a Direct Anonymous Attestation process specification to distinguish between operations performed by the host and those performed by the TPM. This distinction is not necessary for our definition of user-controlled anonymity because this property can only be achieved if both the host and TPM are trusted. By contrast, a corrupt host – even in collaboration with a corrupt TPM (where the TPM is known to be rogue) – should not be able to violate traceability properties and therefore an alternative process specification, which distinguishes between actions performed by the host and TPM, would be required.
For user-controlled anonymity it is necessary to ensure a distinct basename is used during phase 2 (when $bsn \not= \perp$). Since the applied pi calculus does not record state, this is achieved by an abstraction. Proving that this abstraction does not lose generality is an open problem. In addition, a stateful variant of the applied pi calculus would be useful.
The study of user-controlled anonymity in Direct Anonymous Attestation schemes is particular interesting due to the real-world deployment of the TPM. However, verification of cryptographic protocols does not ensure their secure deployment because vulnerabilities may be introduced during implementation (**Larrecq05:Verifing-C-Implementations?**; **Bhargavan06?**; **Bhargavan08c?**; **Paterson09:SSH-attack?**). Automatically deriving models from implementations and verifying security properties using ProVerif has been considered (**Bhargavan06?**; **Bhargavan08c?**; **Bhargavan08?**) and verified reference implementations have been introduced to aid the development of secure systems (**Bhargavan06b?**; **Bhargavan08b?**; **Mukhamedov09:TPM-reference?**). In the context of DAA, automatically verifying implementations (for example, (**Smyth06:MEng?**; **Strasser08?**; **Sterckx09:DAAImpl?**; **Chen10:ECC-DAA-assymmetric-optimised?**)) and developing a secure reference implementation remains as future work.
## Observational equivalence and barriers
Evaluating whether the synchronous compiler (Definition [def:syncProcess]) enforces the informally discussed semantic behaviour of barrier synchronisation is difficult to establish due to the complexity of definition. In this instance, it would be more suitable to formally define the semantics in the calculus of ProVerif and prove that the synchronous compiler encodes an approximation of the desired observational behaviour. Moreover, by extending the definition of observational equivalence to consider barriers, stronger results could be stated; that is, results could be stated about $P$ rather than $\Delta(P)$ (see, for example, Examples [ex:::] & [ex:swappingSet] and Section [sec:obs:FOO]).
Proving soundness of the proof technique is ongoing work. At a high level it would be sufficient to show that for all biprocesses $P$, if there exists $Q\in\Delta'(P)$ such that $Q$ satisfies strong uniformity, then $\Delta(P)$ satisfies observational equivalence. Accordingly, it would be sufficient to prove that for all biprocesses $P$, we have for all $Q\in \Delta'(P)$, that $\textnormal{fst}(\Delta(P)) \sim \textnormal{fst}(Q)$ and $\textnormal{snd}(\Delta(P)) \sim \textnormal{snd}(Q)$. (As previously stated, the formal semantics of barriers are not defined and thus we cannot state observational equivalence results involving processes with barriers; that is, we must rely upon the synchronous compiler.)
The definition of labelled bisimilarity (**AppliedPi?**), which complements observational equivalence (Definition [def:obs]), has proven to be useful for handwritten proofs of equivalence. A similar notion to complement Definition [def:proverif:obs] may be useful to prove observational equivalence in cases where automated reasoning is not possible. Furthermore, general procedures which consider arbitrary processes (rather than biprocesses) could be sought.
## Emerging directions
The formalisation of user-controlled anonymity in Direct Anonymous Attestation (Chapter [chap:DAA]) is similar, but distinct, from the formalisation of privacy in electronic voting (Section [sec:obs:example]) and vehicular ad-hoc networks (Appendix [app:obs:src:VANETS]). In electronic voting, vote privacy for two voters $\mathcal{A}$, $\mathcal{B}$ is formalised as the indistinguishability between a situation in which voter $\mathcal{A}$ votes for candidate $s$ and voter $\mathcal{B}$ votes for candidate $s'$, from another in which $\mathcal{A}$ votes $s'$ and $\mathcal{B}$ votes $s$. Using terminology from our formalisation of user-controlled anonymity, this essentially corresponds to two voters participating in the *challenge* phase. By comparison, in DAA we consider a single signer during the challenge phase. It is necessary to consider two voters for vote privacy because the election outcome will be made public and this would represent an observable distinction if only a single voter participated in the challenge, that is, we can distinguish between an election outcome of $s$ and $s'$. Establishing a generic class of definitions suitable for analysing privacy in a variety of settings would be desirable to obviate the need for numerous protocol dependent privacy definitions (for example, (**KR05:vote-privacy?**; **Chothia06:Mute?**; **Backes08:Voting?**; **DKR08?**; **ArapinisCSF10:RFID-privacy?**; **ChatzikokolakisCSF10:RFID-privacy?**; **Delaune10:Vanets?**)). Moreover, such a framework would allow the relative degrees of privacy to be studied.
# Conclusion
This thesis will aid the secure design of cryptographic protocols and facilitate the evaluation of existing schemes by advancing formal method verification techniques. Our definition of election verifiability has been shown to be suitable for the analysis of a wide range of electronic voting protocols and its future application will allow the thorough analysis of schemes prior to deployment, thereby helping ensure integral elections. The study of user-controlled anonymity in RSA-based Direct Anonymous Attestation discovered a vulnerability and established a fix which potentially avoided violations of privacy for TPM users. Our definition of user-controlled anonymity will also facilitate the analysis of future DAA schemes, helping prevent privacy invasions. Finally, the adoption of our reasoning technique for observational equivalence, by the research community, gives us confidence that the methodology is of value and, moreover, can be used to evaluate numerous security properties including vote privacy and coercion resistance in electronic voting, and privacy in vehicular ad-hoc networks.
**Appendices**
# Election verifiability results
This appendix contains proofs supporting Chapter [chap:ev].
# Election verifiability in raising hands
This appendix presents a proof of election verifiability in raising hands (Example [ex:raising-hands-spec]). The proof illustrates an interesting aspect of our definition: we do not require a voter to identify her credential, it is sufficient for a voter to identify a credential. If desired, a stronger definition of election verifiability can be constructed with the additional soundness condition $\Phi^{IV}_i \sigma \wedge \Phi^{IV}_i \{\textnormal{\raisebox{2pt}{\footnotesize $\hat w'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $\hat w$}}\} \sigma \Rightarrow \pi_{i}(\hat w)\sigma \simeq \pi_{i}(\hat w')\sigma$.
## Proof of Proposition [prop:handsEV]
*Proof.* Suppose $m\in\mathbb{N}$ and tests $\Phi^{IV}$, $\Phi^{UV}_m$, $\Phi^{EV}_m$ are given as follows: $$\begin{array}{lcl}
\Phi^{IV}& \widehat = & y =_E\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(r),\mathsf{sign}(r,v)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} %\textrm{\sout{$\wedge \Getmsg{w} =_\EE \Pk{r}$}}
\wedge \mathsf{checksign}(x_{pk},w) =_E\mathsf{true}\\
\Phi^{UV}_m & \widehat = & \hat v =_E\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{getmsg}(\pi_{2}(\pi_{1}(\hat y))),\dots,\mathsf{getmsg}(\pi_{2}(\pi_{m}(\hat y)))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} \\
\Phi^{EV}_m &\widehat= & \bigwedge_{1\leq i \leq m} \big( \mathsf{checksign}(x_{pk},\pi_{i}(\hat w)) =_E\mathsf{true}\wedge \pi_{1}(\pi_{i}(\hat y)) =_E\mathsf{getmsg}(\pi_{i}(\hat w)) \\
&&\quad \quad\mathrel{\wedge} \mathsf{checksign}(\pi_{1}(\pi_{i}(\hat y)),\pi_{2}(\pi_{i}(\hat y))) =_E\mathsf{true}\\
&&\quad \quad\quad \quad \mathrel\wedge {\mathsf{snd}(\mathsf{snd}(\mathsf{snd}(\pi_{i}(\hat y)))) \mathrel{=_E} {\varnothing}} \big)
\mathrel\wedge {\mathsf{snd}^m(\hat w) \mathrel{=_E} {\varnothing}} \mathrel\wedge {\mathsf{snd}^m(\hat y) \mathrel{=_E} {\varnothing}}
\end{array}$$ where $r = \textnormal{rv}(\Phi^{IV})$. We will now show for all names $s_1,\dots,s_n$ that the conditions of Definition
[def:ev2] hold.
1. Suppose $C$ is a context, $B$ is a process, $\sigma$ is a substitution, $\tilde n$ is a tuple of names and $i,j$ are integers where $C[{\sf
VP^+_n}(s_1,\dots,\allowbreak s_n)] \mathrel{(\to^* \xrightarrow{\alpha} \to^*)^*} B$, $\varphi(B) \equiv \nu \tilde
n.\sigma$, $\Phi^{IV}\{\textnormal{\raisebox{2pt}{\footnotesize $s_i$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $r_i$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $r$}}, \textnormal{\raisebox{2pt}{\footnotesize $\pi_{i}(\hat w)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $w$}}\}\sigma$ and $\Phi^{IV}\{\textnormal{\raisebox{2pt}{\footnotesize $s_j$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $r_j$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $r$}}, \textnormal{\raisebox{2pt}{\footnotesize $\pi_{j}(\hat w)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $w$}}\}\sigma$. It follows that $\pi_{1}(y)\sigma =_E\mathsf{pk}(r_i)\sigma =_E\mathsf{pk}(r_j)\sigma$. Since the record variables $r_i$, $r_j$ are handles for fresh nonces generated by name restriction in the process $A_{\sf ex}$ and sent to $V_{{\sf ex}, i}$, $V_{{\sf ex},j}$ using a private channel, it follows that $i=j$.
2. We prove a stronger result: namely, the condition holds for all substitutions $\sigma$. Suppose $\sigma$ is an arbitrary substitution such that $\Phi^{UV}_m \sigma$ and $\Phi^{UV}_m \{^{\hat v'}/_{\hat v} \} \sigma$ hold. We have $$\hat v \sigma =_E\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{getmsg}(\pi_{2}(\pi_{1}(\hat y))),\dots,\mathsf{getmsg}(\pi_{2}(\pi_{m}(\hat y)))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma =_E\hat v' \sigma$$ and immediately derive $\hat v\sigma \simeq \hat v'\sigma$.
3. Again, we will show that the condition holds for all substitutions $\sigma$. Suppose $\sigma$ is an arbitrary substitution such that $\bigwedge_{1 \leq i \leq n} \Phi^{IV}_i \{\textnormal{\raisebox{2pt}{\footnotesize $\pi_{i}(\hat{y})$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\} \sigma$ and $\Phi^{UV}_m \sigma$ hold, where $n = m$. By $\bigwedge_{1 \leq i \leq n} \Phi^{IV}_i \{\textnormal{\raisebox{2pt}{\footnotesize $\pi_{i}(\hat{y})$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\} \sigma$ it must be the case for all $1\leq i \leq n$ that $\pi_{i}(\hat y)\sigma =_E\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(r_i),\mathsf{sign}(r_i,s_i)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma$ and hence $\mathsf{getmsg}(\pi_{2}(\pi_{i}(\hat y)))\sigma =_Es_i$. Moreover, since $n = m$ and $\Phi^{UV}_m \sigma$, we have $$\hat v\sigma =_E\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{getmsg}(\pi_{2}(\pi_{1}(\hat y))),\dots,\mathsf{getmsg}(\pi_{2}(\pi_{m}(\hat y)))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma
=_E\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{s_1,\dots,s_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$$ The result $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{s_1,\dots,s_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} \simeq \hat v\sigma$ follows.
- We prove a stronger result: namely, for any substitution $\sigma$ the condition holds. Suppose $\sigma$ is an arbitrary substitution such that $\Phi^{EV}_m \sigma$ and $\Phi^{EV}_m \{^{x'} / _x \mid x\in X \backslash\hat y\} \sigma$ hold. For all $1\leq i\leq m$, we have $$\begin{gathered}
\mathsf{getmsg}(\pi_{i}(\hat w))\sigma =_E\pi_{1}(\pi_{i}(\hat y))\sigma
\wedge \pi_{1}(\pi_{i}(\hat y))\sigma =_E\mathsf{getmsg}(\pi_{i}(\hat w'))\sigma\\
\mathrel{\wedge} \mathsf{checksign}(\pi_{i}(\hat w),x_{pk})\sigma =_E\mathsf{true}\wedge \mathsf{checksign}(\pi_{i}(\hat w'),x_{pk})\sigma =_E\mathsf{true}
\end{gathered}$$ and, by inspection of the equational theory, it must be the case that $\pi_{i}(\hat w)\sigma = \pi_{i}(\hat w')\sigma = \mathsf{sign}(K_i,\pi_{1}(\pi_{i}(\hat y)))\sigma$, where $x_{pk}\sigma = \mathsf{pk}(K_i)$. By $\Phi^{EV}_m \sigma$ and $\Phi^{EV}_m \{^{x'} / _x \mid x\in X \backslash\hat y\} \sigma$ we also have $\mathsf{snd}^m(\hat w) \mathrel{=_E} \mathsf{snd}^m(\hat w') \mathrel{=_E} {\varnothing}$. It must be the case that $\hat w \sigma = \hat w'\sigma = \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{sign}(K_1,\pi_{1}(\pi_{1}(\hat y))),\dots,\allowbreak\mathsf{sign}(K_m,\pi_{1}(\pi_{m}(\hat y)))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma$ and hence $\hat w \sigma \simeq \hat w'\sigma$.
- Suppose $C$ is a context and $B$ is a process such that $C[{\sf VP^+_n}(s_1,\dots,\allowbreak s_n)] \mathrel{(\to^* \xrightarrow{\alpha} \to^*)^*} B$, $\varphi(B)\equiv\nu\tilde n.\sigma$, and $\Phi^{EV}_m \sigma \wedge \Phi^{EV}_m \{^{x'} / _x \mid x\in X\backslash\hat w\} \sigma$. For all $1\leq i \leq m$, we have $\mathsf{checksign}(x_{pk},\pi_{i}(\hat w))\sigma =_E\mathsf{true}$, where $x_{pk}\sigma = \mathsf{pk}(sk_A)$ and $sk_A \in \tilde n$. By inspection of the equational theory it is the case that $\pi_{i}(\hat w)\sigma =_E\mathsf{sign}(sk_A,M_i)$ for some term $M_i$. Since the signing key is under restriction and, by inspection of the voting process, it follows that for all $1 \leq i \leq m$ we have $M_i =_E\mathsf{pk}(sk_{V_i})$, where $sk_{V_i} \in \tilde n$. By $\Phi^{EV}_m \sigma$ and $\Phi^{EV}_m \{^{x'} / _x \mid x\in X\backslash\hat w\} \sigma$ we also have $\pi_{1}(\pi_{i}(\hat y)) \sigma =_E\mathsf{getmsg}(\pi_{i}(\hat w) )\sigma =_E\pi_{1}(\pi_{i}(\hat y') )\sigma$, that is, $$\pi_{1}(\pi_{i}(\hat y))\sigma =_E\mathsf{pk}(sk_{V_i}) =_E\pi_{1}(\pi_{i}(\hat y') )\sigma.$$ Moreover, $\mathsf{checksign}(\pi_{1}(\pi_{i}(\hat y)),\pi_{2}(\pi_{i}(\hat y))) \sigma=_E\mathsf{true}\wedge \mathsf{checksign}(\pi_{1}(\pi_{i}(\hat y')),\pi_{2}(\pi_{i}(\hat y')))\sigma =_E\mathsf{true}$. Since the signing keys $sk_{V_1},\dots,sk_{V_m}$ are under restriction it follows for all $1\leq i\leq m$ that $$\pi_{2}(\pi_{i}(\hat y))\sigma =_E\mathsf{sign}(sk_{V_i},s_i)
=_E\pi_{2}(\pi_{i}(\hat y'))\sigma$$ Furthermore, for all $1\leq i\leq m$, we have $\mathsf{snd}(\mathsf{snd}(\mathsf{snd}(\pi_{i}(\hat y)))) \mathrel{=_E} \mathsf{snd}(\mathsf{snd}(\mathsf{snd}(\pi_{i}(\hat y')))) \mathrel{=_E} {\varnothing}$ and hence $$\pi_{i}(\hat y)\sigma =_E\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(sk_{V_i}), \mathsf{sign}(sk_{V_i},s_i)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} =_E
\pi_{i}(\hat y')\sigma$$ Since $\mathsf{snd}^m(\hat y)\sigma \mathrel{=_E} \mathsf{snd}^m(\hat y')\sigma \mathrel{=_E}{\varnothing}$, we have $\hat y\sigma = _E\hat y'\sigma$ and hence $\hat y \sigma \simeq \hat y'\sigma$.
- Suppose $C$ is a context and $B$ is a process such that $C[{\sf VP^+_n}(s_1,\dots,\allowbreak s_n)] \mathrel{(\to^* \xrightarrow{\alpha} \to^*)^*} B$, $\varphi(B)\equiv\nu\tilde n.\sigma$, and $\bigwedge_{1 \leq i \leq n} \Phi^{IV}_i\{\textnormal{\raisebox{2pt}{\footnotesize $\pi_{i}(\hat y)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}} \} \sigma \wedge \Phi^{EV}_n\{^{\hat w'}/_{\hat w} \} \sigma \wedge \mathsf{snd}^n(\hat w)\sigma =_E{\varnothing}$ holds. For all $1\leq i \leq n$, we have $\mathsf{checksign}(x_{pk},\pi_{i}(\hat w))\sigma =_E\mathsf{true}$, where $x_{pk}\sigma = \mathsf{pk}(sk_A)$ and $sk_A \in \tilde n$. By inspection of the equational theory it is the case that $\pi_{i}(\hat w)\sigma =_E\mathsf{sign}(sk_A,M_i)$ for some term $M_i$. Since the signing key is under restriction and, by inspection of the voting process, it follows for all $1 \leq i \leq n$ that $M_i =_E\mathsf{pk}(sk_{V_i})$, where $sk_{V_i} \in \tilde n$. Moreover, $\mathsf{snd}^n(\hat w)\sigma =_E{\varnothing}$ and hence $$\hat w\sigma =_E\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{sign}(sk_A,\mathsf{pk}(sk_{V_1})),\dots,\mathsf{sign}(sk_A,\mathsf{pk}(sk_{V_n}))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$$ Similarly, we have $1\leq i \leq n$ that $\mathsf{checksign}(x_{pk},\pi_{i}(\hat w'))\sigma =_E\mathsf{true}$, where $x_{pk}\sigma = \mathsf{pk}(sk_A)$ and $sk_A \in \tilde n$. As before, $\pi_{i}(\hat w')\sigma =_E\mathsf{sign}(sk_A,N_i)$ by inspection of the equational theory. Since the signing key is under restriction and, by inspection of the voting process (in particular, observe that $A_{\sf ex}$ outputs exactly $n$ messages of the form $\mathsf{sign}(sk_A,N_i)$), there exists a permutation $\chi$ defined over $\{1,\dots,n\}$ such that for all $1 \leq i \leq n$ we have $N_i =_E\mathsf{pk}(sk_{V_{\chi(i)}})$. Moreover, by $\Phi^{EV}_n\{^{\hat w'}/_{\hat w} \} \sigma$ we have $\mathsf{snd}^n(\hat w') \mathrel{=_E} {\varnothing}$ and hence $$\hat w'\sigma =_E\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{sign}(sk_A,\mathsf{pk}(sk_{V_{\chi(1)}})),\dots,\mathsf{sign}(sk_A,\mathsf{pk}(sk_{V_{\chi(n)}}))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$$ The result $\hat w\sigma \simeq \hat w'\sigma$ follows.
- Suppose $s_1,\dots,s_n$ are names and consider the context $$\begin{array}{lcl}
C &\mathrel{\hat =}& c(w_1).\dots.c(w_n).\overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{w_1,\dots,w_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.\\
&&c(y_1).\dots.c(y_n).\overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{y_1,\dots,y_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.\\
&&\overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{getmsg}(\pi_{2}(y_1)),\dots,\mathsf{getmsg}(\pi_{2}(y_n))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle
\end{array}$$ We have $C[{\sf VP}_n^+(s_1,\dots,s_n)]\allowbreak \mathrel{(\to^* \xrightarrow{\alpha} \to^*)^*} B$ such that $\varphi(B) \equiv \nu sk_A, sk_{V_1}, \ldots, sk_{V_n}.\sigma$, where $$\begin{gathered}
\sigma = \{
^{sk_{V_1}}/_{r_{1}},\dots,^{sk_{V_n}}/_{r_{n}},
\textnormal{\raisebox{2pt}{\footnotesize $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{s_1,\dots,s_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $\hat v$}},
\textnormal{\raisebox{2pt}{\footnotesize $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{sign}(sk_A,\mathsf{pk}(sk_{V_1})),\dots,\mathsf{sign}(sk_A,\mathsf{pk}(sk_{V_n}))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $\hat w$}},\\
^{\mathsf{pk}(sk_A)} / _{x_{pk}},
\textnormal{\raisebox{2pt}{\footnotesize $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}({sk_{V_1}}), \mathsf{sign}(sk_{V_1},s_1)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},\dots,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}({sk_{V_n}}), \mathsf{sign}(sk_{V_n},s_n)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $\hat y$}} \}
\end{gathered}$$ It can trivially be seen that $\bigwedge_{1 \leq i \leq n} \Phi^{IV}_i\{\textnormal{\raisebox{2pt}{\footnotesize $\pi_{i}(\hat y)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\} \sigma \wedge \Phi^{UV}_m \sigma \wedge \Phi^{EV}_m \sigma$.
◻
**Lemma 1**. *Given terms $L,M,N$, if $\mathsf{pet}(L,M,N) =_E\mathsf{true}$, then $M \stackrel{\bullet}{\simeq} N$.*
**Lemma 2**. *Given terms $L,\hat{M},\hat{N}$, if $\mathsf{checkMix}(L,\hat M,\hat N) =_E\mathsf{true}$, then $\hat M \stackrel{\bullet}{\simeq} \hat N$.*
**Lemma 3**. *Given terms $L,\hat{M},\hat{N}$, if $\mathsf{checkMixPair}(L,\hat M,\hat N) \allowbreak =_E\mathsf{true}$, then $\allowbreak\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}\pi_{i}(M_1),\allowbreak\dots,\allowbreak\pi_{i}(M_{|\tilde M|})\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\stackrel{\bullet}{\simeq} \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{i}(N_1),\dots,\pi_{i}(N_{|\hat N|})}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$, where $i\in\{1,2\}$.*
## Proof of Theorem [thm:jcj]
*Proof.* Suppose $m\in\mathbb{N}$ and the tests $\Phi^{IV},\Phi^{UV}_m,\Phi^{EV}_m$ are given above. We will now show for all names $s_1,\dots,s_n$ that the conditions of Definition
[def:ev2] hold.
1. Suppose $C$ is a context, $B$ is a process and $i,j$ are integers such that $C[{\sf VP^+_n}(\allowbreak s_1,\allowbreak\dots,\allowbreak s_n)]\allowbreak \mathrel{(\to^* \xrightarrow{\alpha} \to^*)^*} B$, $\varphi(B)\equiv\nu\tilde n.\sigma$ and $\Phi^{IV}\{^{s_i} /_v,
\textnormal{\raisebox{2pt}{\footnotesize $\tilde r_{i}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $\tilde r$}}, \textnormal{\raisebox{2pt}{\footnotesize $\pi_{i}(\hat w)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $w$}}\}\sigma
\wedge
\Phi^{IV}\{^{s_j} /_v,\allowbreak
\textnormal{\raisebox{2pt}{\footnotesize $\tilde r_{j}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $\tilde r$}}, \textnormal{\raisebox{2pt}{\footnotesize $\pi_{j}(\hat w)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $w$}}\}\sigma$. It follows that $\pi_{1}(y)\sigma =_E\mathsf{penc}(x_{\mathsf{pk_T}},r_{m,i},s_i)\sigma =_E\mathsf{penc}(x_{\mathsf{pk_T}},r_{m,j},\allowbreak
s_j) \sigma$ and, by inspection of the equational theory, it is the case that $r_{m,i}\sigma = r_{m,j}\sigma$. Since the record variables $r_{m,i}$, $r_{m,j}$ are handles for fresh nonces created by name restriction in the voter process, it follows immediately from $r_{m,i}\sigma = r_{m,j}\sigma$ that $i=j$.
2. We prove a stronger result: namely, for any substitution $\sigma$ the condition holds. Suppose $\Phi^{UV}_m \sigma \wedge \Phi^{UV}_m \{^{\hat v'}/_{\hat v} \} \sigma$ and hence $$\hat v\sigma =_E\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{dec}(z_{\mathsf{partial},1},\pi_{1}(z_{\mathsf{bal},1})),\dots,\mathsf{dec}(z_{\mathsf{partial},m},\pi_{1}(z_{\mathsf{bal},m}))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma =_E\hat v'\sigma$$ It follows immediately that $\hat v\sigma \simeq \hat v'\sigma$.
3. Again, we will show that the condition holds for all substitutions $\sigma$. Suppose $\Phi^{IV}\{^{s_i} /_v,\allowbreak \textnormal{\raisebox{2pt}{\footnotesize $\tilde r_{i}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $\tilde r$}},\allowbreak \textnormal{\raisebox{2pt}{\footnotesize $\pi_{i}(\hat w)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $w$}},\allowbreak \textnormal{\raisebox{2pt}{\footnotesize $\pi_{i}(\hat y)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\} \sigma$ holds for $1 \leq i \leq n$ and hence $$\bigwedge_{1 \leq i \leq n} \pi_{1}(\pi_{i}(\hat y))\sigma =_E\mathsf{penc}(x_{\mathsf{pk_T}},r_{m,i},s_i)\sigma.$$ Moreover, suppose $\Phi^{UV}_m \sigma$ holds and $n = m$, therefore $$\begin{gathered}
\mathsf{checkMixPair}({z_{\mathsf{mixPairPf}}},\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(\pi_{1}(\hat y)),\pi_{2}(\pi_{1}(\hat y))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},\ldots,\\\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(\pi_{m}(\hat y)),\pi_{2}(\pi_{m}(\hat y))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},z_{\mathsf{bal},1},\ldots,z_{\mathsf{bal},m})\sigma =_E\mathsf{true}
\end{gathered}$$ holds. By inspection of the equational theory we have $$\pi_{1}(z_{\mathsf{bal},i})\sigma =_E\mathsf{penc}(x_{\mathsf{pk_T}},r_{m,\chi(i)} \circ R_i,s_{\chi(i)})\sigma$$ where $1\leq i \leq n$ for some permutation $\chi$ defined over $\{1,\dots,n\}$ and terms $R_1,\dots,R_n$ (note $R_1,\dots,R_n$ appear in ${z_{\mathsf{mixPairPf}}}\sigma$). By our hypothesis, for all $1 \leq i \leq n$, we have $${\mathsf{checkPartialPf}}(x_{\mathsf{pk_T}},\pi_{1}(z_{\mathsf{bal},i}),z_{\mathsf{partial},i},z_{\mathsf{partialPf},i})\sigma =_E\mathsf{true}$$ and hence $z_{\mathsf{partial},i}\sigma$ is a partial decryption for $\pi_{1}(z_{\mathsf{bal},i})\sigma$. It follows, for all $1 \leq i \leq n$, that $$\mathsf{dec}(z_{\mathsf{partial},i},\pi_{1}(z_{\mathsf{bal},i}))\sigma =_Es_{\chi(i)}$$ Finally, by hypothesis, we also have $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{dec}(z_{\mathsf{partial},1},\pi_{1}(z_{\mathsf{bal},1})),\dots,\mathsf{dec}(z_{\mathsf{partial},m},\pi_{1}(z_{\mathsf{bal},m}))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma =_E\hat v\sigma$$ and hence it follows that $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{s_1,\dots,s_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} \simeq \hat v\sigma$.
4. Suppose $C$ is a context and $B$ is a process such that $C[{\sf VP^+_n}(s_1,\dots,\allowbreak s_n)] \mathrel{(\to^* \xrightarrow{\alpha} \to^*)^*} B$, $\varphi(B)\equiv\nu\tilde n.\sigma$, and $\Phi^{EV}_m \sigma \wedge \Phi^{EV}_m \{^{x'} / _x \mid x\in X\backslash\hat y\} \sigma$. For all $1\leq i \leq m$, we have $\mathsf{checkBallot}(\pi_{3}(\pi_{i}(\hat y)),\pi_{1}(\pi_{i}(\hat y)),\pi_{2}(\pi_{i}(\hat y)))\sigma =_E\mathsf{true}$ and it follows by inspection of the equational theory that $$\pi_{2}(\pi_{i}(\hat y))\sigma =_E\mathsf{penc}(K_i,S_i,M_i)$$ for some terms $K_i, S_i, M_i$. Since $\mathsf{checkMixPair}({z_{\mathsf{mixPairPf}}},\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(\pi_{1}(\hat y)),\pi_{2}(\pi_{1}(\hat y))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},\ldots,\linebreak\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}\pi_{1}(\pi_{m}(\hat y)),\pi_{2}(\pi_{m}(\hat y))\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},z_{\mathsf{bal},1},\ldots,z_{\mathsf{bal},m})\sigma =_E\mathsf{true}$ and $\mathsf{checkMixPair}({z_{\mathsf{mixPairPf}}}',\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}\pi_{1}(\pi_{1}(\hat y)),\allowbreak\pi_{2}(\pi_{1}(\hat y))\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},\ldots,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(\pi_{m}(\hat y)),\pi_{2}(\pi_{m}(\hat y))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},z_{\mathsf{bal},1}',\ldots,z_{\mathsf{bal},m}')\sigma =_E\mathsf{true}$; it follows by Lemma
3 and transitivity of $\stackrel{\bullet}{\simeq}$ that $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{2}(z_{\mathsf{bal},1}),\ldots,\pi_{2}(z_{\mathsf{bal},m})}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma \stackrel{\bullet}{\simeq} \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{2}(z_{\mathsf{bal},1}'),\ldots,\pi_{2}(z_{\mathsf{bal},m}')}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma.$$ Moreover, for all $1\leq i \leq m$, we have $\mathsf{pet}(z_{\mathsf{petPf},i},\pi_{2}(z_{\mathsf{bal},i}),{\bar{z}}_{\mathsf{cred},i})\sigma =_E\mathsf{true}$ and $\mathsf{pet}(z_{\mathsf{petPf},i}',\allowbreak\pi_{2}(z_{\mathsf{bal},i}'),{\bar{z}}_{\mathsf{cred},i}')\sigma =_E\mathsf{true}$; by Lemma
1 it follows that $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{{\bar{z}}_{\mathsf{cred},1},\ldots,{\bar{z}}_{\mathsf{cred},m}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma \stackrel{\bullet}{\simeq} \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{{\bar{z}}_{\mathsf{cred},1}',\ldots,{\bar{z}}_{\mathsf{cred},m}'}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma.$$ We have $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{z_{\mathsf{cred},1},\ldots,z_{\mathsf{cred},m}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma\simeq\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{{\bar{z}}_{\mathsf{cred},1},\ldots,{\bar{z}}_{\mathsf{cred},m}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma$, $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{z_{\mathsf{cred},1}',\ldots,z_{\mathsf{cred},m}'}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\allowbreak\sigma\simeq\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\bar{z}}_{\mathsf{cred},1}',\ldots,\allowbreak{\bar{z}}_{\mathsf{cred},m}'\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma$ and hence we trivially derive $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{z_{\mathsf{cred},1},\ldots,z_{\mathsf{cred},m}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma \stackrel{\bullet}{\simeq} \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{z_{\mathsf{cred},1}',\ldots,z_{\mathsf{cred},m}'}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma.$$ Since $\mathsf{checkMix}({z_{\mathsf{mixPf}}},\mathsf{getmsg}(\pi_{1}(\hat w)),\ldots,\mathsf{getmsg}(\pi_{m}(\hat w)),z_{\mathsf{cred},1},\ldots,z_{\mathsf{cred},m})\sigma =_E\mathsf{true}$ and $\mathsf{checkMix}({z_{\mathsf{mixPf}}}',\mathsf{getmsg}(\pi_{1}(\hat w')),\ldots,\mathsf{getmsg}(\pi_{m}(\hat w')),z_{\mathsf{cred},1}',\ldots,z_{\mathsf{cred},m}')\sigma=_E\mathsf{true}$; it follows by Lemma
2 that $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{getmsg}(\pi_{1}(\hat w)),\ldots,\mathsf{getmsg}(\pi_{m}(\hat w))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma \stackrel{\bullet}{\simeq} \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{getmsg}(\pi_{1}(\hat w')),\ldots,\mathsf{getmsg}(\pi_{m}(\hat w'))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma.$$ For all $1\leq i \leq m$, we have $\mathsf{checksign}(x_{spk_R},\pi_{i}(\hat w))\sigma =_E\mathsf{true}$ and $\mathsf{checksign}(\allowbreak x_{spk_R},\pi_{i}(\hat w'))\sigma \allowbreak=_E\mathsf{true}$, where $x_{spk_R}\sigma = \mathsf{pk}(ssk_R)$ and $ssk_R \in \tilde{n}$. By inspection of the equational theory it is the case that $\pi_{i}(\hat w)\sigma =_E\mathsf{sign}(ssk_R,M_i)\sigma$ and $\pi_{i}(\hat w')\sigma =_E\mathsf{sign}(ssk_R,M'_i)\sigma$ for some terms $M_i,M'_i$. Furthermore, since, for all $1\leq i \leq m$, we have $\mathsf{getmsg}(\pi_{i}(\hat w))\sigma =_EM_i$, $\mathsf{getmsg}(\pi_{i}(\hat w'))\sigma =_EM'_i$ and because $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{getmsg}(\pi_{1}(\hat w)),\ldots,\mathsf{getmsg}(\pi_{m}(\hat w))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma \stackrel{\bullet}{\simeq}\break\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}\mathsf{getmsg}(\pi_{1}(\hat w')),\ldots,\mathsf{getmsg}(\pi_{m}(\hat w'))\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma$, it follows that $\tilde M \stackrel{\bullet}{\simeq} \tilde M'$. Now, since the signing key is under restriction and, by inspection of the voting process and its possible outputs, it follows for all $1\leq i \leq m$ that $$\begin{array}{lcl}
\mathsf{getmsg}(\pi_{i}(\hat w))
\sigma =_E\mathsf{penc}(\mathsf{pk}(sk_R),m''_{\chi(i)},d_{\chi(i)}) \\
\mathsf{getmsg}(\pi_{i}(\hat w'))\sigma =_E\mathsf{penc}(\mathsf{pk}(sk_R),m''_{\chi'(i)},d_{\chi'(i)})
\end{array}$$ where $d_i,m''_i$ are names under restriction in the registrar process $R$, $x_{pk_R}\sigma \allowbreak=_E\mathsf{pk}(sk_R)$ and $\chi, \chi'$ are permutations defined over $\{1,\dots,n\}$. Finally, we have $\mathsf{snd}^m(\hat w) =_E\mathsf{snd}^m(\hat w') =_E{\varnothing}$ and hence conclude $\hat w \sigma \simeq \hat w' \sigma$.
5. Suppose $C$ is a context and $B$ is a process such that $C[{\sf VP^+_n}(s_1,\dots,\allowbreak s_n)] \mathrel{(\to^* \xrightarrow{\alpha} \to^*)^*} B$, $\varphi(B)\equiv\nu\tilde n.\sigma$, and $\Phi^{EV}_m \sigma \wedge \Phi^{EV}_m \{^{x'} / _x \mid x\in X\backslash\hat w\} \sigma$. For all $1\leq i \leq m$, we have $\mathsf{checksign}(x_{spk_R},\pi_{i}(\hat w))\sigma =_E\mathsf{true}$, where $x_{spk_R}\sigma = \mathsf{pk}(ssk_R)$ and $ssk_R \in \tilde{n}$. By inspection of the equational theory it is the case that $$\pi_{i}(\hat w)\sigma =_E\mathsf{sign}(ssk_R,M_i)\sigma$$ for some term $M_i$. Since the signing key is under restriction and, by inspection of the voting process, it follows that for all $1\leq i \leq m$ we have $$M_i =_E\mathsf{penc}(\mathsf{pk}(sk_R),m''_i,d_i)$$ where $d_i,m''_i$ are names under restriction in the registrar process $R$ and $x_{pk_R}\sigma =_E\mathsf{pk}(sk_R)$. Since $\mathsf{checkMix}({z_{\mathsf{mixPf}}},\mathsf{getmsg}(\pi_{1}(\hat w)),\ldots,\mathsf{getmsg}(\pi_{m}(\hat w)),z_{\mathsf{cred},1},\allowbreak\ldots,z_{\mathsf{cred},m})\sigma =_E\mathsf{true}$, $\mathsf{checkMix}({z_{\mathsf{mixPf}}}',\mathsf{getmsg}(\pi_{1}(\hat w)),\ldots,\mathsf{getmsg}(\pi_{m}(\hat w)),\allowbreak z_{\mathsf{cred},1}',\ldots,z_{\mathsf{cred},m}')\sigma =_E\mathsf{true}$ and for all $1 \leq i \leq m$ we have $\mathsf{getmsg}(\pi_{i}(\hat w))\sigma =_EM_i$; it follows that $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{z_{\mathsf{cred},1},\ldots,z_{\mathsf{cred},m}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma \stackrel{\bullet}{\simeq} \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{z_{\mathsf{cred},1}',\ldots,z_{\mathsf{cred},m}'}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma$$ by Lemma
2. We have $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{z_{\mathsf{cred},1},\ldots,z_{\mathsf{cred},m}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma\simeq\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\bar{z}}_{\mathsf{cred},1},\ldots,\allowbreak{\bar{z}}_{\mathsf{cred},m}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma$ and $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}z_{\mathsf{cred},1}',\allowbreak\ldots,\allowbreak z_{\mathsf{cred},m}'\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma\simeq\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\bar{z}}_{\mathsf{cred},1}',\ldots,\allowbreak{\bar{z}}_{\mathsf{cred},m}'\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma$; it trivially follows that $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{{\bar{z}}_{\mathsf{cred},1},\ldots,{\bar{z}}_{\mathsf{cred},m}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma \stackrel{\bullet}{\simeq} \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{{\bar{z}}_{\mathsf{cred},1}',\ldots,{\bar{z}}_{\mathsf{cred},m}'}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma.$$ Moreover, for all $1\leq i \leq m$, we have $\mathsf{pet}(z_{\mathsf{petPf},i},\pi_{2}(z_{\mathsf{bal},i}),{\bar{z}}_{\mathsf{cred},i})\sigma =_E\mathsf{true}$ and $\mathsf{pet}(z_{\mathsf{petPf},i}',\allowbreak\pi_{2}(z_{\mathsf{bal},i}'),{\bar{z}}_{\mathsf{cred},i}')\sigma =_E\mathsf{true}$; hence by Lemma
1 it follows that $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{2}(z_{\mathsf{bal},1}),\ldots,\pi_{2}(z_{\mathsf{bal},m})}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma \stackrel{\bullet}{\simeq} \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{2}(z_{\mathsf{bal},1}'),\ldots,\pi_{2}(z_{\mathsf{bal},m}')}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma.$$ By $\mathsf{checkMixPair}({z_{\mathsf{mixPairPf}}},\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(\pi_{1}(\hat y)),\pi_{2}(\pi_{1}(\hat y))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},\ldots,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(\pi_{m}(\hat y)),\pi_{2}(\pi_{m}(\hat y))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},z_{\mathsf{bal},1},\ldots,\linebreak z_{\mathsf{bal},m})\sigma =_E\mathsf{true}$, $\mathsf{checkMixPair}({z_{\mathsf{mixPairPf}}}',\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(\pi_{1}(\hat y')),\pi_{2}(\pi_{1}(\hat y'))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},\ldots,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}\pi_{1}(\pi_{m}(\hat y')),\linebreak\pi_{2}(\pi_{m}(\hat y'))\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},z_{\mathsf{bal},1}',\ldots,z_{\mathsf{bal},m}')\sigma =_E\mathsf{true}$ and Lemma
3 we have $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{2}(\pi_{1}(\hat y)),\ldots,\pi_{2}(\pi_{m}(\hat y))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma \stackrel{\bullet}{\simeq} \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{2}(\pi_{1}(\hat y')),\ldots,\pi_{2}(\pi_{m}(\hat y'))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma.$$ For all $1\leq i \leq m$, we have $\mathsf{checkBallot}(\pi_{3}(\pi_{i}(\hat y)),\pi_{1}(\pi_{i}(\hat y)),\pi_{2}(\pi_{i}(\hat y)))\sigma =_E\mathsf{true}$ and $\mathsf{checkBallot}(\pi_{3}(\pi_{i}(\hat y')),\pi_{1}(\pi_{i}(\hat y')),\pi_{2}(\pi_{i}(\hat y')))\sigma =_E\mathsf{true}$. By inspection of the equational theory and because $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{2}(\pi_{1}(\hat y)),\ldots,\pi_{2}(\pi_{m}(\hat y))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma \stackrel{\bullet}{\simeq} \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{2}(\pi_{1}(\hat y')),\ldots,\allowbreak\pi_{2}(\pi_{m}(\hat y'))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma \stackrel{\bullet}{\simeq} \linebreak\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{penc}(\mathsf{pk}(sk_R),m''_1,d_1),\dots,\mathsf{penc}(\mathsf{pk}(sk_R),m''_n,d_n)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ it is the case that $$\begin{array}{lcl}
\pi_{3}(\pi_{i}(\hat y))\sigma &=_E& \mathsf{ballotPf}(PK_{T_i},R_i,N_i,\mathsf{pk}(sk_R),S_i,d_{\chi(i)}) \\
\pi_{3}(\pi_{i}(\hat y'))\sigma &=_E& \mathsf{ballotPf}(PK'_{T_i},R'_i,N'_i,\mathsf{pk}(sk_R),S'_i,d_{\chi'(i)})
\end{array}$$ for some terms $PK_{T_i}, R_i, N_i, S_i, PK'_{T_i},R'_i,N'_i,S'_i$ and permutations $\chi,\chi'$ defined over $\{1,\allowbreak\dots,n\}$. Since for all $1\leq i \leq m$ the name $d_i$ is under restriction in the voting process specification, it follows that $$\begin{array}{lcl}
\pi_{3}(\pi_{i}(\hat y))\sigma &=_E& \mathsf{ballotPf}(\mathsf{pk}(sk_T),m_{\chi(i)},s_{\chi(i)},\mathsf{pk}(sk_R),m'_{\chi(i)},d_{\chi(i)}) \\
\pi_{3}(\pi_{i}(\hat y'))\sigma &=_E& \mathsf{ballotPf}(\mathsf{pk}(sk_T),m_{\chi'(i)},s_{\chi'(i)},\mathsf{pk}(sk_R),m'_{\chi'(i)},d_{\chi'(i)})
\end{array}$$ (that is, $\pi_{3}(\pi_{i}(\hat y))\sigma$ and $\pi_{3}(\pi_{i}(\hat y'))\sigma$ are the signature proofs of knowledge output by the voters) and, moreover, by the validity of the proof, we have $$\begin{array}{lcl}
\pi_{1}(\pi_{i}(\hat y))\sigma &=_E& \mathsf{penc}(\mathsf{pk}(sk_T),m_{\chi(i)},s_{\chi(i)})\\
\pi_{1}(\pi_{i}(\hat y'))\sigma &=_E& \mathsf{penc}(\mathsf{pk}(sk_T),m_{\chi'(i)},s_{\chi'(i)})
\end{array}$$ $$\begin{array}{lcl}
\pi_{2}(\pi_{i}(\hat y))\sigma &=_E& \mathsf{penc}(\mathsf{pk}(sk_R),m'_{\chi(i)},d_{\chi(i)})\\
\pi_{2}(\pi_{i}(\hat y'))\sigma &=_E& \mathsf{penc}(\mathsf{pk}(sk_R),m'_{\chi'(i)},d_{\chi'(i)})
\end{array}$$ Since $\bigwedge_{i=1}^{m} \pi_{4}(\hat y) =_E{\varnothing}$ and $\bigwedge_{i=1}^{m} \pi_{4}(\hat y') =_E{\varnothing}$, it follows for all $1\leq i \leq m$ that $\pi_{i}(\hat y) =_E\pi_{i}(\hat y)$. Finally, $\mathsf{snd}^m(\hat y) =_E\mathsf{snd}^m(\hat y') =_E{\varnothing}$ and hence we conclude $\hat y \sigma\simeq \hat y'\sigma$.
6. Suppose $C$ is a context and $B$ is a process such that $C[{\sf VP^+_n}(s_1,\dots,\allowbreak s_n)] \mathrel{(\to^* \xrightarrow{\alpha} \to^*)^*} B$, $\varphi(B)\equiv\nu\tilde n.\sigma$, and $\bigwedge_{1 \leq i \leq n} \Phi^{IV}_i\{\textnormal{\raisebox{2pt}{\footnotesize $\pi_{i}(\hat y){y}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $\}$}} \sigma \wedge \Phi^{EV}_n\{^{\hat w'}/_{\hat w} \} \sigma \mathrel\wedge \mathsf{snd}^n(\hat w)\sigma =_E{\varnothing}$ holds. For all $1 \leq i \leq n$, we have $\pi_{i}(\hat w)\sigma = \pi_{2}(r_{cred_i})\sigma$. Since $\mathsf{snd}^n(\hat w)\sigma =_E{\varnothing}$ and, by inspection of the voting process, we have $$\hat w\sigma =_E(\mathsf{sign}(ssk_R,\mathsf{penc}(\mathsf{pk}(sk_R),m''_1,d_1)),\dots,\mathsf{sign}(ssk_R,\mathsf{penc}(\mathsf{pk}(sk_R),m''_n,d_n)))$$ In addition, we have $\pi_{2}(\pi_{i}(\hat y))\sigma =_E\mathsf{penc}(\mathsf{pk}(sk_R),m'_i,d_i)$ for all $1 \leq i \leq n$ and by similar reasoning to the above (see Condition
[evCond1]) we derive $\hat w\sigma \simeq \hat w'\sigma$.
7. This can be witnessed by modelling the complete JCJ-Civitas protocol as the context $C[\_]$.
◻
*Proof.* Let ${\sf DAA_{RSA}}$ be the augmented Direct Anonymous Attestation biprocess derived from the specification $\langle \sf{Join}_{RSA}, \sf{Sign}_{RSA} \rangle$. Let us consider the evaluation context $$\begin{array}{lcl}
C[\_] &=& \overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(sk_I),\texttt{bsn}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.\\
&& c(w).c(x).\overline{c}\langle\mathsf{penc}(w,n,n_e)\rangle.c(z_a).\textnormal{if } z_a=\mathsf{hash}(n_e,\pi_{2}(x)) \textnormal{ then }\\
&& \overline{c}\langle n_i\rangle.c(z_s).\overline{c}\langle\mathsf{clsign}(sk_I,e,v'',\pi_{2}(x))\rangle.\\
&& c(w').c(x').\overline{c}\langle\mathsf{penc}(w',n,n_e)\rangle.c(z'_a).\textnormal{if } z'_a=\mathsf{hash}(n_e,\pi_{2}(x')) \textnormal{ then }\\
&& \overline{c}\langle n_i\rangle.c(z'_s).\overline{c}\langle\mathsf{clsign}(sk_I,e,v'',\pi_{2}(x'))\rangle.\\
&& \overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\texttt{bsn},{\sf msg}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.\overline{c}\langle n_v\rangle.c(y).
\textnormal{if } \pi_{1}(x)=\pi_{3}(y) \textnormal{ then } \overline{b}\langle{\sf fail}\rangle \textnormal{ else }0\mid\_
\end{array}$$ We have $$\textnormal{fst}(C[{\sf DAA_{RSA}}]) \xrightarrow{}^* C'[\textnormal{if }
\mathsf{commit}(\texttt{tsk},\zeta_I)=\mathsf{commit}(\texttt{tsk},\zeta) \textnormal{ then } \overline{b}\langle{\sf fail}\rangle \textnormal{ else }0]$$ and $$\textnormal{snd}(C[{\sf DAA_{RSA}}]) \xrightarrow{}^* C'[\textnormal{if }
\mathsf{commit}(\texttt{tsk},\zeta_I)=\mathsf{commit}(\texttt{tsk}',\zeta) \textnormal{ then } \overline{b}\langle{\sf fail}\rangle \textnormal{ else }0]$$ where $$\begin{array}{lcl}
\texttt{tsk}&=& \mathsf{hash}(\mathsf{hash}(\texttt{DAASeed},\mathsf{hash}(\mathsf{pk}(sk_I))),\texttt{cnt},\mathsf{0})\\
\texttt{tsk}'&=& \mathsf{hash}(\mathsf{hash}(\texttt{DAASeed}',\mathsf{hash}(\mathsf{pk}(sk_I))),\texttt{cnt}',\mathsf{0})\\
\zeta_I &=& \mathsf{hash}(\mathsf{0},\texttt{bsn})\\
\zeta &=& \mathsf{hash}(\mathsf{0},\texttt{bsn})
\end{array}$$ It follows that $\textnormal{fst}(C[{\sf DAA_{RSA}}]) \not\sim \textnormal{snd}(C[{\sf DAA_{RSA}}])$ because $\textnormal{fst}(C[{\sf DAA_{RSA}}])$ can output on channel $b$, but $\textnormal{snd}(C[{\sf DAA_{RSA}}])$ cannot; and therefore ${\sf DAA_{RSA}}$ does not satisfy user-controlled anonymity. ◻
# Analysis: Restoring user-controlled anonymity
This section provides the scripts used to automatically verify that the revised RSA-based DAA protocol (Section [sec:daa:RSA:solution]) satisfies user-controlled anonymity. The free name declarations, function definitions and equations for the RSA-based DAA process specification appear in Listing [lst:app:example:daa:eq]; the join algorithm $\sf{Join}_{RSA'}$ is presented in Listing [lst:app:example:daa:join], and the sign algorithm $\sf{Sign}_{RSA'}$ appears in Listing [lst:app:example:daa:sign]. Finally, the augmented Direct Anonymous Attestation biprocess ${\sf DAA_{RSA'}}$ is presented in Listing [lst:app:example:daa:anon]. (The nonce `XXTERMINATION` is introduced to avoid an over-approximation issue.) ProVerif can be used to automatically verify observational equivalence of Listing [lst:app:example:daa:anon] and hence the revised RSA-based DAA protocol satisfies user-controlled anonymity.
```
fun accept/0.
fun zero/0.
fun one/0.
fun FJoin/0.
fun FSign/0.
fun clgetnonce/1.
fun clgetprime/1.
fun hash/1.
fun pk/1.
fun commit/2.
fun circ/2.
fun dec/2.
fun open/2.
fun checkclsign/3.
fun checkspk/3.
fun clcommit/3.
fun clopen/3.
fun penc/3.
fun spk/3.
fun clsign/4.
equation dec(k,penc(pk(k),r,m)) = m.
equation clgetprime(clsign(xsk,xprime,xrand,xmsg)) = xprime.
equation clgetnonce(clsign(xsk,xprime,xrand,xmsg)) = xrand.
equation checkclsign(pk(xsk),xmsg,clsign(xsk,xprime,xrand,xmsg))
= accept.
equation open(xrand,commit(xrand,xplain)) = xplain.
equation clopen(x,xrand,clcommit(x,xrand,xplain)) = xplain.
equation clopen(pk(xsk),xrand,clsign(xsk,yprime,yrand,
clcommit(pk(xsk),xrand,xmsg))) = clsign(xsk,yprime,xrand,xmsg).
equation checkspk(FJoin,(xzeta,xpk,commit(xtsk,xzeta),
clcommit(xpk,xv,xtsk),xmsg),
spk(FJoin,(xtsk,xv),(xzeta,xpk,commit(xtsk,xzeta),
clcommit(xpk,xv,xtsk),xmsg))) = accept.
equation checkspk(FSign,(xzeta,pk(xsk),commit(xtsk,xzeta),
clcommit(pk(xsk),xw,clsign(xsk,xe,xv,xtsk)),xmsg),
spk(FSign,(xtsk,xw),(xzeta,pk(xsk),commit(xtsk,xzeta),
clcommit(pk(xsk),xw,clsign(xsk,xe,xv,xtsk)),xmsg))) = accept.
```
```
let join =
in(aj,((pkI,bsnI),DAASeed,cnt,skM));
new v';
let zetaI = hash((zero,bsnI)) in
let tsk = hash((hash((DAASeed,hash(pkI))),cnt,zero)) in
let NI = commit(tsk,zetaI) in
let U = clcommit(pkI,v',tsk) in
out(c,(NI,U));
in(c,encNe);
let ne = dec(skM,encNe) in
out(c,hash((U,ne)));
in(c,ni);
new nt;
out(c,(nt,spk(FJoin,(tsk,v'),(zetaI,pkI,NI,U,(nt,ni)))));
in(c,sig);
let cre = clopen(pkI,v',sig) in
if checkclsign(pkI,tsk,cre) = accept then
out(aj',(cre,tsk)).
```
```
let sign =
in(as,((pkI,bsnI),bsnV,m,cre,tsk,xxTERMINATION));
in(c,nv);
new nt;new w;
if bsnV = bottom then (
new zeta;
let creHat = clcommit(pkI,w,cre) in
let NV = commit(tsk,zeta) in
out(as',(zeta,pkI,NV,creHat,nt,
spk(FSign,(tsk,w),(zeta,pkI,NV,creHat,(nt,nv,m)))))
) else (
let zeta = hash((one,bsnV)) in
let creHat = clcommit(pkI,w,cre) in
let NV = commit(tsk,zeta) in
out(as',(zeta,pkI,NV,creHat,nt,
spk(FSign,(tsk,w),(zeta,pkI,NV,creHat,(nt,nv,m)))))
).
```
```
free c.
free chlP.
free chlM.
fun bottom/0.
let SignerP =
new aj;new aj';new as;new as';( !join )|( !sign )|(
new cnt;new DAASeed;new skM;out(c,pk(skM));
! out(aj,(wparams,DAASeed,cnt,skM));
in(aj',(cre,tsk));
(!
in(c,(xmsg,=bottom));new XXTERMINATION;
out(as,(wparams,bottom,xmsg,cre,tsk,XXTERMINATION));
in(as',z);out(c,z)
)|(!
in(c,(xmsg,xbsn));new XXTERMINATION;
out(as,(wparams,(chlP,xbsn),xmsg,cre,tsk,XXTERMINATION));
in(as',z);out(c,z)
)|(
out(wb,(cre,tsk))
)
).
let Challenge =
new as;new as';( sign ) | (
in(bA,(creA,tskA));
in(bB,(creB,tskB));
let cre = choice[creA,creB] in
let tsk = choice[tskA,tskB] in
(
in(c,(xmsg,=bottom));new XXTERMINATION;
out(as,(wparams,bottom,xmsg,cre,tsk,XXTERMINATION));
in(as',x);out(c,x)
)|(
in(c,(xmsg,xbsn));new XXTERMINATION;
out(as,(wparams,(chlM,xbsn),xmsg,cre,tsk,XXTERMINATION));
in(as',x);out(c,x)
)
).
process
in(c,wparams);new bA;new bB;
(let wb = bA in SignerP)|
(let wb = bB in SignerP)|
(Challenge)
```
#### Optimised analysis.
The ProVerif script in Listing [lst:app:example:daa:anon] has an execution time of 6 minutes 43 seconds By removing the name restrictions on the secret part of the endorsement key for each signer, the execution time is reduced to 92 seconds. This optimised script is presented in Listing [lst:app:example:daa:anon-opt].
```
free c.
free chlP.
free chlM.
free skA,skB.
fun bottom/0.
let SignerP =
new aj;new aj';new as;new as';( !join )|( !sign )|(
new cnt;new DAASeed;
! out(aj,(wparams,DAASeed,cnt,skM));
in(aj',(cre,tsk));
(!
in(c,(xmsg,=bottom));new XXTERMINATION;
out(as,(wparams,bottom,xmsg,cre,tsk,XXTERMINATION));
in(as',z);out(c,z)
)|(!
in(c,(xmsg,xbsn));new XXTERMINATION;
out(as,(wparams,(chlP,xbsn),xmsg,cre,tsk,XXTERMINATION));
in(as',z);out(c,z)
)|(
out(wb,(cre,tsk))
)
).
let Challenge =
new as;new as';( sign ) | (
in(bA,(creA,tskA));
in(bB,(creB,tskB));
let cre = choice[creA,creB] in
let tsk = choice[tskA,tskB] in
(
in(c,(xmsg,=bottom));new XXTERMINATION;
out(as,(wparams,bottom,xmsg,cre,tsk,XXTERMINATION));
in(as',x);out(c,x)
)|(
in(c,(xmsg,xbsn));new XXTERMINATION;
out(as,(wparams,(chlM,xbsn),xmsg,cre,tsk,XXTERMINATION));
in(as',x);out(c,x)
)
).
process
in(c,wparams);new bA;new bB;
(let (wb,skM) = (bA,skA) in SignerP)|
(let (wb,skM) = (bB,skB) in SignerP)|
(Challenge)
```
# ProVerif scripts supporting Chapter [chap:obs]
The proof of claims made in Example [ex:compiler] can be automatically verified using Listing [lst:app:example] as input to ProVerif, and Example [ex:compilerS] can be checked using Listing [lst:app:examplee].
```
free c,k,m,n,s.
query ev:eventM() ==> ev:eventK().
query ev:eventN() ==> ev:eventK().
query ev:eventS() ==> ev:eventK().
process
new a1;new a2;new a3;new a4;new a5;new a6;new a7;new a8;
(
out(a1,a1);in(a3,x); (* sync 1 *)
event eventK();
out(c,k);
out(a5,a5);in(a7,x'); (* sync 2 *)
event eventM();
out(c,m)
)|(
out(a2,a2);in(a6,y); (* sync 2 *)
event eventN();
out(c,n)
)|(
out(a4,a2);in(a8,y); (* sync 3 *)
event eventS();
out(c,s)
)|(
in(a1,x);out(a3,x); (* sync 1 *)
in(a5,x');in(a2,y); out(a7,x');out(a6,y); (* sync 2 *)
in(a4,z);out(a8,z) (* sync 3 *)
)
```
```
free c,k,m,n,s.
fun bot/0.
fun pair/2.
reduc fst(pair(x,y)) = x.
reduc snd(pair(x,y)) = y.
process
new a1;new a2;new a3;new a4;new a5;new a6;new a7;new a8;
(
(* start sync 1 *)
out(a1,choice[a1,pair(c,pair(k,pair(m,bot)))]);
in(a3,x);
(* end sync 1 *)
out(choice[c,fst(x)],choice[k,fst(snd(x))]);
(* start sync 2 *)
out(a5,choice[a5,pair(fst(x),pair(fst(snd(snd(x))),bot))]);
in(a7,x');
(* end sync 2 *)
out(choice[c,fst(x')],choice[m,fst(snd(x'))])
)|(
(* start sync 2 *)
out(a2,choice[a2,pair(c,pair(n,bot))]);
in(a6,y);
(* end sync 2 *)
out(choice[c,fst(y)],choice[n,fst(snd(y))])
)|(
(* start sync 3 *)
out(a4,choice[a4,pair(c,pair(s,bot))]);
in(a8,z);
(* end sync 3 *)
out(choice[c,fst(z)],choice[s,fst(snd(z))])
)|(
in(a1,x);out(a3,x); (* sync 1 *)
in(a5,x');in(a2,y);out(a7,x');out(a6,y); (* sync 2 *)
in(a4,z);out(a8,z) (* sync 3 *)
)
```
# Privacy results using ProSwapper
Chapter [chap:obs] introduces a methodology to automatically analyse equivalence properties between processes which use barrier synchronisation. This technique has been implemented as a tool called ProSwapper which is available online: . More precisely, ProSwapper implements the compiler specified by Definition [def:stageElimWithSwap]. It takes processes with barriers as input and outputs a process, defined over the standard ProVerif syntax, with the possible swapping processes defined by process macros. If ProVerif can prove equivalence for a particular swapping process, then the input script should satisfy observational equivalence. The ProSwapper output included in this appendix was produced by ProSwapper version 0.2 alpha.
Several of the examples in Chapter [chap:obs] have been automatically verified using ProSwapper. Listing [lst:app:example-3-7] models Example [ex:swappingSet] (pp) which can be compiled using ProSwapper to produce Listing [lst:app:example-3-7a], and automatically analysed using ProVerif. (For readability, the swapping process used to prove observational equivalence is included and the alternative swapping processes are omitted.) The remainder of this appendix considers vote privacy in the FOO electronic voting protocol (Section [app:obs:src:FOO]) and privacy in vehicular ad-hoc network (Section [app:obs:src:VANETS])
```
free c,m,n.
process
(
out(c,m);
sync 1;
out(c,choice[m,n])
)|(
sync 1;
out(c,choice[n,m])
)
```
```
free c,m,n.
process
new aaa'1;new aaa'2;new aaa'3;new aaa'4;
(
out(c,m);
out(aaa'1,(n,m,c));
in(aaa'2,(xxx'1,xxx'2,xxx'3));
out(xxx'3,choice[xxx'2,xxx'1])
)|(
out(aaa'3,(m,n,c));
in(aaa'4,(xxx'1,xxx'2,xxx'3));
out(xxx'3,choice[xxx'2,xxx'1])
)|(
in(aaa'3,y1);in(aaa'1,y2);
out(aaa'4,choice[y1,y2]);out(aaa'2,choice[y2,y1])
)
```
# Privacy in electronic voting
Section [sec:obs:FOO] presents an analysis of privacy in the FOO electronic voting protocol. This section provides the scripts used to automatically perform this analysis. The free name declarations, function definitions and equations appear in Listing [lst:app:example:foo:eq]. The encoding (Listing [lst:app:example:foo:proc]) of vote privacy follows immediately from pp and this script can be provided as input to ProSwapper to produce Listing [lst:app:example:foo:procA]. This listing can be automatically analysed with ProVerif.
```
free c.
free skR,skA,skB.
fun s/0.
fun s'/0.
fun true/0.
fun blind/2.
fun unblind/2.
fun open/2.
fun commit/2.
fun pk/1.
fun getmsg/1.
fun sign/2.
fun checksign/2.
equation unblind(x,sign(y,blind(x,z))) = sign(y,z).
equation unblind(x,blind(x,y)) = y.
equation open(x,commit(x,y)) = y.
equation checksign(pk(x),sign(x,y)) = true.
equation getmsg(sign(x,y)) = y.
```
```
let foo =
new k;new k';
let M = commit(k,Xvote) in
let MM = blind(k',M) in
out(c,(pk(Xsk),sign(Xsk,MM)));
in(c,y);
if checksign(pk(skR),y) = true then
if getmsg(y) = MM then
let M' = unblind(k',y) in
sync 1;
out(c,(M,M'));
sync 2;
in(c,(z,=M,=M'));
out(c,(z,k)).
process
(let (Xsk,Xvote) = (skA,choice[s,s']) in foo)
| (let (Xsk,Xvote) = (skB,choice[s',s]) in foo)
```
```
process
new aaa'1;new aaa'2;new aaa'3;new aaa'4;
new aaa'5;new aaa'6;new aaa'7;new aaa'8;
(
let (Xsk,Xvote) = (skA,choice[s(),s'()]) in
new k;new k';
let M = commit(k,Xvote) in
let MM = blind(k',M) in
out(c, (pk(Xsk),sign(Xsk,MM)));
in(c, y);
if checksign(pk(skR),y) = true() then
if getmsg(y) = MM then
let M' = unblind(k',y) in
out(aaa'1, (k,M',M,c));
in(aaa'2, (xxx'1,xxx'2,xxx'3,xxx'4));
out(xxx'4, (xxx'3,xxx'2));
out(aaa'3, (xxx'1,xxx'4,xxx'2,xxx'3));
in(aaa'4, (xxx'1,xxx'2,xxx'3,xxx'4));
in(xxx'2, (z,=xxx'4,=xxx'3));
out(xxx'2, (z,xxx'1))
)|(
let (Xsk,Xvote) = (skB,choice[s'(),s()]) in
new k;new k';
let M = commit(k,Xvote) in
let MM = blind(k',M) in
out(c, (pk(Xsk),sign(Xsk,MM)));
in(c, y);
if checksign(pk(skR),y) = true() then
if getmsg(y) = MM then
let M' = unblind(k',y) in
out(aaa'5, (k,M',M,c));
in(aaa'6, (xxx'1,xxx'2,xxx'3,xxx'4));
out(xxx'4, (xxx'3,xxx'2));
out(aaa'7, (xxx'1,xxx'4,xxx'2,xxx'3));
in(aaa'8, (xxx'1,xxx'2,xxx'3,xxx'4));
in(xxx'2, (z,=xxx'4,=xxx'3));
out(xxx'2, (z,xxx'1))
)|(
in(aaa'5, y1);in(aaa'1, y2);
out(aaa'6,choice[y1,y2]);out(aaa'2,choice[y2,y1]);
in(aaa'7, y3);in(aaa'3, y4);
out(aaa'8,choice[y3,y3]);out(aaa'4,choice[y4,y4])
)
```
# Privacy in vehicular ad-hoc networks
Dahl, Delaune & Steel (**Delaune10:Vanets?**) adopt the notion of swapping defined in (**Smyth08:Obs?**) to analyse privacy in the CMIX vehicular ad-hoc networking protocol (**Freudiger07:CMIX-vanet-protocol?**). In this section, (**Delaune10:Vanets?**) will be revisited to show that ProSwapper can be used to automatically prove privacy. First, we recall the model used by Dahl, Delaune & Steel. Listing [lst:app:example:vanets:eq] contains the free name declarations, function definitions and equations as specified by (**Delaune10:Vanets?**); and Listings [lst:app:example:vanets:proc] & [lst:app:example:vanets:procA] present the ProVerif script manually derived using (**Smyth08:Obs?**) (see (**Delaune10:Vanets?**) for the original encoding without swapping). Listing [lst:app:example:vanets:procB] presents a variant of Listings [lst:app:example:vanets:proc] & [lst:app:example:vanets:procA] written by Dahl, suitable for input to ProSwapper; the relative complexity of the encodings should illustrate the benefits of our abstraction. The ProSwapper input script can be compiled to produce Listing [lst:app:example:vanets:procC], which can be automatically analysed using ProVerif. The execution times are comparable: ProVerif takes 44ms to analyse Listings [lst:app:example:vanets:proc]/[lst:app:example:vanets:procA], and 30ms to analyse Listing [lst:app:example:vanets:procC] (the associated compile time is negligible).
```
free c,ack,request.
free enterLeft,enterRight,zone,exitLeft,exitRight.
private free sk.
private free prsu,krsu,kc.
private free pva1,kva1,pva2,kva2,pvb1,kvb1,pvb2,kvb2.
fun pk/1.
fun sign/2.
fun enc/2.
fun senc/3.
reduc getmess(sign(x,y)) = x.
reduc checksign(sign(x,y),pk(y)) = x.
reduc decrypt(enc(x,pk(y)),y) = x.
reduc sdecrypt(senc(x,y,r),y) = x.
```
```
let rsu =
in(c,X);
let (SignaturePart,CertificatePart) = X in
let (Pv,PkKv) = checksign(CertificatePart,pk(kc)) in
let (=request,Ts,=Pv) = checksign(SignaturePart,PkKv) in
out(c,(enc(sign((Pv,sk,Ts),krsu),PkKv),sign((prsu,pk(krsu)),kc))).
let carBefore =
out(enter,pv1);
new ts;
out(enter,(sign((request,ts,pv1),kv1),sign((pv1,pk(kv1)),kc)));
in(enter,X);
let (encedPart,CertificatePart) = X in
let (Prsu,PkKrsu) = checksign(CertificatePart,pk(kc)) in
let SignaturePart = decrypt(encedPart,kv1) in
let (=pv1,sk,=ts) = checksign(SignaturePart,PkKrsu) in
new r; out(zone,senc(pv1,sk,r));
out(pcPv1,pv1);
out(pcKv1,kv1);
out(pcPv2,pv2);
out(pcKv2,kv2);
out(pcSk,sk);
out(pcExit,exit).
let carAfter =
new r;new r';
out(exit,senc(pv1,sk,r));
out(exit,senc(pv2,sk,r'));
out(exit,pv2).
```
```
process
out(c,pk(kc));out(c,pk(krsu));
(
!rsu
)|(
new pcaExit;new pcaKv1;new pcaKv2;new pcaPv1;new pcaPv2;new pcaSk;
new pcbExit;new pcbKv1;new pcbKv2;new pcbPv1;new pcbPv2;new pcbSk;
(
let (kv1,kv2,pv1,pv2) = (kva1,kva2,pva1,pva2) in
let (pcKv1,pcKv2,pcPv1,pcPv2) = (pcaKv1,pcaKv2,pcaPv1,pcaPv2) in
let enter = enterLeft in
let exit = choice[exitLeft,exitRight] in
let pcExit = pcaExit in
let pcSk = pcaSk in
carBefore
)|(
let (kv1,kv2,pv1,pv2) = (kvb1,kvb2,pvb1,pvb2) in
let (pcKv1,pcKv2,pcPv1,pcPv2) = (pcbKv1,pcbKv2,pcbPv1,pcbPv2) in
let enter = enterRight in
let exit = choice[exitRight,exitLeft] in
let pcExit = pcbExit in
let pcSk = pcbSk in
carBefore
)|(
in(pcaPv1,aPv1);in(pcaKv1,aKv1);in(pcaPv2,aPv2);
in(pcaKv2,aKv2);in(pcaSk,aSk);in(pcaExit,aExit);
in(pcbPv1,bPv1);in(pcbKv1,bKv1);in(pcbPv2,bPv2);
in(pcbKv2,bKv2);in(pcbSk,bSk);in(pcbExit,bExit);
(
let pv1 = choice[aPv1,bPv1] in
let kv1 = choice[aKv1,bKv1] in
let pv2 = choice[aPv2,bPv2] in
let kv2 = choice[aKv2,bKv2] in
let sk = choice[aSk,bSk] in
let exit = choice[aExit,bExit] in
carAfter
)|(
let pv1 = choice[bPv1,aPv1] in
let kv1 = choice[bKv1,aKv1] in
let pv2 = choice[bPv2,aPv2] in
let kv2 = choice[bKv2,aKv2] in
let sk = choice[bSk,aSk] in
let exit = choice[bExit,aExit] in
carAfter
)
)
)
```
```
let rsu =
in(c,X);
let(SignaturePart,CertificatePart) = X in
let(Pv,PkKv) = checksign(CertificatePart,pk(kc)) in
let(=request,Ts,=Pv) = checksign(SignaturePart,PkKv) in
out(c,(enc(sign((Pv,sk,Ts),krsu),PkKv),sign((prsu,pk(krsu)),kc))).
let car =
out(enter,pv1);
new ts;
out(enter,(sign((request,ts,pv1),kv1),sign((pv1,pk(kv1)),kc)));
in(enter,X);
let(encedPart,CertificatePart) = X in
let(Prsu,PkKrsu) = checksign(CertificatePart,pk(kc)) in
let SignaturePart = dec(encedPart,kv1) in
let(=pv1,sk,=ts) = checksign(SignaturePart,PkKrsu) in
new r;
out(zone,senc(pv1,sk,r));
sync 1;
new r;
new r';
out(exit,senc(pv1,sk,r));
out(exit,senc(pv2,sk,r'));
out(exit,pv2).
process
out(c,pk(kc));
out(c,pk(krsu));
(
!rsu
)|(
let (kv1,kv2,pv1,pv2) = (kva1,kva2,pva1,pva2) in
let enter = enterLeft in
let exit = choice[exitLeft,exitRight] in
car
)|(
let (kv1,kv2,pv1,pv2) = (kvb1,kvb2,pvb1,pvb2) in
let enter = enterRight in
let exit = choice[exitRight,exitLeft] in
car
)
```
```
process new aaa'1;new aaa'2;new aaa'3;new aaa'4;
out(c,pk(kc));out(c,pk(krsu));
(!
in(c,X);
let (SignaturePart,CertificatePart) = X in
let (Pv,PkKv) = checksign(CertificatePart,pk(kc)) in
let (=request,Ts,=Pv) = checksign(SignaturePart,PkKv) in
out(c,(enc(sign((Pv,sk,Ts),krsu),PkKv),sign((prsu,pk(krsu)),kc)))
)|(
let (kv1,kv2,pv1,pv2) = (kva1,kva2,pva1,pva2) in
let enter = enterLeft in
let exit = choice[exitLeft,exitRight] in
out(enter,pv1);new ts;
out(enter,(sign((request,ts,pv1),kv1),sign((pv1,pk(kv1)),kc)));
in(enter,X);
let (encedPart,CertificatePart) = X in
let (Prsu,PkKrsu) = checksign(CertificatePart,pk(kc)) in
let SignaturePart = dec(encedPart,kv1) in
let (=pv1,sk,=ts) = checksign(SignaturePart,PkKrsu) in
new r;out(zone,senc(pv1,sk,r));
out(aaa'1,(pv2,sk,pv1,exit));
in(aaa'2,(xxx'1,xxx'2,xxx'3,xxx'4));
new r;new r';
out(xxx'4,senc(xxx'3,xxx'2,r));out(xxx'4,senc(xxx'1,xxx'2,r'));
out(xxx'4,xxx'1)
)|(
let (kv1,kv2,pv1,pv2) = (kvb1,kvb2,pvb1,pvb2) in
let enter = enterRight in
let exit = choice[exitRight,exitLeft] in
out(enter,pv1);new ts;
out(enter,(sign((request,ts,pv1),kv1),sign((pv1,pk(kv1)),kc)));
in(enter,X);
let (encedPart,CertificatePart) = X in
let (Prsu,PkKrsu) = checksign(CertificatePart,pk(kc)) in
let SignaturePart = dec(encedPart,kv1) in
let (=pv1,sk,=ts) = checksign(SignaturePart,PkKrsu) in
new r;out(zone,senc(pv1,sk,r));
out(aaa'3,(pv2,sk,pv1,exit));
in(aaa'4,(xxx'1,xxx'2,xxx'3,xxx'4));
new r;new r';
out(xxx'4,senc(xxx'3,xxx'2,r));out(xxx'4,senc(xxx'1,xxx'2,r'));
out(xxx'4,xxx'1)
)|(
in(aaa'3,y1);in(aaa'1,y2);
out(aaa'4,choice[y1,y2]);out(aaa'2,choice[y2,y1])
)
```
[^1]: The RSA-based DAA protocol (**Chen04:RSA-DAA?**) does not explicitly specify how the issuer learns a trusted platform’s public endorsement key during an execution of the join algorithm. However, it seems reasonable to assume that the public key would be sent as plaintext. By contrast, Cesena *et al.* (**Sadeghi10:TLS-DAA?**; **Cesena10?**) define an extension of RSA-based DAA which uses TLS to hide the affiliation between groups and trusted platforms; this variant would thwart a passive adversary, but not corrupt administrators.
[^2]: The use of two distinct channel names for the input and output channels is not strictly necessary; however, it aids automation. In particular, it helps avoid a ProVerif incompleteness issue that arises because there is no distinction between messages input and messages output on a particular channel.
[^3]: Note that $\zeta^{\tilde{r}_f} \equiv \zeta^{f_0 + f_1 2^{l_f}} \pmod{\Gamma}$ and the order of $\rho < \Gamma$ the calculation $\zeta^{\tilde{r}_f} \pmod{\Gamma}$ will involve a smaller exponential thus providing a performance gain.
