**Definition 7** (Validity of injective correspondence property). *Let $E$ be an equational theory, and $A_0$ an extended process. We say that $A_0$ *satisfies the injective correspondence property* $\overline{f}\langle M\rangle \rightsquigarrow \mathsf{inj}\;\overline{g}\langle N\rangle$ if for all execution paths $$A_0 \to^*\xrightarrow{\alpha_1}\to^*
A_1 \to^*\xrightarrow{\alpha_2}\to^*
\dots \to^*\xrightarrow{\alpha_n}\to^* A_n,$$ there exists a partial injective function $h:\{1,\ldots,n\} \xrightarrow{}\{1,\ldots,n\}$ such that for all $i\in\{1,\ldots,n\}$, substitution $\sigma$ and variable $e$ such that $\alpha_i=\nu\,e.\overline{f}\langle e\rangle$ and $e\varphi(A_i)=_EM\sigma$, then the following conditions are satisfied: (1) $h(i)$ is defined; (2) $\alpha_{h(i)}=\nu\,e'.\overline{g}\langle e'\rangle$ for some $e'$ such that $e'\varphi(A_{h(i)})=_EN\sigma$; and, (3) $h(i)
Returning to our Handshake protocol, observe that authentication of ${\ensuremath{\mathcal{C}}}$ is injective; that is, if ${\ensuremath{\mathcal{S}}}$ reaches the end of the protocol with the belief that she has session key $k$ with interlocutor ${\ensuremath{\mathcal{C}}}$, then she has indeed done so; and moreover, ${\ensuremath{\mathcal{C}}}$ has done so in this session (that is, there is an injective relationship).
**Example 5** (Reasoning with correspondence, revisited). *Consider the annotated Hand-shake protocol and observe the injective correspondence property $$\overline{completedS}\langle{\ensuremath{\mathsf{pair}(y,{\ensuremath{\mathsf{true}}})}}\rangle \allowbreak\rightsquigarrow \mathsf{inj}\;\overline{startedC}\langle y\rangle$$ is valid. To show this conclusively, one has to consider all the possible execution paths, and show that for each of them, whenever there is a label $\nu\,e.\overline{completedS}\langle e\rangle$ associated with the substitution $\{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}(M,{\ensuremath{\mathsf{true}}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $e$}}\}$, then there is an earlier label $\nu\,e'.\overline{startedC}\langle e'\rangle$ and substitution $\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $e'$}}\}$; such that no two occurrences of the event $completedS$ are mapped to the same event $startedC$. ProVerif can be used to prove this result.*
## Fixing the Handshake protocol
As mentioned in Section 1, the man-in-the-middle attack that is illustrated in Figure 1 can be avoided by putting the participants’ public keys along with $k$ in the signature formed by ${\ensuremath{\mathcal{S}}}$. The resulting process looks like this: $$\begin{array}{llcl}
& P &\triangleq& \nu\,sk_{{\ensuremath{\mathcal{S}}}}.\nu\,sk_{{\ensuremath{\mathcal{C}}}}.\nu\,s.\\
&&& \textnormal{let } pk_{S}={\ensuremath{\mathsf{pk}(sk_{{\ensuremath{\mathcal{S}}}})}} \textnormal{ in } \textnormal{let } pk_{C}={\ensuremath{\mathsf{pk}(sk_{{\ensuremath{\mathcal{C}}}})}} \textnormal{ in }\\
&&& (\overline{c}\langle pk_{S}\rangle \mid \overline{c}\langle pk_{C}\rangle \mid {!P_{{\ensuremath{\mathcal{S}}}}} \mid {!P_{{\ensuremath{\mathcal{C}}}}})\\
\\
& P_{{\ensuremath{\mathcal{S}}}} &\triangleq& c(x\_pk).\nu\,k.\overline{c}\langle{\ensuremath{\mathsf{aenc}(x\_pk,{\ensuremath{\mathsf{sign}(sk_{{\ensuremath{\mathcal{S}}}},{\ensuremath{\mathsf{pair}(pk_{S},{\ensuremath{\mathsf{pair}(x\_pk,k)}})}})}})}}\rangle.\\
& && c(z).\textnormal{if } {\ensuremath{\mathsf{fst}({\ensuremath{\mathsf{sdec}(k,z)}})}}=tag \textnormal{ then }Q\\
\\
& P_{{\ensuremath{\mathcal{C}}}} &\triangleq& c(y).\textnormal{let } y'={\ensuremath{\mathsf{adec}(sk_{{\ensuremath{\mathcal{C}}}},y)}} \textnormal{ in }\textnormal{let } y''={\ensuremath{\mathsf{snd}({\ensuremath{\mathsf{getmsg}(y')}})}} \textnormal{ in }\\
& && \textnormal{if } {\ensuremath{\mathsf{fst}(y'')}}=pk_{C} \textnormal{ then }\\
& && \textnormal{if } {\ensuremath{\mathsf{checksign}(pk_{S},y')}}={\ensuremath{\mathsf{true}}} \textnormal{ then }\\
& && \overline{c}\langle{\ensuremath{\mathsf{senc}({\ensuremath{\mathsf{snd}(y'')}},{\ensuremath{\mathsf{pair}(tag,s)}})}}\rangle\\
\end{array}$$ As an exercise the reader may like to identify exactly which step of the attack of Figure 1 fails for the revised protocol.
We remark that the injective correspondence property $\overline{completedC}\langle{\ensuremath{\mathsf{pair}(x,y)}}\rangle \rightsquigarrow \mathsf{inj}\;\overline{startedS}\langle\allowbreak{\ensuremath{\mathsf{pair}(x,y)}}\rangle$ does not hold, because the client cannot ascertain as to whether the initial message he receives is fresh. However, this does not affect the security of the protocol’s high-level objective which is to enable the client ${\ensuremath{\mathcal{C}}}$ to share the secret $s$ with the server ${\ensuremath{\mathcal{S}}}$.
# Equivalence properties
The notion of indistinguishability is a powerful concept which allows us to reason about complex properties that cannot be expressed as secrecy or correspondence properties. Intuitively, two processes are said to be equivalent if an observer has no way to tell them apart. The processes may be handling different data, and internally performing quite different computations, but they look the same to an external observer. This notion allows us to define strong notions of secrecy and privacy.
A natural starting point for defining observational equivalence says that processes $A$ and $B$ are equivalent if they can output on the same channels, no matter what the context they are placed inside. Formally we write $A\Downarrow c$ when $A$ can evolve to a process that can send a message on channel $c$, that is, when $A\to^*C[\overline{c}\langle M\rangle.P]$ for some term $M$, process $P$ and evaluation context $C[\_]$ that does not bind $c$. This then allows us to characterise equivalence as follows: for all contexts $C[\_]$, we have $C[A]\Downarrow c$ if and only if $C[B]\Downarrow c$. One might think that this condition is too weak – it should say that $C[A]$ and $C[B]$ output the *same term* on the channel $c$ – but that is not necessary, since if two processes output different terms then a context that inspects the output could be constructed to distinguish them.
## Observational equivalence
In practice, the definition motivated above is hard to compute, and instead a stronger definition is often used. The stronger definition, called observational equivalence, has a recursive character. Roughly speaking, processes $A$ and $B$ are said to be observationally equivalent if they can output on the same channel for all contexts they are placed inside (as before); and also, for all contexts and every step made by $A$ inside the context, there exists a step that $B$ can make (inside the context), such that the resulting pair of processes are observationally equivalent (and vice-versa). We avoid the circularity of this informal characterisation, and define it rigorously as follows.
**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[\_]$.*
Note that we insist that $\mathrel{\mathcal{R}}$ is symmetric, so we can state the Conditions 1 and 2 in a non-symmetric way (the symmetric part is guaranteed by the symmetry of $\mathrel{\mathcal{R}}$). Note also the added condition that the two processes have the same domain; this captures the ‘observable’ difference between processes in which the value of a variable appearing in one frame, is not defined in the other.
A classical example illustrates the difference between observational equivalence and the notion of equivalence mentioned at the start of Section 1 (sometimes called *trace equivalence*). Intuitively, trace equivalence checks that the outputs on the traces allowed by $C[A]$ are the same as those of $C[B]$, but it does not enforce that *decisions* inside $A$ and $B$ occur at the same point. Let us use the notation $A_1+A_2$ to mean the non-deterministic choice of $A_1$ or $A_2$. This is expressible in applied pi, as follows: $$A_1+A_2 \triangleq\nu\,a . (\overline{a}\langle\textrm{left}\rangle\mid\overline{a}\langle\textrm{right}\rangle\mid a(x).\textnormal{if } x=\textrm{left} \textnormal{ then } A_1 \textnormal{ else }A_2)$$ Here, left and right are names, and a scheduler chooses which message output $\overline{a}\langle\textrm{left}\rangle$ or $\overline{a}\langle\textrm{right}\rangle$ to perform, and hence whether $A_1$ or $A_2$ runs. Note that only one of $A_1$ and $A_2$ runs, in contrast with $A_1\mid
A_2$; moreover, only one of the outputs $\overline{a}\langle\textrm{left}\rangle$, $\overline{a}\langle\textrm{right}\rangle$ may occur, because there is only one input $a(x)$, and $a$ is restricted. Now consider the processes $A \triangleq\overline{d}\langle b_1\rangle.\overline{d}\langle b_2\rangle+\overline{d}\langle b_1\rangle.\overline{d}\langle b_3\rangle$ and $B \triangleq\overline{d}\langle b_1\rangle.(\overline{d}\langle b_2\rangle+\overline{d}\langle b_3\rangle)$. One can see that they are trace equivalent, by experimenting with a variety of contexts. However, in $A$ the decision between outputting $b_2$ or $b_3$ is taken earlier than it is in $B$. Observational equivalence captures this as an observable difference. Consider the context $C[\_]=\_\mid d(y)$. Although $C[A]$ and $C[B]$ have the same output capabilities, $C[B]$ can evolve to a process (namely $\overline{d}\langle b_2\rangle+\overline{d}\langle b_3\rangle$) which is not equivalent to any process that $C[A]$ can evolve to (namely, the processes $\overline{d}\langle b_2\rangle$ or $\overline{d}\langle b_3\rangle$).
## Labelled bisimilarity
The quantification over contexts makes the definition of observational equivalence hard to use in practice. Therefore, labelled bisimilarity is introduced, which is more suitable for both manual and automatic reasoning. Labelled bisimilarity relies on an equivalence relation between frames, called static equivalence, which we define first. Intuitively, two frames are statically equivalent if no ‘test’ $M=N$ can tell them apart, where $M$ and $N$ have variables that are substituted from the frame. Formally:
**Definition 2** (Static equivalence). *Two closed frames $\varphi$ and $\psi$ are statically equivalent, denoted $\varphi \approx_s \psi$, if $\textnormal{dom}(\varphi) = \textnormal{dom}(\psi)$ and there exists a set of names $\tilde n$ and substitutions $\sigma,\tau$ such that $\varphi\equiv \nu\,\tilde{n}.\sigma$ and $\psi
\equiv \nu\,\tilde{n}.\tau$ and for all terms $M,N$ such that $\tilde{n} \cap (\textnormal{fn}(M)
\cup \textnormal{fn}(N)) = \emptyset$, we have $M\sigma =_EN\sigma$ holds if and only if $M\tau =_EN\tau$ holds. We say two closed extended processes $A,B$ are statically equivalent, and write $A \approx_s
B$, when their frames are statically equivalent; that is, $\varphi(A) \approx_s
\varphi(B)$.*
The relation is called *static* equivalence because it only examines the current state of the processes (as represented by their frames), and not the processes’ dynamic behaviour (that is, the ways in which they may execute in the future). Thus, two processes are statically equivalent if they cannot be distinguished on the basis of their output so far. Static equivalence captures the static part of observational equivalence. More precisely, observational equivalence and static equivalence coincide on frames. Static equivalence can straightforwardly be shown to be closed under structural equivalence, internal reduction and application of closing evaluation contexts.
**Example 1** (Static equivalence). *In the following examples we assume the signature $\Sigma_S = \{\mathsf{hash},\mathsf{fst},\mathsf{snd},\mathsf{pair}\}$ and the smallest equational theory $E_S$ satisfying the equations ${\ensuremath{\mathsf{fst}({\ensuremath{\mathsf{pair}(x,y)}})}}=x$, ${\ensuremath{\mathsf{snd}({\ensuremath{\mathsf{pair}(x,y)}})}}=y$ over all variables $x,y$, where as expected $\mathsf{hash}$, $\mathsf{fst}$, $\mathsf{snd}$ are unary functions and $\mathsf{pair}$ is a binary function.*
- *$\nu\,m.\{\textnormal{\raisebox{2pt}{\footnotesize $m$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\} \approx_s
\nu\,n.\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$; trivial, since they are structurally equivalent.*
- *$\nu\,m.\{\textnormal{\raisebox{2pt}{\footnotesize $m$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\} \approx_s
\nu\,n.\{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{hash}(n)}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$.*
- *$\{\textnormal{\raisebox{2pt}{\footnotesize $m$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\} \not\approx_s \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{hash}(m)}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$. The first one satisfies $x=m$ but the second one does not.*
- *$\nu\,k.\{\textnormal{\raisebox{2pt}{\footnotesize $k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\mid\nu\,s.\{\textnormal{\raisebox{2pt}{\footnotesize $s$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\approx_s\nu\,k.(\{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{hash}({\ensuremath{\mathsf{pair}(a,k)}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\mid\{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{hash}({\ensuremath{\mathsf{pair}(b,k)}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}$.*
- *$\nu\,k.\{\textnormal{\raisebox{2pt}{\footnotesize $k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\mid\nu\,s.\{\textnormal{\raisebox{2pt}{\footnotesize $s$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\not\approx_s\nu\,k.(\{\textnormal{\raisebox{2pt}{\footnotesize $k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\mid\{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{hash}(k)}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\})$, since the second one satisfies ${\ensuremath{\mathsf{hash}(x)}}=y$ and the first one does not.*
- *$\nu\,s.\{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}(s,s)}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\not\approx_s\nu\,s.\{\textnormal{\raisebox{2pt}{\footnotesize $s$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$, since the first one satisfies ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{fst}(x)}},{\ensuremath{\mathsf{snd}(x)}})}}=x$ but the second one does not.*
As mentioned, static equivalence captures the static part of observational equivalence. The following definition of labelled bisimilarity captures the dynamic part.
**Definition 3** (Labelled bisimilarity). *Labelled bisimilarity ($\approx_l$) is the largest symmetric relation $\mathcal{R}$ on closed extended processes such that $A \mathrel{\mathcal{R}}B$ implies:*
1. *$A \approx_s B$;*
2. *if $A \xrightarrow{}A'$, then $B \xrightarrow{}^* B'$ and $A' \mathrel{\mathcal{R}}B'$ for some $B'$;*
3. *if $A \xrightarrow{\alpha} A'$ and $\textnormal{fv}(\alpha) \subseteq \textnormal{dom}(A)$ and $\textnormal{bn}(\alpha) \cap \textnormal{fn}(B) = \emptyset$; then $B\xrightarrow{}^*\xrightarrow{\alpha}\xrightarrow{}^* B'$ and $A' \mathrel{\mathcal{R}}B'$ for some $B'$.*
Clauses 2 and 3 of this definition correspond to classical notions of bisimilarity (**Milner99?**). Notice the use of the “largest relation” construction, to allow us to insist that the processes $A'$ and $B'$ are again within the relation. Clause 1 asserts static equivalence at each step of the bisimulation.
Let us now consider the side condition of Clause 3. Recall that there are three possibilities for $\alpha$, namely $c(M)$, $\overline{c}\langle u\rangle$, and $\nu u.\overline{c}\langle u\rangle$, where $u$ is either a channel name or a variable of base type. In Clause 3, $\alpha$ can have free variables (in the cases $c(M)$ and $\overline{c}\langle u\rangle$), but any such variables must be defined by the frame of $A$ (and since $A \approx_s B$, also by the frame of $B$). Hence the condition $\textnormal{fv}(\alpha) \subseteq \textnormal{dom}(A)$. The label $\alpha$ can also have bound names (in the case $\nu d.\overline{c}\langle d\rangle$, where $d$ is a channel name), in which case the transition $A\xrightarrow{\alpha}A'$ has the effect of removing the restriction on a bound channel name. That channel must not occur free in $B$, to avoid confusing the restricted name with the global name; hence the condition $\textnormal{bn}(\alpha) \cap \textnormal{fn}(B) = \emptyset$. To see this in more detail, consider $A,B$ such that $A\approx_l B$, and suppose $a\in\textnormal{fn}(B) \backslash \textnormal{fn}(A)$. (For example, $A$ is $0$ and $B$ is $\textnormal{if } a=b \textnormal{ then }{\overline{c}\langle a\rangle}$.) Intuitively, we would like $A\mid(\nu a.\overline{c}\langle a\rangle)\approx_l B\mid(\nu a.\overline{c}\langle a\rangle)$. But to achieve that, we need the side condition, for otherwise the transition $A\mid(\nu a.\overline{c}\langle a\rangle) \xrightarrow{\nu a.\overline{c}\langle a\rangle}A$ would have to be matched on the right hand side by $B \mid (\nu a.\overline{c}\langle a\rangle) \xrightarrow{\nu a.\overline{c}\langle a\rangle} B$, which is false.
#### Working with labelled bisimilarity.
To show labelled bisimilarity of $A$ and $B$, it is necessary to find a symmetric relation $\mathrel{\mathcal{R}}$ that satisfies the conditions contained in Definition 3, such that $A\mathrel{\mathcal{R}}B$. Note that the $\mathrel{\mathcal{R}}$ we find is not required to be the largest one. That is because the set of relations that satisfies the conditions contained in Definition 3 is closed under union. Therefore, the largest one is the union of them all. *Any* relation satisfying the conditions of Definition 3 can serve as a witness to show that two processes are labelled bisimilar. Note also that, although labelled bisimilarity is easily seen to be an equivalence relation, the relation $\mathrel{\mathcal{R}}$ is merely required to be symmetric.
**Example 2** (Labelled bisimilarity). *We prove that for all closed processes $P_1,P_2,C$ and names $\tilde
n$ such that $c\in\tilde n$, we have $\nu\tilde n.(\overline{c}\langle a\rangle.P_1\mid c(x).P_2)\mid C\approx_l
\nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\mid C$. Intuitively, the equivalence holds because the only choice that the left side has, which the right side does not, is an internal reduction (private channel communication). Let $A\mathrel{\mathcal{R}}B$ hold if there exists a closed extended process $C'$ such that one of the following holds:*
- *$A\equiv \nu\tilde n.(\overline{c}\langle a\rangle.P_1\mid c(x).P_2)\mid C'$ and $B\equiv \nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\mid C'$; or*
- *$B\equiv \nu\tilde n.(\overline{c}\langle a\rangle.P_1\mid c(x).P_2)\mid C'$ and $A\equiv \nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\mid C'$; or*
- *$A\equiv B$.*
*One may show that $\mathrel{\mathcal{R}}$ satisfies the conditions contained in Definition
3. First, $\mathrel{\mathcal{R}}$ is easily seen to be symmetric. For the next part, suppose $A\mathrel{\mathcal{R}}B$.*
1. *We show $A\approx_sB$. There are three cases.*
1. *$A\equiv \nu\tilde n.(\overline{c}\langle a\rangle.P_1\mid c(x).P_2)\mid C'$ and $B\equiv \nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\mid C'$. Since $\nu\tilde n.(\overline{c}\langle a\rangle.P_1\mid c(x).P_2)\approx_s\nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})$, we have $A\approx_s B$.*
2. *$B\equiv \nu\tilde n.(\overline{c}\langle a\rangle.P_1\mid c(x).P_2)\mid C'$ and $A\equiv \nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\mid C'$. In this case, a similar argument applies.*
3. *$A\equiv B$ and hence we trivially have $A\approx_s B$.*
2. *Now suppose $A\to A'$. There are again three cases to consider.*
1. *$A\equiv \nu\tilde n.(\overline{c}\langle a\rangle.P_1\mid c(x).P_2)\mid C'$ and $B\equiv \nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\mid C'$. If $A'\equiv \nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\mid C'$, then let $B'\triangleq B$. Otherwise, $A'\equiv \nu\tilde n.(\overline{c}\langle a\rangle.P_1\mid c(x).P_2)\mid C''$ for some $C''$, in which case let $B'\triangleq\nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\mid C''$.*
2. *$A\equiv \nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\mid C'$ and $B\equiv \nu\tilde n.(\overline{c}\langle a\rangle.P_1\mid c(x).P_2)\mid
C'$. Since $B\to A$, it follows that $B\to^*A'$, so let $B' \triangleq A'$.*
3. *$A\equiv B$ and hence the result follows trivially by $B' \triangleq A'$.*
*In all cases we have $A' \mathrel{\mathcal{R}}B'$, as required.*
3. *Now suppose $A\xrightarrow{\alpha} A'$. Again we have three cases:*
1. *$A\equiv \nu\tilde n.(\overline{c}\langle a\rangle.P_1\mid c(x).P_2)\mid C'$ and $B\equiv \nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\mid C'$. Since only the $C'$ part is able to make a labelled transition, $A'\equiv \nu\tilde n.(\overline{c}\langle a\rangle.P_1\mid c(x).P_2)\mid C''$ for some $C''$, in which case let $B'\triangleq\nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\mid C''$, and we have $B\xrightarrow{\alpha} B'$.*
2. *$A\equiv \nu\tilde n.(P_1\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\mid C'$ and $B\equiv \nu\tilde n.(\overline{c}\langle a\rangle.P_1\mid c(x).P_2)\mid
C'$. Since $B\to A$, it follows that $B\to^*\xrightarrow{\alpha}A'$, so let $B' \triangleq A'$.*
3. *$A\equiv B$ and hence the result is trivial by $B' \triangleq A'$.*
*In all cases we have $A' \mathrel{\mathcal{R}}B'$, as required.*
**Lemma 1**. *Given closed extended processes $A,B$ and a closing evaluation context $C[\_]{}$, we have $A\approx_lB$ implies $C[A]\approx_l C[B]$.*
**Theorem 1**. *Observational equivalence and labelled bisimilarity coincide: ${\approx} = {\approx_l}$.*
The condition stating that active substitutions are of base type (Section [sec:syntax]) is crucial to Theorem 1. Without this constraint, one would have the following counterexample: $\nu\,a.(\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\mid x(y).\overline{c}\langle n\rangle) \not\approx \nu\,a.\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ (this can be seen using the closing evaluation context $C[\_] = \overline{x}\langle b\rangle\mid \_$); whereas $\nu\,a.(\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\mid x(y).\overline{c}\langle n\rangle) \approx_l \nu\,a.\{\textnormal{\raisebox{2pt}{\footnotesize $a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$.
## Strong secrecy
Our earlier definition of secrecy required that the secret was not obtained by the adversary. We will now use notions of equivalence to demonstrate a stronger notion of secrecy which states an adversary is unable to distinguish when the secret changes (**Abadi99?**; **CRZ07?**). Intuitively, this means the value of the secret should not effect the observable behaviour of the protocol. Strong secrecy is useful, for example, to capture the adversary’s inability to learn any partial information about the secret.
Strong secrecy is also useful to formalise ‘dictionary attacks’, also known as ‘guessing attacks’, in which the attacker tries all the possible values of the secret until he finds the right one. If a secret is chosen from a relatively small set of possible values, then such an attack might be possible; we call such a secret “weak”. Passwords are often examples of weak secrets. For example, a server which requires the user to send her password $s$, deterministically encrypted with server’s public key $pk$, that is, to send ${\ensuremath{\left\{\!\left|{s}\right|\!\right\}^{\mathsf a}_{pk}}}$, is vulnerable to guessing attacks on $s$. That is because an attacker in possession of ${\ensuremath{\left\{\!\left|{s}\right|\!\right\}^{\mathsf a}_{pk}}}$ can make a guess $s'$ of the password $s$, and check the validity of his guess by constructing ${\ensuremath{\left\{\!\left|{s'}\right|\!\right\}^{\mathsf a}_{pk}}}$ and comparing it with ${\ensuremath{\left\{\!\left|{s}\right|\!\right\}^{\mathsf a}_{pk}}}$. Suppose instead the server requires the user to include a random nonce in the encryption, that is, to send ${\ensuremath{\left\{\!\left|{{\ensuremath{\langle{s},{r}\rangle}}}\right|\!\right\}^{\mathsf a}_{pk}}}$, where $r$ is a nonce chosen from a large set. In that case the system is not vulnerable to guessing attacks.
This may be formalised by the following definitions (**baudet-ccs2005?**; **DelauneKremerRyan:compositionofpassword?**).
**Definition 4**. *Let $\varphi \equiv \nu{n}. \varphi'$ be a frame. We say that $\varphi$ is *resistant to guessing attacks* against ${n}$ if, and only if, $\nu {n}. (\varphi' \mid
\{\textnormal{\raisebox{2pt}{\footnotesize ${n}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize ${x}$}}\}) \approx_s \nu {n}'. \nu
{n}. (\varphi' \mid \{\textnormal{\raisebox{2pt}{\footnotesize ${n}'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize ${x}$}}\})$ where ${n}'$ is a fresh name and ${x}$ is a variable such that $x\not\in \textnormal{dom}(\varphi)$.*
The definition says that the environment cannot distinguish between a situation in which he possesses the correct value of the secret, from another one in which he has some random value instead. This definition can be extended to the more general case.
**Definition 5** (Guessing attacks). *Let $A$ be a process and ${n} \in \textnormal{bn}(A)$. We say that $A$ is *resistant to guessing attacks* against ${n}$ if, for every process $B$ such that $A (\to^*\xrightarrow{\alpha}\to^*)^* B$, then we have that $\varphi(B)$ is resistant to guessing attacks against ${n}$.*
**Example 3** (TPM authentication (**ChenRyan:future?**)). *We consider a protocol where a client ${\ensuremath{\mathcal{A}}}$ shares a secret $s$ with a server ${\ensuremath{\mathcal{B}}}$ (the protocol is based on the one used in the Trusted Platform Module (**TCGspec?**)). In this example, the terms $M$ and $N$ are commonly used for tuples, so it is convenient to introduce a little syntactic sugar to express them. We write $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1,\dots,M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ to mean ${\ensuremath{\mathsf{pair}(M_1,{\ensuremath{\mathsf{pair}(M_2,{\ensuremath{\mathsf{pair}(\dots,{\ensuremath{\mathsf{pair}(M_{n},*)}}\dots)}})}})}}$, where $*$ is any constant. We also write ${\ensuremath{\mathsf{1st}(M)}}$, ${\ensuremath{\mathsf{2nd}(M)}}$, and ${\ensuremath{\mathsf{3rd}(M)}}$ to mean $\textnormal{fst}(M)$, $\textnormal{fst}(\textnormal{snd}(M))$, and $\textnormal{fst}(\textnormal{snd}(\textnormal{snd}(M)))$ respectively. Note that $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1,\ldots,M_k}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$, ${\ensuremath{\mathsf{1st}(N)}}$, etc., are not new functions, but merely syntactic sugar for combinations of functions that we already have. The protocol proceeds as follows. The client sends commands to the server, and authenticates them by supplying a MAC of the command values, keyed on $s$. An additional nonce $n$ is supplied and used in the MAC, to ensure it has high entropy. More precisely, to run the command ‘comm’, ${\ensuremath{\mathcal{A}}}$ sends the message $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\text{comm}, n, {\ensuremath{\mathsf{mac}(s,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\text{comm},n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$})}}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$. ${\ensuremath{\mathcal{B}}}$ checks the MAC by reconstructing it, and if it is correct, sends the response ‘resp’. This protocol may be modelled by the following process $P$, where we assume the signature $\Sigma_T = \Sigma_S \cup \{{\sf mac}\}$ and equational theory $E_S$ (recall that $\Sigma_S$ and $E_S$ were defined in Example
1, and note that binary function ${\sf mac}$ has no equations). $$\begin{array}{llcl}
& P &\triangleq& \nu\,s. ( {!P_A} \mid {!P_B})\\
\\
& P_A &\triangleq& \nu\,n. \overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\text{comm},\, n,\, {\ensuremath{\mathsf{mac}(s,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\text{comm},n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$})}}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle\\
\\
& P_B &\triangleq& c(x). \textnormal{if } {\ensuremath{\mathsf{3rd}(x)}}={\ensuremath{\mathsf{mac}(s,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{{\ensuremath{\mathsf{1st}(x)}},{\ensuremath{\mathsf{2nd}(x)}}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$})}} \textnormal{ then }\overline{c}\langle\text{resp}\rangle
\end{array}$$ $P$ is vulnerable to guessing attacks on $s$. To see this, we consider the transition $$P\xrightarrow{\nu x.\overline{c}\langle x\rangle} \nu s.(\nu n.\{\textnormal{\raisebox{2pt}{\footnotesize $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\text{comm},\, n,\, {\ensuremath{\mathsf{mac}(s,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\text{comm},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 $x$}}\} \mid {!P_A} \mid {!P_B})$$ The frame of this latter process is vulnerable to guessing attacks on $s$, since we have $$\begin{array}{l}
\nu s.\nu n.(\{\textnormal{\raisebox{2pt}{\footnotesize $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\text{comm},\, n,\, {\ensuremath{\mathsf{mac}(s,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\text{comm},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 $x$}}\}\mid \{\textnormal{\raisebox{2pt}{\footnotesize $s$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z$}}\})\\
\qquad{}\not\approx_s
\nu s'.\nu s.\nu n.(\{\textnormal{\raisebox{2pt}{\footnotesize $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\text{comm},\, n,\, {\ensuremath{\mathsf{mac}(s,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\text{comm},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 $x$}}\}\mid \{\textnormal{\raisebox{2pt}{\footnotesize $s'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z$}}\})
\end{array}$$ as witnessed by the test $${\ensuremath{\mathsf{3rd}(x)}} ={\ensuremath{\mathsf{mac}(z,\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{{\ensuremath{\mathsf{1st}(x)}},{\ensuremath{\mathsf{2nd}(x)}}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$})}}.$$*
c@width 1pt\> X@width 1ptc &&
&
&
&
&
&
&
&
&&
The purpose of the value $n$ is to allow the officer to count the signed vote only once. The synchronisation point, denoted $\text{synch}$, ensures that every voter receives the officer’s signature before any of them submit the unblinded value for counting. It is necessary to ensure vote privacy; without it, traffic analysis might link the voter’s signature in the first message with the anonymous submission in the third one. This protocol is inadequate for a real election, but it does satisfy the property of vote privacy.
We formalise this illustrative voting protocol in the applied pi calculus as follows. We assume a public channel $c$ for communication between the voter and the officer, and a channel $vote$ for the officer to declare the list of counted votes. $$\begin{array}{llcl}
& P &\triangleq& \nu\,sk_{1}\,\dots\, \nu\,sk_{n}.\; \nu\,sk_O.\\
&&& \textnormal{let } pk_1={\ensuremath{\mathsf{pk}(sk_{1})}} \textnormal{ in } \dots\ \textnormal{let } pk_n={\ensuremath{\mathsf{pk}(sk_{n})}} \textnormal{ in }\\
&&& \textnormal{let } pk_O={\ensuremath{\mathsf{pk}(sk_O)}} \textnormal{ in } \\
&&& (\overline{c}\langle pk_{1}\rangle \mid\dots\mid\overline{c}\langle pk_{n}\rangle \mid \overline{c}\langle pk_O\rangle \mid P_{V}\{\textnormal{\raisebox{2pt}{\footnotesize $sk_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\} \mid\dots \mid P_V\{\textnormal{\raisebox{2pt}{\footnotesize $sk_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\} \mid {!P_O} \mid S)\\
\\
& P_V &\triangleq& \nu n. \nu r.\textnormal{let } bvn={\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}} \textnormal{ in }\\
&&& \overline{c}\langle{\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_V)}},{\ensuremath{\mathsf{sign}(sk_V,bvn)}})}}\rangle.\\
&&& c(x). \textnormal{if } {\ensuremath{\mathsf{checksign}(pk_O,x)}}={\ensuremath{\mathsf{true}}} \textnormal{ then }\\
&&& \textnormal{if } {\ensuremath{\mathsf{getmsg}(x)}}=bvn \textnormal{ then }\\
&&& \textit{synch.}\\
&&& \overline{c}\langle{\ensuremath{\mathsf{unblind}(r,x)}}\rangle\\
\\
& P_O &\triangleq& c(y).\textnormal{if } {\ensuremath{\mathsf{checksign}({\ensuremath{\mathsf{fst}(y)}},{\ensuremath{\mathsf{snd}(y)}})}}={\ensuremath{\mathsf{true}}} \textnormal{ then }\\
&&& \textnormal{if } \mathsf{Eligible}({\ensuremath{\mathsf{fst}(y)}})={\ensuremath{\mathsf{true}}} \textnormal{ then }\\
&&& \overline{c}\langle{\ensuremath{\mathsf{sign}(sk_O,{\ensuremath{\mathsf{getmsg}({\ensuremath{\mathsf{snd}(y)}})}})}}\rangle. \\
&&& c(w). \\
&&& \textnormal{if } {\ensuremath{\mathsf{checksign}(pk_O,w)}}={\ensuremath{\mathsf{true}}} \textnormal{ then }\\
&&& \textnormal{if } \mathsf{NotSeen}(w)={\ensuremath{\mathsf{true}}} \textnormal{ then }\\
&&& \overline{vote}\langle{\ensuremath{\mathsf{fst}({\ensuremath{\mathsf{getmsg}(w)}})}}\rangle
\end{array}$$ In the above process, we assume functions $\mathsf{Eligible}(x)$ and $\mathsf{NotSeen}(x)$ are available to the officer. $\mathsf{Eligible}(x)$ checks whether the voter with public key $x$ is eligible and hasn’t already voted; $\mathsf{NotSeen}(x)$ stores $x$ and returns true if it has not seen $x$ before; otherwise it returns false. The purpose of $\mathsf{NotSeen}(x)$ is to ensure that the voter can’t use the signed token twice. We also assume a subprocess $\textit{synch}$ which a voter uses to synchronise with other voters. This can be modelled by defining a process $S$ to coordinate the synchronisation. In the case of $n$ voters, the coordination process receives precisely $n$ tokens, and then sends them back. To synchronise with the other voters, a voter sends a token to this synchronisation coordinator and awaits its response. Thus, $$\begin{array}{rcl}
\text{synch}&\triangleq& \overline{syn}\langle*\rangle.syn'(o)\\
S &\triangleq& syn(x_1)\dots syn(x_n).\overline{syn'}\langle*\rangle\dots\overline{syn'}\langle*\rangle\\
\end{array}$$ where $syn,syn'$ are private channels shared between the voters and $S$, $*$ is any name and $o$ is a variable.
Now we define the property of vote privacy, and prove it. Since it should hold even if the officer is corrupt, we can suppose that the officer is part of the attacker, and we need not consider its formalisation as $P_O$ above. This means the secrecy of the officer’s key is not required for the vote privacy property, so we can treat it as a free name. Moreover, the voters’ secret keys are also not required to be kept secret in order to ensure the vote privacy property. They too can be treated as free names. (Of course, these keys *are* required to be secret for other properties.)
Consider two voters $\mathcal{A}$, $\mathcal{B}$ and two candidates $v_a$, $v_b$. Based upon (**DKR09?**), we formalise vote privacy for two voters with the assertion that the attacker (including the election officers) cannot distinguish between a situation in which $\mathcal{A}$ votes $v_a$ and $\mathcal{B}$ votes $v_b$, from another one in which $\mathcal{A}$ votes $v_b$ and $\mathcal{B}$ votes $v_a$. We will write this as the equivalence: $$\begin{gathered}
%\new{sk_{V1}}.\new{sk_{V2}}.\new{sk_O}.\Letin{pk_O}{\Pk{sk_O}}
\nu\,syn.\nu\,syn'.(
P_V\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\}
\mid P_V\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\}
\mid S)\\
\approx_l
\nu\,syn.\nu\,syn'.(
P_V\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\}
\mid P_V\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\}
\mid S)
\end{gathered}$$ To prove this equivalence, let us call the left hand side $\mbox{{\sc Lhs}}$, and the right hand side $\mbox{{\sc Rhs}}$. We need to show a relation $\mathrel{\mathcal{R}}$ satisfying the requirements of Definition 3 such that $\mbox{{\sc Lhs}}\mathrel{\mathcal{R}}\mbox{{\sc Rhs}}$. As we have seen, the idea of $\mathrel{\mathcal{R}}$ is to relate successors of $\mbox{{\sc Lhs}}$ and $\mbox{{\sc Rhs}}$ that are expected to correspond to each other in the bisimulation. As $\mbox{{\sc Lhs}}$ evolves, the corresponding evolution of $\mbox{{\sc Rhs}}$ is the one that mimics $\mathcal{A}$ moves in $\mbox{{\sc Lhs}}$ with $\mathcal{A}$ moves in $\mbox{{\sc Rhs}}$, and $\mathcal{B}$ moves in $\mbox{{\sc Lhs}}$ with $\mathcal{B}$ moves in $\mbox{{\sc Rhs}}$, up to the synchronisation. After the synchronisation, $\mathcal{A}$ moves in $\mbox{{\sc Lhs}}$ are mimicked by $\mathcal{B}$ moves in $\mbox{{\sc Rhs}}$, and $\mathcal{B}$ moves in $\mbox{{\sc Lhs}}$ are mimicked by $\mathcal{A}$ moves in $\mbox{{\sc Rhs}}$. The reason for the ‘swap’ in mimicking is to ensure that the static equivalences will hold; before the synchronisation, the output data produced by $\mathcal{A}$ on both the $\mbox{{\sc Lhs}}$ and $\mbox{{\sc Rhs}}$ are indistinguishable (and similarly for $\mathcal{B}$). Observe that the output data reveals the keys ${\ensuremath{\mathsf{pk}(sk_A)}}$, ${\ensuremath{\mathsf{pk}(sk_B)}}$ (matched by ${\ensuremath{\mathsf{pk}(sk_A)}}$, ${\ensuremath{\mathsf{pk}(sk_B)}}$) and the signed blind votes ${\ensuremath{\mathsf{sign}(sk_{A},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v_a,n)}})}})}}$, ${\ensuremath{\mathsf{sign}(sk_{B},{\ensuremath{\mathsf{blind}(r',{\ensuremath{\mathsf{pair}(v_b,n')}})}})}}$ (matched by ${\ensuremath{\mathsf{sign}(sk_{A},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v_b,n)}})}})}}$, ${\ensuremath{\mathsf{sign}(sk_{B},{\ensuremath{\mathsf{blind}(r',{\ensuremath{\mathsf{pair}(v_a,n')}})}})}}$) where names $n,n',r,r'$ are under restriction in both $\mbox{{\sc Lhs}}$ and $\mbox{{\sc Rhs}}$. Indistinguishability between the $\mbox{{\sc Lhs}}$ and $\mbox{{\sc Rhs}}$ with respect to the signed blind votes is due to the properties of blinding. After the synchronisation $\mathcal{A}$ will reveal $v_a$ on the $\mbox{{\sc Lhs}}$ and $v_b$ on the $\mbox{{\sc Rhs}}$ (similarly $\mathcal{B}$ will reveal $v_b$ on the $\mbox{{\sc Lhs}}$ and $v_a$ on the $\mbox{{\sc Rhs}}$). Hence after synchronisation the actions mimicked are swapped.
To define this formally, we first define some partial evolutions of $P_V$, as follows. $$\begin{array}{llcl}
& P_1 &\triangleq&
\nu n. \nu r.\\
&&& \overline{c}\langle{\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_V)}},{\ensuremath{\mathsf{sign}(sk_{V},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}})}})}}\rangle.\\
&&& c(x). \textnormal{if } {\ensuremath{\mathsf{checksign}(pk_O,x)}}={\ensuremath{\mathsf{true}}} \textnormal{ then }\\
&&& \textnormal{if } {\ensuremath{\mathsf{getmsg}(x)}}={\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}} \textnormal{ then }\\
&&& \overline{syn}\langle*\rangle.syn'(o).\\
&&& \overline{c}\langle{\ensuremath{\mathsf{unblind}(r,x)}}\rangle
\end{array}$$ $$\begin{array}{llcl}
& P_2 &\triangleq&
\nu n. \nu r.\big( \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_V)}},{\ensuremath{\mathsf{sign}(sk_{V},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid\\
&&& c(x). \textnormal{if } {\ensuremath{\mathsf{checksign}(pk_O,x)}}={\ensuremath{\mathsf{true}}} \textnormal{ then }\\
&&& \textnormal{if } {\ensuremath{\mathsf{getmsg}(x)}}={\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}} \textnormal{ then }\\
&&& \overline{syn}\langle*\rangle.syn'(o).\\
&&& \overline{c}\langle{\ensuremath{\mathsf{unblind}(r,x)}}\rangle \big)
\end{array}$$ $$\begin{array}{llcl}
& P_3 &\triangleq&
\nu n. \nu r.\big( \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_V)}},{\ensuremath{\mathsf{sign}(sk_{V},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid\\
&&& \textnormal{if } {\ensuremath{\mathsf{checksign}(pk_O,m)}}={\ensuremath{\mathsf{true}}} \textnormal{ then }\\
&&& \textnormal{if } {\ensuremath{\mathsf{getmsg}(m)}}={\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}} \textnormal{ then }\\
&&& \overline{syn}\langle*\rangle.syn'(o).\\
&&& \overline{c}\langle{\ensuremath{\mathsf{unblind}(r,m)}}\rangle\big)
\end{array}$$ $$\begin{array}{llcl}
& P_4 &\triangleq&
\nu n. \nu r.\big( \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_V)}},{\ensuremath{\mathsf{sign}(sk_{V},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid\\
&&& \textnormal{if } {\ensuremath{\mathsf{getmsg}(m)}}={\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}} \textnormal{ then }\\
&&& \overline{syn}\langle*\rangle.syn'(o).\\
&&& \overline{c}\langle{\ensuremath{\mathsf{unblind}(r,m)}}\rangle\big)
\end{array}$$ $$\begin{array}{llcl}
& P_5 &\triangleq&
\nu n. \nu r.\big( \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_V)}},{\ensuremath{\mathsf{sign}(sk_{V},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid\\
&&& \overline{syn}\langle*\rangle.syn'(o).\\
&&& \overline{c}\langle{\ensuremath{\mathsf{unblind}(r,{\ensuremath{\mathsf{sign}(sk_{O},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}})}})}}\rangle\big)
\end{array}$$ $$\begin{array}{llcl}
& P_6 &\triangleq&
\nu n. \nu r.\big( \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_V)}},{\ensuremath{\mathsf{sign}(sk_{V},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid\\
&&& syn'(o).\\
&&& \overline{c}\langle{\ensuremath{\mathsf{unblind}(r,{\ensuremath{\mathsf{sign}(sk_{O},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}})}})}}\rangle\big)
\end{array}$$ $$\begin{array}{llcl}
& P_7 &\triangleq&
\nu n. \nu r.\big( \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_V)}},{\ensuremath{\mathsf{sign}(sk_{V},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid\\
&&& \overline{c}\langle{\ensuremath{\mathsf{unblind}(r,{\ensuremath{\mathsf{sign}(sk_{O},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}})}})}}\rangle\big)
\end{array}$$ $$\begin{array}{llcl}
& P_8 &\triangleq&
\nu n. \nu r.\big( \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_V)}},{\ensuremath{\mathsf{sign}(sk_{V},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid\\
&&& \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{unblind}(r,{\ensuremath{\mathsf{sign}(sk_{O},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v,n)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}}\}\big)
\end{array}$$ These are abbreviations that will be useful in our definition of the simulation relation. We define the relation $\mathrel{\mathcal{R}}$ as follows. Given closed extended processes $X$ and $Y$, $X\mathrel{\mathcal{R}}Y$ and $Y\mathrel{\mathcal{R}}X$ both hold if
- there exist integers $i,j$, variables $w,z$ and terms $M,N$ with $1\leq i,j\leq 6$ and $$\begin{array}{l}
X\equiv P_i\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $w$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}, \textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $m$}}\}
\mid P_j\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}, \textnormal{\raisebox{2pt}{\footnotesize $N$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $m$}}\}\mid S_{i,j},\\
Y\equiv P_i\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $w$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}, \textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $m$}}\}
\mid P_j\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}, \textnormal{\raisebox{2pt}{\footnotesize $N$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $m$}}\}\mid S_{i,j};\\
\end{array}$$ and if $i=4$ then ${\ensuremath{\mathsf{checksign}(pk_O,M)}}={\ensuremath{\mathsf{true}}}$, and if $j=4$ then ${\ensuremath{\mathsf{checksign}(pk_O,N)}}={\ensuremath{\mathsf{true}}}$; or
- there exist integers $i,j$, and variables $s,t,w,z$ with $6\leq i,j\leq 8$ and $$\begin{array}{l}
X\equiv P_i\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $w$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}, \textnormal{\raisebox{2pt}{\footnotesize $s$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}}\}
\mid P_j\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}, \textnormal{\raisebox{2pt}{\footnotesize $t$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}}\}\mid S_{i,j},\\
Y\equiv P_j\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $w$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}, \textnormal{\raisebox{2pt}{\footnotesize $t$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}}\}
\mid P_i\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}, \textnormal{\raisebox{2pt}{\footnotesize $s$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}}\}\mid S_{i,j}.\\
\end{array}$$
Notice that the substitutions above are syntactic, and recall that in an active substitution, the variable in the domain is considered to occur free. Thus, $(A\mid\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\})\{\textnormal{\raisebox{2pt}{\footnotesize $x$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}=A\{\textnormal{\raisebox{2pt}{\footnotesize $x$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid\{\textnormal{\raisebox{2pt}{\footnotesize $M\{\textnormal{\raisebox{2pt}{\footnotesize $x$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$; that is, the domain variable changed from $y$ to $x$.
In the definition of $\mathrel{\mathcal{R}}$, $S_{i,j}$ is whatever part of $S$ is left to execute. More precisely, $$S_{i,j}\triangleq\left\{\begin{array}{ll}
syn(x)syn(x).\overline{syn}\langle*\rangle\overline{syn}\langle*\rangle
&\text{if $i,j<6$}\\
syn(x).\overline{syn}\langle*\rangle\overline{syn}\langle*\rangle
&\text{if $i=6,j<6$ or $i<6,j=6$}\\
\overline{syn}\langle*\rangle\overline{syn}\langle*\rangle
&\text{if $i,j=6$}\\
\overline{syn}\langle*\rangle
&\text{if $i=6,j=7$ or $i=7,j=6$}\\
0
&\text{if $i,j\ge7$}\\
\end{array}\right.$$ We present a proof sketch that $\mathrel{\mathcal{R}}$ satisfies the requirements of Definition 3.
Static equivalence.
Consider, for example: $$\begin{gathered}
P_1\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\}\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid S_{1,2}\\
\mathrel{\mathcal{R}}\; P_1\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}})\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid S_{1,2}
\end{gathered}$$ The frame of the process on the left is $\nu n. \nu r. \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_{B})}},{\ensuremath{\mathsf{sign}(sk_{B},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v_b,n)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z$}}\}$ while the one on the right is $\nu n. \nu r. \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_{B})}},{\ensuremath{\mathsf{sign}(sk_{B},{\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v_a,n)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z$}}\}$. These differ only by the subterm $v_b$ on the left ($v_a$ on the right). Static equivalence holds because of the blinding. Consider $$\begin{gathered}
P_7\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $w$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid P_8\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}},\textnormal{\raisebox{2pt}{\footnotesize $t$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}}\}\mid S_{7,8}\\
\mathrel{\mathcal{R}}\; P_7\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid P_8\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $w$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}},\textnormal{\raisebox{2pt}{\footnotesize $t$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $u$}}\}\mid S_{7,8}
\end{gathered}$$ The frame of the process on the left is structurally equivalent to $$\begin{array}{l}
\nu n_1.\nu r_1. \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_{A})}},{\ensuremath{\mathsf{sign}(sk_{A},{\ensuremath{\mathsf{blind}(r_1,{\ensuremath{\mathsf{pair}(v_a,n_1)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $w$}}\}\mid{}\\
\nu n_2.\nu r_2.\big(\{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_{B})}},{\ensuremath{\mathsf{sign}(sk_{B},{\ensuremath{\mathsf{blind}(r_2,{\ensuremath{\mathsf{pair}(v_b,n_2)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z$}}\}\mid{}\\\qquad\qquad
\{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{unblind}(r_2,{\ensuremath{\mathsf{sign}(sk_O,{\ensuremath{\mathsf{blind}(r_2,{\ensuremath{\mathsf{pair}(v_b,n_2)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $t$}}\}
\big)
\end{array}$$ while the frame on the right is structurally equivalent to $$\begin{array}{l}
\nu n_1.\nu r_1. \{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_{B})}},{\ensuremath{\mathsf{sign}(sk_{B},{\ensuremath{\mathsf{blind}(r_1,{\ensuremath{\mathsf{pair}(v_a,n_1)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z$}}\}\mid{}\\
\nu n_2.\nu r_2.\big(\{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{pair}({\ensuremath{\mathsf{pk}(sk_{A})}},{\ensuremath{\mathsf{sign}(sk_{A},{\ensuremath{\mathsf{blind}(r_2,{\ensuremath{\mathsf{pair}(v_b,n_2)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $w$}}\}\mid{}\\\qquad\qquad
\{\textnormal{\raisebox{2pt}{\footnotesize ${\ensuremath{\mathsf{unblind}(r_2,{\ensuremath{\mathsf{sign}(sk_O,{\ensuremath{\mathsf{blind}(r_2,{\ensuremath{\mathsf{pair}(v_b,n_2)}})}})}})}}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $t$}}\}
\big)
\end{array}$$ These frames are statically equivalent.
Unlabelled transitions.
Suppose, for example, $A\xrightarrow{}A'$ and $$\begin{array}{rcl}
A &\equiv & P_3\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $w$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}},\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $m$}}\}\mid P_4\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}},\textnormal{\raisebox{2pt}{\footnotesize $N$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $m$}}\}\mid S_{3,4}\\
A'&\equiv & P_3\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $w$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}},\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $m$}}\}\mid P_5\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid S_{3,5}
\end{array}$$ Then, by $\mathrel{\mathcal{R}}$, $$\begin{array}{rcl}
B &\equiv &P_3\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $w$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}},\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $m$}})\mid P_4\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}},\textnormal{\raisebox{2pt}{\footnotesize $N$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $m$}})\mid S_{3,4}\\
\end{array}$$ and ${\ensuremath{\mathsf{checksign}(pk_O,N)}}={\ensuremath{\mathsf{true}}}$. Since the transition $A\to A'$ was possible, we have ${\ensuremath{\mathsf{getmsg}(N)}}\linebreak={\ensuremath{\mathsf{blind}(r,{\ensuremath{\mathsf{pair}(v_b,n)}})}}$, where $r,n$ are the values used inside the occurrence of $P_4$. It follows that we have $N={\ensuremath{\mathsf{sign}(sk_O,{\ensuremath{\mathsf{getmsg}({\ensuremath{\mathsf{snd}(z)}})}})}}$. Therefore, the transition $B\to B'$ is possible, where $$\begin{array}{rcl}
B'&\triangleq& P_3\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $w$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}},\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $m$}}\}\mid P_5\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid S_{3,5},
\end{array}$$ and we have $A'\mathrel{\mathcal{R}}B'$.
Labelled transitions.
Suppose, for example, $A\xrightarrow{\nu
w.\overline{c}\langle w\rangle} A'$ and $$\begin{array}{rcl}
A &\equiv & P_1\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\}\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid S_{1,2}\\
A'&\equiv & P_2\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}, \textnormal{\raisebox{2pt}{\footnotesize $w$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid S_{2,2}
\end{array}$$ Then, by $\mathrel{\mathcal{R}}$, $$\begin{array}{rcl}
B &\equiv &P_1\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\}\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid S_{1,2}
\end{array}$$ and so we set $$\begin{array}{rcl}
B'&\triangleq&P_2\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $w$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid S_{2,2}.
\end{array}$$ We have $A'\mathrel{\mathcal{R}}B'$.
Suppose, for example, $A\xrightarrow{c(T)}A'$ and $$\begin{array}{rcl}
A &\equiv & P_1\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\}\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid S_{1,2}\\
A'&\equiv & P_1\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\}\mid P_3\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}},\textnormal{\raisebox{2pt}{\footnotesize $T$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $m$}}\}\mid S_{1,3}
\end{array}$$ Then, by $\mathrel{\mathcal{R}}$, $$\begin{array}{rcl}
B &\equiv & P_1\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\}\mid P_2\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}}\}\mid S_{1,2}\\
\end{array}$$ and so we set $$\begin{array}{rcl}
B'&\triangleq& P_1\{\textnormal{\raisebox{2pt}{\footnotesize $sk_A$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_b$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}}\}\mid P_3\{\textnormal{\raisebox{2pt}{\footnotesize $sk_B$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $sk_V$}},\textnormal{\raisebox{2pt}{\footnotesize $v_a$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $v$}},\textnormal{\raisebox{2pt}{\footnotesize $z$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y$}},\textnormal{\raisebox{2pt}{\footnotesize $T$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $m$}}\}\mid S_{1,3}
\end{array}$$ We again have $A'\mathrel{\mathcal{R}}B'$.
This concludes our proof sketch of the labelled bisimilarity that expresses the privacy property for two voters. To complete this proof formally, once would have to consider all the cases involved in showing that $\mathrel R$ satisfies the requirements of Definition 3.
# Outlook
This chapter studies the applied pi calculus and demonstrates its applicability for analysing secrecy, correspondence and observational equivalence properties in the context of security protocols. In this section we briefly refer to some on-going research about the calculus. Our discussion is neither exhaustive nor complete.
The ability to reason with security properties is largely dependent on being able to reason with the equational theory. Abadi & Cortier (**Abadi04b?**) have studied decidability of secrecy and static equivalence for a large class of equational theories in the presence of a passive adversary. Subsequent work by Baudet, Cortier & Delaune (**Baudet09?**) and Ciobâcă, Delaune & Kremer (**Ciobaca09?**) introduces automated tools for analysing static equivalence with respect to convergent equational theories.
For an active adversary, reachability properties, in particular secrecy, have been studied in (**Blanchet2001?**; **Abadi2002?**) with updated and extended versions (**BlanchetJACM05?**; **Blanchet2010?**). Strong secrecy has been considered in (**Blanchet04?**). Correspondence properties have been presented in the context of authenticity (**Blanchet2002?**), and subsequently extended upon and revised in (**BlanchetJCS09?**). Proofs of observational equivalence have been studied with respect to processes that differ only by the choice of the terms that they contain, using the notion of uniformity (**Blanchet05?**; **Blanchet07b?**). But this notion of uniformity is often too strict; for example, the voting process discussed in this chapter does not satisfy it. A practical approach to overcoming the problem is introduced (**DRS08?**), (**BenSmythThesis?**) (the technique defined by (**BenSmythThesis?**) has been implemented as a tool called ProSwapper (**Smyth10:ObsA?**)) and subsequently used (**Backes08?**; **Delaune10:Vanets?**). As an alternative to uniformity as a proof technique, a symbolic version of the applied pi calculus is introduced in (**DKR09symbolic?**); by treating inputs symbolically, it avoids potentially infinite branching of processes due to inputs from the environment. Cortier & Delaune (**Cortier09?**) have shown that observational equivalence coincides with trace equivalence for determinate processes; and based on the symbolic semantics, this yields a decision procedure for observational equivalence of finite determinate processes without replication.
# Acknowledgements
We are very grateful to Myrto Arapinis and the editors of (**ChapterVersion?**) for careful reading of a draft of this work. In addition, we are grateful to Jiangshan Yu and Takahiro Kubota for highlighting mistakes in an earlier version of this document. This work has been partly supported by the EPSRC projects: *UbiVal: Fundamental Approaches to Validation of Ubiquitous Computing Applications and Infrastructures* (EP/D076625/2); and *Verifying Interoperability Requirements in Pervasive Systems* (EP/F033540/1). This work was partly done while Ben Smyth was at CNRS, Département d’Informatique, École Normale Supérieure, Paris, France with support from the *Direction Générale pour l’Armement*.
[^1]: This work is an extended version of Mark D. Ryan and Ben Smyth (2011) *Applied pi calculus*. In V Cortier and S Kremer, editor, Formal Models and Techniques for Analyzing Security Protocols.
[^2]: This work is an extended version of Mark D. Ryan and Ben Smyth (2011) *Applied pi calculus*. In V Cortier and S Kremer, editor, Formal Models and Techniques for Analyzing Security Protocols.