\mid&\neg\phi&\mbox{negation}\end{array}\qquad\qquad\begin{array}[]{rl}\mbox{abbreviations:}&\mathtt{tt}\triangleq
M=M\\\ &M\not=N\triangleq\neg(M=N)\\\
&\mathopen{\big{[}\pi\big{]}}\phi\triangleq\neg\mathopen{\big{\langle}\pi\big{\rangle}}\neg\phi\\\
&\phi\vee\psi\triangleq\neg\left(\neg\phi\wedge\neg\psi\right)\end{array}$

The semantics of classical $\mathcal{F}\\!\mathcal{M}$ is given by the least
relation $A\models\phi$ between extended processes $A$ and formulae $\phi$
satisfying the conditions in Fig. 7.

$\displaystyle\begin{array}[]{lcl}\mathopen{\nu\vec{x}.}\left(\theta\mathrel{\mid}P\right)\models
M=N&\mbox{iff}&M\theta\mathrel{=_{E}}N\theta~{}\mbox{ and }~{}\mbox{$\vec{x}$
are fresh for $M$ and $N$}\\\
A\models\mathopen{\big{\langle}\pi\big{\rangle}}\phi&\mbox{iff}&\mbox{there
exists }B~{}\mbox{ such that }~{}A\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{12.0pt}{0.6pt}}\limits^{\pi}$}\mkern-7.0mu\blacktriangleright}B~{}\mbox{
and }~{}B\models\phi.\\\
A\models\phi_{1}\land\phi_{2}&\mbox{iff}&A\models\phi_{1}~{}\mbox{ and
}~{}A\models\phi_{2}.\\\ A\models\neg\phi&\mbox{iff}&A\models\phi~{}\mbox{
does not hold.}\end{array}$
Figure 7. The semantics of modal logic “classical
$\mathcal{F}\\!\mathcal{M}$”.

The following theorem formulates what it means for classical
$\mathcal{F}\\!\mathcal{M}$ to characterise strong early bisimilarity.

######  Theorem 8.

$P\sim Q$, whenever, for all formula $\phi$, we have $P\models\phi$ if and
only if $Q\models\phi$.

The proof is provided in Appendix B. From the contrapositive of the above
theorem, whenever $P\not\sim Q$, there exists a formula $\phi$ such that
$P\models\phi$ holds, but $Q\not\models\phi$. Such a formula is called a
distinguishing formula.

####  3.3.2. The attack on BAC as a formula.

We are now in a position to prove Theorem 1, restated below for convenience,
which establishes that strong unlinkability of the BAC protocol fails.

######  Theorem 9 (Theorem 1 restated).

$\textit{System}\not\approx\textit{Spec}$.

######  Proof 3.1.

In order to establish the failure of strong unlinkability of the BAC protocol,
we make use of the following classical $\mathcal{F}\\!\mathcal{M}$ formula
$\psi$.

$\psi\triangleq\begin{array}[t]{l}\mathopen{\big{\langle}\overline{c}(u_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{c}(u_{2})\big{\rangle}}\mathopen{\big{\langle}d\,\textit{get\\_challenge}\big{\rangle}}\mathopen{\big{\langle}\overline{c}(\varv)\big{\rangle}}\big{(}\\\
\qquad\begin{array}[t]{l}\varv\not=\textit{get\\_challenge}\wedge{}\\\
\mathopen{\big{[}d\,\varv\big{]}}\big{(}\begin{array}[t]{l}\mathopen{\big{\langle}\overline{c}(\varw)\big{\rangle}}\mathopen{\big{\langle}d\,\varw\big{\rangle}}\mathopen{\big{\langle}\overline{c}(z)\big{\rangle}}\big{(}\varw\neq\textit{get\\_challenge}\wedge
z\neq\textit{get\\_challenge}\wedge z\neq\textit{error}\big{)}\\\ \vee\
\mathopen{\big{[}\overline{c}(\varw)\big{]}}\left(\varw=\textit{get\\_challenge}\right)\big{)}\big{)}\end{array}\end{array}\end{array}$

For this formula we can verify ${\textbf{{System}}}\models\psi$ holds; while
${\textbf{{Spec}}}\not\models\psi$. Hence, by Theorem 8,
${\textbf{{System}}}\not\sim{\textbf{{Spec}}}$; thereby by Theorem 5,
$\textit{System}\not\approx\textit{Spec}$, as required.

This closes the initial question of whether or not unlinkability holds for the
BAC protocol; the answer is that the BAC protocol does not satisfy
unlinkability, at least as specified originally in CSF’10 [ACRR10]. This leads
to several immediate questions. Firstly, how do we construct the above formula
from the distinguishing strategy given by open bisimilarity (to be addressed
in Sec. 3.3.3)? Secondly, can we explain why the formula is distinguishing,
and from that explanation describe a practical attack? Thirdly, how do we
approach the problem of constructing a formula in general and how do we handle
cases when a spurious counterexample is discovered? We focus mainly on the
first question in this paper. The second question we we return to in the next
section; while the third question is worthy of future work, since it would
enable tool support.

We emphasise at this point that there are infinitely many alternative
distinguishing formulae for this problem, not only $\psi$. Some such
distinguishing formulae use no box modality and instead employ conjunction,
where conjunction also appeals to the branching time nature of bisimilarity.
We postpone discussing alternatives until Sec. 4, where we propose an
alternative model of unlinkability, where the meaning of distinguishing
strategies is clearer.

####  3.3.3. How to construct the distinguishing formula

We construct the formula named $\phi$, used as the distinguishing formula in
the proof of Theorem 1 (reiterated as Theorem 9), by induction on the depth of
the distinguishing strategy summarised at the top of Sec. 3.3. To do so, we
work backwards through the distinguishing strategy. Note we refer to processes
representing intermediate states of an execution previously defined throughout
Sec. 3.

Firstly, observe that when the system is in state
${\textbf{{System}}}^{\mathrm{V}}$ the specification must be in a state where
either $\textit{error}=z$, $\textit{get\\_challenge}=z$ or
$\textit{get\\_challenge}=\varw$, where each pair of messages shows static
equivalence is violated. Since for ${\textbf{{System}}}^{\mathrm{V}}$ both
$\varw$ and $z$ cannot be unified with get_challenge or error with respect to
the history at that point, the intuitionistic negation and classical negation
coincide for these equalities, leading to the following formula distinguishing
${\textbf{{System}}}^{\mathrm{V}}$ from any state the specification can reach
at that point.

${\textbf{{System}}}^{\mathrm{V}}\models\textit{error}\not=z\wedge\textit{get\\_challenge}\not=z\wedge\textit{get\\_challenge}\neq\varw$

Since the system leads in order to reach this state using transition
${\textbf{{System}}}^{\mathrm{IV}}\mathclose{\left\\{{}^{\varv,\varw}\\!/\\!_{nt,\vary}\right\\}}\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{17.34111pt}{0.6pt}}\limits^{\overline{c}(z)}$}\mkern-7.0mu\blacktriangleright}{\textbf{{System}}}^{\mathrm{V}}$,
we add a diamond modality to the formula, as follows.

${\textbf{{System}}}^{\mathrm{IV}}\mathclose{\left\\{{}^{\varv,\varw}\\!/\\!_{nt,\vary}\right\\}}\models\mathopen{\big{\langle}\overline{c}(z)\big{\rangle}}\left(\textit{error}\not=z\wedge\textit{get\\_challenge}\not=z\wedge\textit{get\\_challenge}\neq\varw\right)$

The above step is standard for constructing modal logic formulae for
distinguishing strategies; however the next step requires care. Firstly, note
that the substitution
$\mathclose{\left\\{{}^{\varv,\varw}\\!/\\!_{nt,\vary}\right\\}}$ concerns
input variables. Thus we push these substitutions back through the
distinguishing strategy until the relevant input is instantiated. At this
point, since the input action in the distinguishing strategy reaching state
${\textbf{{System}}}^{\mathrm{IV}}\mathclose{\left\\{{}^{\varv,\varw}\\!/\\!_{nt,\vary}\right\\}}$
introduced variable $y$, that variable is instantiated immediately, and $nt$
is pushed back through the strategy, refining the distinguishing strategy to
obtain the following transitions using the rules of Fig. 3.

${\textbf{{System}}}^{\mathrm{III}}\mathclose{\left\\{{}^{\varv}\\!/\\!_{nt}\right\\}}\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{20.12651pt}{0.6pt}}\limits^{\overline{c}(\varw)}$}\mkern-7.0mu\blacktriangleright}\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{14.99207pt}{0.6pt}}\limits^{d\,\varw}$}\mkern-7.0mu\blacktriangleright}{\textbf{{System}}}^{\mathrm{IV}}\mathclose{\left\\{{}^{\varv,\varw}\\!/\\!_{nt,\vary}\right\\}}$

Since the system was leading,
${\textbf{{System}}}^{\mathrm{III}}\mathclose{\left\\{{}^{\varv}\\!/\\!_{nt}\right\\}}$
can be distinguished from
${\textbf{{Spec}}}^{\mathrm{III}}\mathclose{\left\\{{}^{\varv}\\!/\\!_{nt}\right\\}}$
by the following formula.

${\textbf{{System}}}^{\mathrm{III}}\mathclose{\left\\{{}^{\varv}\\!/\\!_{nt}\right\\}}\models\mathopen{\big{\langle}\overline{c}(\varw)\big{\rangle}}\mathopen{\big{\langle}d\,\varw\big{\rangle}}\mathopen{\big{\langle}\overline{c}(z)\big{\rangle}}\left(\textit{error}\not=z\wedge\textit{get\\_challenge}\not=z\wedge\textit{get\\_challenge}\neq\varw\right)$

The next step in the distinguishing strategy involves a change of leading
player, where the specification leads with an action. By pushing back the
substitution through the strategy, instantiating the input variable on the
label, we have the following transition led by the specification:
${\textbf{{Spec}}}^{\mathrm{II}}\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{14.99207pt}{0.6pt}}\limits^{d\,\varv}$}\mkern-7.0mu\blacktriangleright}{\textbf{{Spec}}}^{\mathrm{III}}\mathclose{\left\\{{}^{\varv}\\!/\\!_{nt}\right\\}}$.
Since the specification leads at this point and the system follows in any way
it can, we write the box modality in the distinguishing formula for the system
followed by a disjunction of formulae, where each formula distinguishes
${\textbf{{Spec}}}^{\mathrm{III}}\mathclose{\left\\{{}^{\varv}\\!/\\!_{nt}\right\\}}$
from any state reachable from ${\textbf{{System}}}^{\mathrm{II}}$ by an input
transition labelled with $d\,\varv$.

$\textstyle{(\dagger)~{}{\textbf{{System}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{c}(u_{1})}$Spec$\scriptstyle{\overline{c}(u_{1})}$$\scriptstyle{\overline{c}(u_{2})}$$\scriptstyle{\overline{c}(u_{2})}$$\scriptstyle{d\,\textit{get\\_challenge}}$$\scriptstyle{d\,\textit{get\\_challenge}}$$\textstyle{{\textbf{{System}}}^{\mathrm{I}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{c}(\varv)}$$\textstyle{{\textbf{{Spec}}}^{\mathrm{I}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{c}(\varv)}$$\scriptstyle{\overline{c}(\varv)}$$\textstyle{{\textbf{{System}}}^{\mathrm{II}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{d\,\varv}$$\scriptstyle{d\,\varv}$$\textstyle{(\dagger)~{}{\textbf{{Spec}}}^{\mathrm{II}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{d\,\varv}$$\textstyle{\varv=\textit{get\\_challenge}}$$\textstyle{(\dagger)~{}{\textbf{{System}}}^{\mathrm{III}}\mathclose{\left\\{{}^{\varv}\\!/\\!_{nt}\right\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{c}(\varw)}$$\scriptstyle{\overline{c}(\varw)}$$\textstyle{{\textbf{{Spec}}}^{\mathrm{III}}\mathclose{\left\\{{}^{\varv}\\!/\\!_{nt}\right\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{c}(\varw)}$$\scriptstyle{\overline{c}(\varw)}$$\scriptstyle{d\,\varw}$$\textstyle{\varw=\textit{get\\_challenge}}$$\scriptstyle{d\,\varw}$$\textstyle{\varw=\textit{get\\_challenge}}$$\textstyle{{\textbf{{System}}}^{\mathrm{IV}}\mathclose{\left\\{{}^{\varv,\varw}\\!/\\!_{nt,\vary}\right\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{c}(z)}$$\textstyle{{\textbf{{Spec}}}^{\mathrm{IV}}\mathclose{\left\\{{}^{\varv,\varw}\\!/\\!_{nt,\vary}\right\\}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{c}(z)}$$\scriptstyle{\overline{c}(z)}$$\textstyle{z\not=\textit{error}\wedge
z\not=\textit{get\\_challenge}}$$\textstyle{z=\textit{error}}$$\textstyle{z=\textit{get\\_challenge}}$
Figure 8. Distinguishing strategy implied by distinguishing formula $\psi$.

Observe that, as well as
${\textbf{{System}}}^{\mathrm{III}}\mathclose{\left\\{{}^{\varv}\\!/\\!_{nt}\right\\}}$
for which we constructed a distinguishing formula above, there is another,
quite distinct, process reachable from ${\textbf{{System}}}^{\mathrm{II}}$ by
a $d\,\varv$ transition that can be distinguished by formula
$\mathopen{\big{[}\overline{c}(\varw)\big{]}}(\varw=\textit{get\\_challenge})$
representing that the case when input transition labelled with $d\,\varv$
results in feeding $\varv$ into a new reader session, which kills the
possibility of continuing an existing session with an output transition. Note
this formula is also constructed algorithmically, as we are describing, but
this branch is more due to a limitation of the original model unlinkability
communicated in CSF’10, that we address next in Sec. 4. Hence we draw no
further attention to that branch at this point.

Thereby, we obtain the following formula distinguishing
${\textbf{{System}}}^{\mathrm{II}}$ from ${\textbf{{Spec}}}^{\mathrm{II}}$.

${\textbf{{System}}}^{\mathrm{II}}\models\mathopen{\big{[}d\,\varv\big{]}}\big{(}\begin{array}[t]{l}\mathopen{\big{\langle}\overline{c}(\varw)\big{\rangle}}\mathopen{\big{\langle}d\,\varw\big{\rangle}}\mathopen{\big{\langle}\overline{c}(z)\big{\rangle}}\big{(}\varw\neq\textit{get\\_challenge}\wedge
z\neq\textit{get\\_challenge}\wedge z\neq\textit{error}\big{)}\\\ \vee\
\mathopen{\big{[}\overline{c}(\varw)\big{]}}\left(\varw=\textit{get\\_challenge}\right)\big{)}\end{array}$

The rest of the construction of formula $\psi$ follows the pattern of steps
already described above, where a diamond modality is appended whenever the
system leads and substitutions are pushed back through the distinguishing
strategy until they instantiate the relevant input, or reach the root of the
formula.

We present an informal graphical depiction of the game that $\psi$ describes
in Fig. 8. In the figure, annotation $(\dagger)$ indicates where a process
takes over as the leading process in the strategy. When a process is not
leading it may have the option to try more than one counter move, represented
by the branches in the strategy.

##  4\. A New Chapter for Unlinkability: Refining the Model of Unlinkability

While the previous sections closed a chapter in the story of unlinkability, by
proving that there is an attack on the model of unlinkability of the BAC
protocol as originally communicated in the proceedings of CSF’10 [ACRR10],
this section opens a new chapter by justifying a new model of unlinkability.
This new model of unlinkability is a modest improvement on the model
previously proposed. It incorporates some explicit observables reflecting the
ability of the attacker to observe and hence control the creation of radio
frequency communication channels. We demonstrate here why our proposed model
of unlinkability more accurately models the distinguishing power of an
attacker; and how descriptions of attacks on the BAC protocol, given by modal
logic formulae, become clearer. This section can also been seen as introducing
preliminaries required for Section 5, where we show how the model proposed
discovers new attacks on the PACE protocol that follow a similar pattern to
the attacks discovered on the BAC protocol.

The model of strong unlinkability originally proposed in CSF’10 [ACRR10] has
many merits. However, a limitation we would like to draw attention to is that
it matters whether or not we include the get_challenge message that the reader
sends to initiate the protocol. That get_challenge message happens to be
essential for the attacks on unlinkability described in the previous section
since, by controlling the get_challenge messages sent and received, we can
count the number of sessions that are present and thereby infer when a message
sent is a ciphertext in an existing session of the protocol rather than a
fresh nonce at the beginning of a new protocol.

This is perhaps clearest in Fig. 8 of the previous section. Observe that in
order to reach the bottommost state in the figure, we ensure that no
additional sessions are started beyond the two reader sessions and one
ePassport session at the beginning triggered by the topmost three actions in
the figure. This causes problems, three of which are highlighted below, which
are all due to the modelling decision where all parties use the same channel
$c$ for outputs and $d$ for inputs.

  * •

Limitation 1. It is inconvenient and confusing to, throughout the strategy,
add branches that have the effect of saying “at this point we don’t start a
new session.”

  * •

Limitation 2. In the reality, the attacker can directly observe whether or not
two inputs or outputs are performed within the same session of a protocol and,
furthermore, can distinguish between a session with a reader or with an
ePassport. This is not only because the attacker must be aware of the physical
location of each entity, but also because, for each session, the attacker must
open a new channel using the underlying transport protocol, as standardised in
ISO/IEC 14443 [ISO18].

  * •

Limitation 3. Finally, the fact that the get_challenge message is useful for
counting the number of each type of session initiated, is rather a misuse of
that message. Message get_challenge contributes nothing to this authentication
protocol (other than impeding the stronger authentication property
synchronisation [CMdV06], which is immediately violated in protocols with a
constant message). Hence removing it from a model of BAC should not result in
attacks ceasing to exist.

The above limitations of existing models used to analyse the unlinkability of
the BAC protocol, as employed in previous sections, can be addressed simply by
declaring a fresh public channel for each session. To do so, we extend the
model with two channels, say passport and reader, that are used to model the
creation of a new channel in the respective roles of either an ePassport or a
reader. In the applied $\pi$-calculus, we achieve this by sending a fresh
channel to the environment on these channels for each session, as in the
following new scheme for the system and specification.

$\begin{array}[]{ll}\mbox{Scheme for
System:}&\mathopen{!}\mathopen{\nu\vec{k}.}\mathopen{!}\left(\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{passport}}}\left<c\right>}.\textit{Prover}(c,\vec{k})\mathrel{\mid}\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{reader}}}\left<c\right>}.\textit{Verifier}(c,\vec{k})\right)\\\
\mbox{Scheme for
Specification:}&\mathopen{!}\mathopen{\nu\vec{k}.}\left(\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{passport}}}\left<c\right>}.\textit{Prover}(c,\vec{k})\mathrel{\mid}\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{reader}}}\left<c\right>}.\textit{Verifier}(c,\vec{k})\right)\end{array}$

The above we propose as a general scheme for RFID protocols employing
symmetric keys $\vec{k}$, which are shared through another channel that the
attacker cannot intercept. Recall, in the case of ePassport protocols, this is
usually achieved by an OCR session; but may be achieved by other means such as
sending the key to the reader via a secure connection between a personal
device and the reader. Thus a fundamental assumption in all these models of
unlinkability is that we are considering use cases where intercepting and
manipulating RFID communication is easier than intercepting the keys, which
would trivially break unlinkability.

Notice we directly employ a presentation of processes that does not involve
$\tau$-transitions. This simplifies the problem such that strong notions of
bisimilarity may be employed, without loss of modelling power. Of course, to
do so, we should assume each instance of Prover and Verifier is a sequential
process (or apply another suitable restriction for forbidding
$\tau$-transitions internal to a single reader or ePassport).

###  4.1. The unlinkability of the BAC protocol, simplified

Following the above scheme for the BAC protocol, $\vec{k}$ is $ke,km$, and
$\textit{Prover}(c,ke,km)$ and $\textit{Verifier}(c,ke,km)$ are instantiated
with the processes $P_{\textit{BAC}}(c,ke,km)$ and $V_{\textit{BAC}}(c,ke,km)$
defined below.

$\begin{array}[]{rl}P_{\textit{BAC}}(c,ke,km)\triangleq&\begin{array}[t]{l}\nu
nt.\mathopen{\mathopen{\overline{c}}\left<nt\right>}.c(y).\\\
\texttt{if}\,\mathopen{\texttt{snd}}\left(y\right)=\mathopen{\texttt{missing}}{mac}\left(\mathopen{\texttt{fst}}\left(y\right),km\right)\,\texttt{then}\\\
\qquad\begin{array}[t]{l}\texttt{if}\,nt=\mathopen{\texttt{fst}}\left(\mathopen{\texttt{snd}}\left(\mathopen{\texttt{missing}}{dec}\left(\mathopen{\texttt{fst}}\left(y\right),ke\right)\right)\right)\,\texttt{then}\\\
\qquad\begin{array}[t]{l}\nu
kt.\texttt{let}\,m=\left\\{\left<{nt},\,{\left<{\mathopen{\texttt{fst}}\left(\mathopen{\texttt{missing}}{dec}\left(\mathopen{\texttt{fst}}\left(y\right),ke\right)\right)},\,{kt}\right>}\right>\right\\}_{ke}\,\texttt{in}\\\
\mathopen{\mathopen{\overline{c}}\left<m,\mathopen{\texttt{missing}}{mac}\left(m,km\right)\right>}\end{array}\\\
\texttt{else}\,\mathopen{\mathopen{\overline{c}}\left<error\right>}\end{array}\\\
\texttt{else}\,\mathopen{\mathopen{\overline{c}}\left<error\right>}\end{array}\\\
V_{\textit{BAC}}(c,ke,km)\triangleq&\begin{array}[t]{l}c(nt).\nu nr.\nu kr.\\\
\texttt{let}\,m=\left\\{\left<{nr},\,{\left<{nt},\,{kr}\right>}\right>\right\\}_{ke}\,\texttt{in}\,\mathopen{\mathopen{\overline{c}}\left<m,\mathopen{\texttt{missing}}{mac}\left(\left<{m},\,{km}\right>\right)\right>}\end{array}\end{array}$

Notice the above processes are simply
$\textit{P}(ke,km)\mathclose{\left\\{{}^{c}\\!/\\!_{d}\right\\}}$ and
$\textit{V}(ke,km)\mathclose{\left\\{{}^{c}\\!/\\!_{d}\right\\}}$ from the
previous sections, but with prefixes concerning the get_challenge message
removed.

In summary, we propose that the problem of whether there is an attack on the
unlinkability of the BAC protocol can be resolved by proving that the
following theorem holds.

######  Theorem 10.

$\textit{System}_{\textit{BAC}}\not\sim\textit{Spec}_{\textit{BAC}}$, where

$\begin{array}[]{rl}\textit{System}_{\textit{BAC}}\triangleq&\mathopen{!}\mathopen{\nu
ke,km.}\mathopen{!}\left(\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{passport}}}\left<c\right>}.P_{\textit{BAC}}(c,ke,km)\mathrel{\mid}\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{reader}}}\left<c\right>}.V_{\textit{BAC}}(c,ke,km)\right)\\\
\textit{Spec}_{\textit{BAC}}\triangleq&\mathopen{!}\mathopen{\nu
ke,km.}\left(\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{passport}}}\left<c\right>}.P_{\textit{BAC}}(c,ke,km)\mathrel{\mid}\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{reader}}}\left<c\right>}.V_{\textit{BAC}}(c,ke,km)\right)\end{array}$

######  Proof 4.1.

Consider the $\mathcal{F}\\!\mathcal{M}$ formula below.

$\varphi\triangleq\begin{array}[t]{l}\mathopen{\big{\langle}\overline{\textit{reader}}(c_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{\textit{reader}}(c_{2})\big{\rangle}}\mathopen{\big{\langle}\overline{\textit{passport}}(c_{3})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(nt)\big{\rangle}}\Big{(}\\\
\qquad\begin{array}[t]{rl}&\mathopen{\big{\langle}c_{1}\,nt\big{\rangle}}\mathopen{\big{\langle}\overline{c_{1}}(\varw)\big{\rangle}}\mathopen{\big{\langle}c_{3}\,\varw\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(z)\big{\rangle}}\left(z\neq\textit{error}\right)\\\
\wedge&\mathopen{\big{\langle}c_{2}\,nt\big{\rangle}}\mathopen{\big{\langle}\overline{c_{2}}(\varw)\big{\rangle}}\mathopen{\big{\langle}c_{3}\,\varw\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(z)\big{\rangle}}\left(z\neq\textit{error}\right)~{}\Big{)}\end{array}\end{array}$

Since $\textit{System}_{\textit{BAC}}\models\varphi$, but
$\textit{Spec}_{\textit{BAC}}\not\models\varphi$, by Theorem 8,
$\textit{System}_{\textit{BAC}}\not\sim\textit{Spec}_{\textit{BAC}}$.

---
$\textstyle{(\dagger)~{}\textit{System}_{\textit{BAC}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{\textit{reader}}(c_{1})}$$\textstyle{\textit{Spec}_{\textit{BAC}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{\textit{reader}}(c_{1})}$$\scriptstyle{\overline{\textit{reader}}(c_{2})}$$\scriptstyle{\overline{\textit{reader}}(c_{2})}$$\scriptstyle{\overline{\textit{passport}}(c_{3})}$$\scriptstyle{\overline{\textit{passport}}(c_{3})}$$\scriptstyle{\overline{\textit{passport}}(c_{3})}$$\scriptstyle{\overline{c_{3}}(nt)}$$\scriptstyle{\overline{c_{3}}(nt)}$$\scriptstyle{\overline{c_{3}}(nt)}$$\scriptstyle{c_{1}\,nt}$$\scriptstyle{c_{2}\,nt}$$\scriptstyle{c_{1}\,nt}$$\scriptstyle{c_{2}\,nt}$$\scriptstyle{\overline{c_{1}}(\varw)}$$\scriptstyle{\overline{c_{2}}(\varw)}$$\scriptstyle{\overline{c_{1}}(\varw)}$$\scriptstyle{\overline{c_{2}}(\varw)}$$\scriptstyle{c_{3}\,\varw}$$\scriptstyle{c_{3}\,\varw}$$\scriptstyle{c_{3}\,\varw}$$\scriptstyle{c_{3}\,\varw}$$\scriptstyle{\overline{c_{1}}(z)}$$\scriptstyle{\overline{c_{2}}(z)}$$\scriptstyle{\overline{c_{1}}(z)}$$\scriptstyle{\overline{c_{2}}(z)}$$\textstyle{z\not=\textit{error}}$$\textstyle{z\not=\textit{error}}$$\textstyle{z=\textit{error}}$$\textstyle{z=\textit{error}}$
Figure 9. Distinguishing strategy implied by distinguishing formula $\varphi$.

Now compare the distinguishing strategy generated by $\varphi$, presented in
Fig. 9, to the distinguishing strategy for $\psi$ in the previous section,
presented in Fig. 8. The attacks described start in a similar fashion. In both
figures, the system starts up two readers and an ePassport with the same keys.
The specification can only follow by starting two readers with different keys;
hence when the ePassport is initialised is has different keys from at least
one of the readers. We draw attention to two key differences between the
strategies presented below.

The first notable difference between the strategies is that Fig. 9 does not
require several sub-branches of the strategy involving get_challenge messages.
Those branches that appear throughout Fig. 8 are no longer required, since we
can directly observe the number of sessions that are present, rather than
implicitly controlling the number of sessions by preventing new sessions from
initialising. This difference is beneficial for cleaning up messy strategies,
making them easier to explain, and allowing more protocols to be analysed
without having to insert constant messages into the model of the protocol.

The second notable difference between the strategies is that, in Fig. 9, the
system always leads, including at the point where branching occurs. By the
time the system decides which branch to take, the specification has already
committed to a state where the the ePassport has different keys from either
the reader on channel $c_{1}$ or the reader on channel $c_{2}$. The strategy
of the system is to choose to communicate with the reader which has keys that
are different to those of the ePassport. Thereby the system wins the game
since it can reach a state where no error is produced by the chosen ePassport
— a strategy that cannot be matched by the specification. In contrast, the
strategy in Fig. 8 achieved a similar effect but in a different way: the
attacker changes perspective by switching to a view where the leading player
is the specification, i.e., what should hypothetically happen. Recall, in Fig.
8, after the change of player, the strategy is for the specification to choose
to communicate with a reader that should produce an error message; but the
system has no way to produce such an error message hence the system clearly is
not equivalent to the hypothetical situation modelled by the specification.

###  4.2. Alternative formulas for describing attacks

The formula in the proof of Theorem 10 is not the only formula describing an
attack on unlinkability of the BAC protocol. Indeed, in Section 3.3.2 we noted
that, when there is an attack, there are infinitely many alternative formulae.
In this section, we introduce and explain another formula that is a little
longer than $\varphi$, defined in the previous section, but is useful for
situating the attacks discovered.

Consider the $\mathcal{F}\\!\mathcal{M}$ formula below.

$\varsigma\triangleq\begin{array}[t]{l}\mathopen{\big{\langle}\overline{\textit{reader}}(c_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{\textit{passport}}(c_{3})\big{\rangle}}\Big{(}\\\
\quad\begin{array}[t]{rl}&\mathopen{\big{\langle}\overline{c_{3}}(nt)\big{\rangle}}\mathopen{\big{\langle}c_{1}\,nt\big{\rangle}}\mathopen{\big{\langle}\overline{c_{1}}(\varw)\big{\rangle}}\mathopen{\big{\langle}c_{3}\,\varw\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(z)\big{\rangle}}\left(z\neq\textit{error}\right)\\\
\wedge&\mathopen{\big{\langle}c_{1}\,nt^{\prime}\big{\rangle}}\mathopen{\big{\langle}\overline{c_{1}}(w^{\prime})\big{\rangle}}\mathopen{\big{\langle}\overline{\textit{reader}}(c_{2})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(nt)\big{\rangle}}\mathopen{\big{\langle}c_{2}\,nt\big{\rangle}}\mathopen{\big{\langle}\overline{c_{2}}(\varw)\big{\rangle}}\mathopen{\big{\langle}c_{3}\,\varw\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(z)\big{\rangle}}\left(z\neq\textit{error}\right)~{}\Big{)}\end{array}\end{array}$

The above formula also serves as an alternative proof certificate for Theorem
10. Observe that $\textit{System}_{\textit{BAC}}\models\varsigma$, but
$\textit{Spec}_{\textit{BAC}}\not\models\varsigma$; and hence, by Theorem 8,
$\textit{System}_{\textit{BAC}}\not\sim\textit{Spec}_{\textit{BAC}}$. The
distinguishing strategy described by $\varsigma$ is depicted in Fig. 10.

$\textstyle{(\dagger)~{}\textit{System}_{\textit{BAC}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{\textit{reader}}(c_{1})}$$\textstyle{\textit{Spec}_{\textit{BAC}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\overline{\textit{reader}}(c_{1})}$$\scriptstyle{\overline{\textit{passport}}(c_{3})}$$\scriptstyle{\overline{\textit{passport}}(c_{3})}$$\scriptstyle{\overline{\textit{passport}}(c_{3})}$$\scriptstyle{\overline{c_{3}}(nt)}$$\scriptstyle{{c_{1}}\,nt^{\prime}}$$\scriptstyle{\overline{c_{3}}(nt)}$$\scriptstyle{{c_{1}}\,nt^{\prime}}$$\scriptstyle{c_{1}\,nt}$$\scriptstyle{\overline{c_{1}}(w^{\prime})}$$\scriptstyle{c_{1}\,nt}$$\scriptstyle{\overline{c_{1}}(w^{\prime})}$$\scriptstyle{\overline{c_{1}}(\varw)}$$\scriptstyle{\overline{\textit{reader}}(c_{2})}$$\scriptstyle{\overline{c_{1}}(\varw)}$$\scriptstyle{\overline{\textit{reader}}(c_{2})}$$\scriptstyle{c_{3}\,\varw}$$\scriptstyle{\overline{c_{3}}(nt)}$$\scriptstyle{c_{3}\,\varw}$$\scriptstyle{\overline{c_{3}}(nt)}$$\scriptstyle{\overline{c_{1}}(z)}$$\scriptstyle{c_{2}\,nt}$$\scriptstyle{\overline{c_{1}}(z)}$$\scriptstyle{c_{2}\,nt}$$\textstyle{z\not=\textit{error}}$$\scriptstyle{\overline{c_{2}}(\varw)}$$\textstyle{z=\textit{error}}$$\scriptstyle{\overline{c_{2}}(\varw)}$$\scriptstyle{c_{3}\,\varw}$$\scriptstyle{c_{3}\,\varw}$$\scriptstyle{\overline{c_{2}}(z)}$$\scriptstyle{\overline{c_{2}}(z)}$$\textstyle{z\not=\textit{error}}$$\textstyle{z=\textit{error}}$
Figure 10. Another distinguishing strategy $\varsigma$, where readers are
created sequentially.

Both formulas $\varsigma$ and $\varphi$ describe attack strategies on the
unlinkability of the BAC protocol. The advantage of $\varphi$ is that it is
more compact. Also, declaring two readers at the top of the strategy and
making a choice between them makes clear the key idea: that there is a
strategy for testing whether two readers are capable of authenticating the
same ePassport.

Formula $\varsigma$ is presented to point out that the two readers need not be
simultaneously active. Observe that in $\varsigma$ the event representing the
creation of the second reader, indicated in both strategies as
$\mathopen{\mathopen{\overline{\textit{reader}}}\left<c_{2}\right>}$, is
pushed later in the attack strategy compared to in $\varphi$. The
distinguishing strategy then proceeds as follows.

  1. (1)

A run of a reader and ePassport is created. What is important at this point is
that the system has an opportunity to start a reader and ePassport run that
match, i.e., the reader is loaded with the key of the ePassport in question.
The specification has two choices, which are the first and second respective
branches taken by $\textit{Spec}_{\textit{BAC}}$ in Fig. 10:

    1. (a)

the specification can start a run with an ePassport with different keys to the
reader;

    2. (b)

or using the same keys as the reader.

  2. (2)

Now consider the two branches of the conjunction in the formula $\varsigma$,
which occurs after one reader and ePassport are created.

    1. (a)

In the first branch of the conjunction, the second reader is never used. There
are only the events required for the run of the ePassport and reader,
initially created on channels $c_{3}$ and $c_{1}$ respectively, to
authenticate. This branch of the conjunction can be played by the attacker
whenever the specification takes its first branch $(\ref{itema})$, where the
run of an ePassport involves keys different from those loaded into the reader
initially created.

    2. (b)

In the second branch of the conjunction, we do make use of a second reader. To
emphasise that no actions of readers need be concurrent for this attack
strategy, we first consume the actions of the reader on channel $c_{1}$ by
using the dummy nonce $nt^{\prime}$ and effectively ignoring the response
$w^{\prime}$ from that reader. At that point, the second reader is created on
channel $c_{2}$ such that it is again loaded with the same keys. This allows
the second reader to successfully authenticate the ePassport created at the
beginning of the attack. This branch of the conjunction is played in response
to the specification taking its second branch $(\ref{itemb})$, where the run
of the ePassport and first reader on $c_{1}$ match, and hence, since no
further run may use the same keys, the second reader must fail to authenticate
in that idealised setting.

The first thing to observe about the attack described by $\varsigma$ is that,
since no two reader runs are concurrently active, we know that designing a
system to force reader runs involving the same ePassport to be conducted
sequentially will not prevent attacks on unlinkability. We raise this point,
since, as explored in related work [Bae21] sequentialising reader sessions
does prevent certain kinds of attacks on the unlinkability of certain
protocols (such as a previously known attack on the PACE protocol that we will
come to in the next Section 5). In that work, an operator, with symbol  ! , is
used as a prefix for reader sessions, which acts like a Kleene star [BLMvT16],
creating infinitely many copies of a thread sequentially rather than in
parallel. The strategy $\varsigma$, shows clearly that such a strengthened
model of the system, where runs of readers with the same ePassport are
sequentialised using a Kleene star, will not prevent the attack we describe.
Thus strengthening the specification of strong unlinkability only by
sequentialising readers will not allow strong unlinkability to be verified.
Furthermore, clearly only one ePassport is needed for all attacks we present,
so also sequentialising the runs of an ePassport will not affect our analysis.

Figure 11. Message sequence chart representation of the left branch in Fig. 10
for $\textit{System}_{\textit{BAC}}$.

The second thing to observe about $\varsigma$ is that we can extract message
sequence charts (MSCs) from Fig. 10 describing the actions of an attacker
required to realise either branch of this attack strategy. Such an MSC is
presented in Fig. 11. An MSC is fundamentally not designed to represent the
branching time and different perspectives in games, however the MSC presented
is an accurate depiction of the left branch of the strategy in Fig. 10 from
the perspective of the system. Observe that, in Fig. 11, the reader concerned
is loaded with the keys of the ePassport present, corresponding to action
$\overline{\textit{passport}}{(c_{1})}$ and
$\overline{\textit{reader}}{(c_{3})}$, and then the attacker relays messages
between the ePassport and the reader, where the actions of the honest reader
and ePassport correspond to the five actions in the left branch of the
strategy, which eventually result in a non-error message. In contrast, if the
run of the reader was loaded with different keys, as in the left branch of the
specification in Fig. 10, then the final message would be an error. Hence this
is the distinguishing strategy, when, according to the specification, the
honest session of the reader will be, or should have been with high
likelihood, present elsewhere. This is how we interpret what the right branch
of the strategy accounts for.

The MSC conveys different information to the depiction of the strategy. The
fake reader and fake ePassport are implicit in this symbolic model, since the
attacker is the observer interacting with the observables of the honest
participants. However, in the MSC we make the steps that an attacker must
perform explicit, which assists us with communicating the attack to
stakeholders. ICAO and ISO experts acknowledged they understood the attack
presented in this way for the purpose of responsible disclosure [Del19].

The MSC diagram in Fig. 11 was easy for students to understand as the basis of
an implementation to demonstrate the feasibility of the attack and for the
evaluation of the wider socio-technical context333
https://github.com/bboyifeel/bac-protocol-unlinkability-exploitation
Repository with implementations of fake reader and fake ePassport for testing
the feasibility of attacks. Maintained by Igor Filimonov. . The dissemination
of that broader study is ongoing. We found off-the-shelf readers typically
keep the keys of an ePassport loaded until new keys are loaded, making the
attack strategy easier than expected by allowing multiple attempts at
reidentifying ePassports. The attack may even be triggered inadvertently,
simply by having an ePassport in the proximity of a reader loaded with the
wrong keys, in fact, this happened live in a lecture where the objective was
just to show ePassports could be read by off-the-shelf apps – the fact that an
ePassport in the vicinity inadvertently triggered an error message told us it
was not the same as the one the was previously used. This makes the
vulnerability uncovered a real risk, particularly, when the ICAO 9303 standard
is being deployed for multiple purposes, not just at airport gates; a risk
confounded by a proliferation of powerful RFID readers and covert components,
such as 180 micron thick overlay cards [And21]. Stakeholders implementing and
deploying ePassport readers should be aware of this risk and possible
mitigation strategies. One may argue that there are more serious side-channel
attacks; however, side-channel attacks may be addressed by better
implementations of ePassports, while the vulnerability we uncover will remain
since it is tied to the specification.

In science in general, interpreting the outputs of a model requires domain
expertise. Security is no exception; hence we expect that there exist further
attacks on the BAC protocol that can be uncovered by selecting a
distinguishing formula and interpreting it meaningfully in a range of socio-
technical scenarios where eDocuments play a role. For example, for the attacks
presented several actions can be permuted, such as the first two actions in
$\varsigma$ creating the ePassport and reader channels, without changing
fundamental strategy. Some of these permutations may give rise to slightly
different scenarios to those described. The essence will however be the same –
the attacker can chose between multiple combinations of devices in order to
attempt an authentication session, when, ideally, only one combination of
ePassport and reader run should work.

###  4.3. Without else branches there is still an attack.

Some papers that analyse the BAC protocol drop the else branch [CDS20]. This
is convenient since not all tools and methods handle else branches. For
example, we may instead try to use the following model of an ePassport in the
system and specification processes.

$\begin{array}[]{rl}P_{\textit{BAC}}^{no\\_else}(c,ke,km)\triangleq&\begin{array}[t]{l}\nu
nt.\mathopen{\mathopen{\overline{c}}\left<nt\right>}.c(y).\\\
\mathopen{\left[\mathopen{\texttt{snd}}\left(y\right)=\mathopen{\texttt{missing}}{mac}\left(\mathopen{\texttt{fst}}\left(y\right),km\right)\right]}\mathopen{\left[nt=\mathopen{\texttt{fst}}\left(\mathopen{\texttt{snd}}\left(\mathopen{\texttt{missing}}{dec}\left(\mathopen{\texttt{fst}}\left(y\right),ke\right)\right)\right)\right]}\\\
\nu
kt.\texttt{let}\,m=\left\\{\left<{nt},\,{\left<{\mathopen{\texttt{fst}}\left(\mathopen{\texttt{missing}}{dec}\left(\mathopen{\texttt{fst}}\left(y\right),ke\right)\right)},\,{kt}\right>}\right>\right\\}_{ke}\,\texttt{in}\,\mathopen{\mathopen{\overline{c}}\left<m,\mathopen{\texttt{missing}}{mac}\left(m,km\right)\right>}\end{array}\end{array}$

However, even for this variant, using bisimilarity, we discover an attack on
unlinkability. To see why, observe that if authentication succeeds, instead of
checking the final message sent by the ePassport is not an error, it is
sufficient to check that some message is sent at that point. If no message was
transmitted, then we can infer the tests on the nonce failed.

A classical $\mathcal{F}\\!\mathcal{M}$ formula distinguishing the system from
the specification, obtained using the process above to model the ePassport in
the scheme at the top of this section, is as follows.

$\varphi^{\prime}\triangleq\begin{array}[t]{l}\mathopen{\big{\langle}\overline{\textit{reader}}(c_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{\textit{reader}}(c_{2})\big{\rangle}}\mathopen{\big{\langle}\overline{\textit{passport}}(c_{3})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(nt)\big{\rangle}}\Big{(}\\\
\qquad\begin{array}[t]{rl}&\mathopen{\big{\langle}c_{1}\,nt\big{\rangle}}\mathopen{\big{\langle}\overline{c_{1}}(\varw)\big{\rangle}}\mathopen{\big{\langle}c_{3}\,\varw\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(z)\big{\rangle}}\mathtt{tt}\\\
\wedge&\mathopen{\big{\langle}c_{2}\,nt\big{\rangle}}\mathopen{\big{\langle}\overline{c_{2}}(\varw)\big{\rangle}}\mathopen{\big{\langle}c_{3}\,\varw\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(z)\big{\rangle}}\mathtt{tt}~{}\Big{)}\end{array}\end{array}$

Notice the difference compared to $\varphi$ is that $\varphi^{\prime}$ does
not need to test to check that $z$ is not an error. Indeed, when we reach the
final action of the distinguishing strategy, the specification is unable to
perform any action on channel $c_{3}$, hence cannot simulate the behaviour of
the system.

###  4.4. From bisimilarity to notions of similarity

As we have already pointed out for Fig. 9, the leader in the strategy in Fig.
10 is always the same. Thus we do not require the full power of bisimilarity
to discover either of these attack strategies, nor even the strategy described
by $\varphi^{\prime}$ in Sec. 4.3. Indeed, to specify this unlinkability
problem, it is sufficient to use a similarity preorder, which is obtained from
strong early bisimilarity in Def. 4 by dropping the requirement that the
relation is symmetric. To be explicit, in the specification of unlinkability,
we could employ the following notion of similarity instead of bisimilarity.
[similarity] A relation between extended processes $\mathrel{\mathcal{R}}$ is
a strong early simulation only if, whenever $A\mathrel{\mathcal{R}}B$ the
following hold:

  * •

$A$ and $B$ are statically equivalent.

  * •

If $A\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{12.0pt}{0.6pt}}\limits^{\pi}$}\mkern-7.0mu\blacktriangleright}A^{\prime}$
there exists $B^{\prime}$ such that $B\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{12.0pt}{0.6pt}}\limits^{\pi}$}\mkern-7.0mu\blacktriangleright}B^{\prime}$
and $A^{\prime}\mathrel{\mathcal{R}}B^{\prime}$.

Process $P$ is simulated by processes $Q$, written $P\preceq Q$, whenever
there exists a strong early simulation $\mathcal{R}$ such that
$P\mathrel{\mathcal{R}}Q$. In both the old scheme for unlinkability, as
communicated in CSF’10, and in our new updated scheme introduced in this
section, it is trivial that the process modelling the specification, e.g.,
$\textit{Spec}_{\textit{BAC}}$, is simulated by the system process
$\textit{System}_{\textit{BAC}}$, i.e.,
$\textit{Spec}_{\textit{BAC}}\preceq\textit{System}_{\textit{BAC}}$ holds. To
see why, intuitively, observe that if we have full control of the system we
can always make it behave like the specification by never using the same
ePassport twice thus the specification can be simulated by the system. Hence,
the problem of checking unlinkability, when cast as a similarity problem, can
be formulated by the problem of checking whether
$\textit{System}_{\textit{BAC}}\preceq\textit{Spec}_{\textit{BAC}}$, i.e.,
checking whether any observable behaviours the system can perform can be
simulated by behaviours of the specification. Stated as a theorem, we have the
following which tightens Theorem 1, where the proof follows from the same
strategy as presented in Fig. 9.

######  Theorem 11.

$\textit{System}_{\textit{BAC}}\preceq\textit{Spec}_{\textit{BAC}}$ does not
hold.

It is helpful to know that similarity is sufficient for this problem, since
similarity preorders have compelling attacker models, e.g., in terms of
probabilistic testing semantics [DvGHM08]. Indeed, it is standard in
cryptography to assume that an adversary has the power of a probabilistic
polynominal-time Turing machine, even if the protocol does not contain
probabilistic choices, which is reflected in power made available to the
attacker by adopting similarity.

######  Remark 12.

There are several variants of similarity in the linear-time / branching-time
spectrum [vG01], which, as touched on in Sec. 2.5, could be compelling choices
for modelling the capabilities of attackers. We argue that a more broadly
applicable design decision would be to employ a stronger notion of similarity
called failure similarity. For example, failure similarity can distinguish
process
${\mathopen{!}\mathopen{\mathopen{\overline{a}}\left<go\right>}.\mathopen{\mathopen{\overline{a}}\left<error\right>}}\mathrel{\mid}{\mathopen{!}\mathopen{\mathopen{\overline{a}}\left<go\right>}}$
from
$\mathopen{!}\mathopen{\mathopen{\overline{a}}\left<go\right>}.\mathopen{\mathopen{\overline{a}}\left<error\right>}$,
whereas similarity in Definition 4.4 cannot distinguish these processes. Thus
we can test that an event does not happen, e.g., by using a timeout [vG21],
which is a distinction that cannot be made using similarity.

Such additional expressive power is not required in order to detect
unlinkability attacks on the BAC protocol, but might be useful in some
scenarios where, for example, the attacker can explicitly observe an error due
to the presence of a message, but cannot explicitly observe a success. In such
scenarios, a success can be inferred by observing that an error does not occur
within an expected time window. For example, the ICAO 9303 specification of
the PACE protocol [MRT15] only requires the ePassport to send an error message
at the end of an unsuccessful authentication session, but does not require it
to send any message if the session results in authentication being successful;
hence successful authentication from the perspective of an ePassport can be
inferred by the absence of an error message at the end of the session within
an expected time window. However, when we model the PACE protocol in Sec. 5,
we use explicit observables for success so as to align with related work,
thereby avoiding unnecessary debate about whether our attacks are particular
to how we model the PACE protocol (they are not). Thus, it is safest to verify
unlinkability with respect to bisimilarity, which covers all such attacks,
including the richer strategy in Fig. 8. Recall, in Sec. 3, that, by using
domain knowledge, we were able to assign a practical meaning to the strategy
in Fig. 8, which failure similarity does not detect.

##  5\. Unlinkability of the PACE protocol

We address the public communication from the office of the secretary general
of ICAO, discussed in the introduction, which challenges whether the
unlinkability vulnerability discovered on the BAC protocol is valid for more
recent versions of the ICAO 9303 ePassport standard [MRT15]. This is a
reasonable question, since the $7^{th}$ edition of the ICAO 9303 standard
recommends the Password Authenticated Connection Establishment protocol
(PACE), as a more secure alternative to BAC.

The PACE protocol does improve on the security of the BAC protocol, making
attacks giving access to private data stored on the chip more difficult. For
example, the PACE protocol satisfies forward secrecy [BFK09, CGIP12]; whereas
the BAC protocol does not, that is: if an attacker intercepts ciphertexts in
anticipation of, in the future, discovering the key for the ePassport, then
she cannot go back and use the key to discover the session key and reveal the
encrypted secrets from those old runs of the protocol.

The PACE protocol also eliminates unlinkability vulnerabilities caused by
using different errors when the protocol fails for different reasons, as was
the case for an implementation of the BAC protocol for French ePassports. Thus
we believe that some of the most serious types of attack on unlinkability
exploiting the BAC protocol have been addressed in the PACE protocol, where
such attacks on the BAC protocol allow an ePassport holder with an
implementation interpreting the specification in a particular way to be
tracked forever after the messages from one session with a trusted reader have
been intercepted.

The clause of the standard that restricts the use of error messages is the
following line in section 4.4.2 of part 11 of the ICAO 9303 standard.

> “An eMRTD chip that supports PACE SHALL respond to unauthenticated read
> attempts (including selection of (protected) files in the LDS) with
> “Security status not satisfied” (0x6982).”

The above explicit statement is an improvement over the specification of the
BAC protocol; however there are still unlinkability vulnerabilities in the
PACE protocol as specified in the ICAO 9303 standard. Similarly to the
vulnerability in the BAC protocol, studied throughout previous sections, there
are vulnerabilities in the PACE protocol valid due to differences between a
successful and failed authentication session observable to an attacker, such
as the presence of the error message highlighted above. We formally analyse
this vulnerability using bisimilarity following our revised approach to
unlinkability justified in Sec. 4.

###  5.1. The PACE protocol

Figure 12. The PACE protocol, using a generic mapping based on Diffie-Hellman
Key Agreement.

There are multiple ways to interpret the PACE protocol since it has various
operational modes that permit a number of cryptographic primitives to be used
at each stage for establishing shared keys. We model here the generic mapping
which uses a Diffie-Hellman key exchange. The message exchange, presented in
Fig. 12, follows closely related work communicated in the Journal of Computer
Security [HBD19], thereby avoiding unnecessary debate on how the protocol is
interpreted.

The message flow in Fig. 12 is as follows.

  1. (1)

The ePassport shares information for generating a key $k$ with the reader,
usually via an OCR session with the biometric page of the ePassport. This is
represented by the dotted line at the top of the figure. PACE uses better
sources of randomness than BAC, however this does not affect our unlinkability
analysis.

  2. (2)

The ePassport key uses the key $k$ to transmit an encrypted nonce
$\left\\{s\right\\}_{k}$ to the reader.

  3. (3)

The ePassport and reader employ one of several operational modes to create
additional randomness for each session. We model the “generic mapping”
operational mode which employs a Diffie-Hellman handshake. This information is
used to generate shared key
$G=\mathopen{\texttt{gen}}\left({(g^{nr})}^{nt},s\right)$, where
$\mathopen{\texttt{gen}}\left(\cdot,\cdot\right)$ is key generation function.
Notice $G=\hat{G}$ in Fig. 12.

  4. (4)

A Diffie-Hellman handshake is performed using $G$ as the generator, which is
used to compute a MAC key $km$. Also an encryption key for the secure
messaging phase, which we do not model, is generated at this point. Again
$km=\hat{km}$. The checks $G^{nr}\neq G^{nt}$ at this point avoid reflection
attacks, where an ePassport or reader is used to authenticate itself.

  5. (5)

Finally the ePassport and reader exchange and verify MACs, using the MAC key
$km$, authenticating the public keys exchanged in the previous step. If
authentication fails at this point an error message is produced. Notice we
include the above mentioned error message (0x6982) if authentication fails at
the end of the protocol.

###  5.2. PACE in the applied $\pi$-calculus

For the PACE protocol we require an extended message theory. We require
symmetric encryption, where decryption is not detectable (modelled by the same
equations as employed for the BAC protocol). For the Diffie-Hellman exchanges
we require exponentiation and also a key generating map, which acts like a two
parameter hash function. As for the BAC protocol, MACs are modelled as a two
parameter hash function. This message theory is presented below.

$\displaystyle\begin{array}[]{rlr}M,N\Coloneqq&x&\mbox{variable}\\\
\mid&\mathopen{\texttt{missing}}{mac}\left(M,N\right)&\mbox{mac}\\\
\mid&\mathopen{\texttt{gen}}\left(M,N\right)&\mbox{generator}\\\
\mid&M^{N}&\mbox{exponentiation}\\\
\mid&\left\\{M\right\\}_{N}&\\!\\!\\!\\!\mbox{encryption}\\\
\mid&\mathopen{\texttt{missing}}{dec}\left(M,N\right)&\mbox{decryption}\end{array}\qquad\qquad\begin{array}[]{c}\mathopen{\texttt{missing}}{dec}\left(\left\\{M\right\\}_{K},K\right)=_{E^{\prime}}M\\\\[12.0pt]
\left\\{\mathopen{\texttt{missing}}{dec}\left(M,K\right)\right\\}_{K}=_{E^{\prime}}M\\\\[12.0pt]
{(M^{N})}^{K}=_{E^{\prime}}{(M^{K})}^{N}\end{array}$

The ePassport and reader for the PACE protocol can be modelled in the applied
$\pi$-calculus as follows.

$\displaystyle P_{\textit{PACE}}(c,k)\triangleq\begin{array}[t]{l}\nu
s.\mathopen{\mathopen{\overline{c}}\left<\left\\{s\right\\}_{k}\right>}.c(x).\mathopen{\mathopen{\overline{c}}\left<g^{nt}\right>}.\\\
\texttt{let}\,G=\mathopen{\texttt{gen}}\left(s,x^{nt}\right)\,\texttt{in}\\\
c(y).\nu
nt^{\prime}.\mathopen{\mathopen{\overline{c}}\left<G^{nt^{\prime}}\right>}\\\
\mathopen{\left[G^{nt^{\prime}}\neq y\right]}c(z).\\\
\texttt{let}\,km=z^{nt^{\prime}}\,\texttt{in}\\\
\texttt{if}\,z=\mathopen{\texttt{missing}}{mac}\left(G^{nt^{\prime}},km\right)\\\
\texttt{then}\,\mathopen{\mathopen{\overline{c}}\left<\mathopen{\texttt{missing}}{mac}\left(z,km\right)\right>}\\\
\texttt{else}\,\mathopen{\mathopen{\overline{c}}\left<\textit{error}\right>}\end{array}\qquad
V_{\textit{PACE}}(c,k)\triangleq\begin{array}[t]{l}c(x).\mathopen{\mathopen{\overline{c}}\left<g^{nr}\right>}.c(y).\\\
\texttt{let}\,G=\mathopen{\texttt{gen}}\left(\mathopen{\texttt{missing}}{dec}\left(x,k\right),y^{nr}\right)\,\texttt{in}\\\
\nu
nr^{\prime}.\mathopen{\mathopen{\overline{c}}\left<G^{nr^{\prime}}\right>}.c(z).\\\
\mathopen{\left[G^{nr^{\prime}}\neq
z\right]}\texttt{let}\,km=z^{nr^{\prime}}\,\texttt{in}\\\
\mathopen{\mathopen{\overline{c}}\left<\mathopen{\texttt{missing}}{mac}\left(z,km\right)\right>}\\\
c(m).\mathopen{\left[m=\mathopen{\texttt{missing}}{mac}\left(G^{nr^{\prime}},km\right)\right]}c(n)\end{array}$

Notice only the ePassport features an error message if authentication fails in
the final step. Also, we add a dummy event $c(n)$ at the end of the reader
session, for the sake of modelling that a reader will proceed to do something
after successfully authenticating. This is to align with related work in
communicated in the Journal of Computer Security [HBD19], in order to
facilitate a comparison of results obtained.

Using the above processes, and our revised scheme for unlinkability in the
previous section we obtain the following result confirming there are attacks
on the unlinkability of PACE.

######  Theorem 13.

$\textit{System}_{\textit{PACE}}\not\sim\textit{Spec}_{\textit{PACE}}$, where

$\begin{array}[]{rl}\textit{System}_{\textit{PACE}}\triangleq&\mathopen{!}\mathopen{\nu
k.}\mathopen{!}\left(\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{passport}}}\left<c\right>}.P_{\textit{PACE}}(c,k)\mathrel{\mid}\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{reader}}}\left<c\right>}.V_{\textit{PACE}}(c,k)\right)\\\
\textit{Spec}_{\textit{PACE}}\triangleq&\mathopen{!}\mathopen{\nu{k}.}\left(\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{passport}}}\left<c\right>}.P_{\textit{PACE}}(c,{k})\mathrel{\mid}\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{reader}}}\left<c\right>}.V_{\textit{PACE}}(c,{k})\right)\end{array}$

######  Proof 5.1.

Consider the following $\mathcal{F}\\!\mathcal{M}$ formula.

$\xi\triangleq\begin{array}[t]{l}\mathopen{\big{\langle}\overline{\textit{reader}}(c_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{\textit{reader}}(c_{2})\big{\rangle}}\mathopen{\big{\langle}\overline{\textit{passport}}(c_{3})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(t)\big{\rangle}}\Big{(}\\\
\begin{array}[t]{rl}&\mathopen{\big{\langle}c_{1}\,t\big{\rangle}}\mathopen{\big{\langle}\overline{c_{1}}(u)\big{\rangle}}\mathopen{\big{\langle}c_{3}\,u\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(v)\big{\rangle}}\mathopen{\big{\langle}c_{1}\,v\big{\rangle}}\mathopen{\big{\langle}\overline{c_{1}}(w)\big{\rangle}}\\\
&\quad\mathopen{\big{\langle}c_{3}\,w\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(x)\big{\rangle}}\mathopen{\big{\langle}c_{1}\,x\big{\rangle}}\mathopen{\big{\langle}\overline{c_{1}}(y)\big{\rangle}}\mathopen{\big{\langle}c_{3}\,y\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(z)\big{\rangle}}\left(z\neq\textit{error}\right)\\\\[5.0pt]
\wedge\\!\\!\\!\\!\\!&\mathopen{\big{\langle}c_{2}\,t\big{\rangle}}\mathopen{\big{\langle}\overline{c_{2}}(u)\big{\rangle}}\mathopen{\big{\langle}c_{3}\,u\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(v)\big{\rangle}}\mathopen{\big{\langle}c_{2}\,v\big{\rangle}}\mathopen{\big{\langle}\overline{c_{2}}(w)\big{\rangle}}\\\
&\quad\mathopen{\big{\langle}c_{3}\,w\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(x)\big{\rangle}}\mathopen{\big{\langle}c_{2}\,x\big{\rangle}}\mathopen{\big{\langle}\overline{c_{2}}(y)\big{\rangle}}\mathopen{\big{\langle}c_{3}\,y\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(z)\big{\rangle}}\left(z\neq\textit{error}\right)~{}\Big{)}\end{array}\end{array}$

Since $\textit{System}_{\textit{PACE}}\models\xi$, but
$\textit{Spec}_{\textit{PACE}}\not\models\xi$, by Theorem 8,
$\textit{System}_{\textit{PACE}}\not\sim\textit{Spec}_{\textit{PACE}}$.

The formula $\xi$ proving that unlinkability does not hold for the PACE
protocol follows a similar pattern to the formula $\varphi$, used in the
previous section to certify that BAC fails unlinkability. In this strategy,
the system starts two readers and an ePassport with the same keys. The
specification can only follow using a strategy where one of the readers will
fail authentication. To win this game, the system simply chooses to
authenticate with the reader that is expected to fail in the specification.
That reader will obviously successfully authenticate in the system, thereby
concluding our distinguishing strategy.

###  5.3. Another attack strategy from related work.

Infinitely many distinguishing strategies exist violating the unlinkability of
the PACE protocol. Indeed related work [HBD19] discovered a violation of the
unlinkability of the PACE protocol, that can be described as a trace. An
attack on unlinkability formulated using trace equivalence is always also an
attack on bisimilarity. The added value that our methodology brings to that
attack, is that we can certify their attack by using the following classical
$\mathcal{F}\\!\mathcal{M}$ formula, describing the distinguishing trace
discovered in the above mentioned related work. The
$\mathcal{F}\\!\mathcal{M}$ formulae characterising trace equivalence are
those consisting of diamond modalities only ending with some formula that does
not involve modalities.

$\vartheta\triangleq\begin{array}[t]{l}\mathopen{\big{\langle}\overline{\textit{reader}}(c_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{\textit{reader}}(c_{2})\big{\rangle}}\mathopen{\big{\langle}\overline{\textit{passport}}(c_{3})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{3}}(t)\big{\rangle}}\mathopen{\big{\langle}c_{1}\,t\big{\rangle}}\mathopen{\big{\langle}c_{2}\,t\big{\rangle}}\\\
\mathopen{\big{\langle}\overline{c_{1}}(u_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{2}}(u_{2})\big{\rangle}}\mathopen{\big{\langle}c_{2}\,u_{1}\big{\rangle}}\mathopen{\big{\langle}c_{1}\,u_{2}\big{\rangle}}\mathopen{\big{\langle}\overline{c_{1}}(v_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{2}}(v_{2})\big{\rangle}}\mathopen{\big{\langle}c_{2}\,v_{1}\big{\rangle}}\mathopen{\big{\langle}c_{1}\,v_{2}\big{\rangle}}\\\
\mathopen{\big{\langle}\overline{c_{1}}(w_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{2}}(w_{2})\big{\rangle}}\mathopen{\big{\langle}c_{2}\,w_{1}\big{\rangle}}\mathopen{\big{\langle}c_{1}\,w_{2}\big{\rangle}}\mathopen{\big{\langle}\overline{c_{1}}(x_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{2}}(x_{2})\big{\rangle}}\mathopen{\big{\langle}c_{2}\,x_{1}\big{\rangle}}\mathopen{\big{\langle}c_{1}\,x_{2}\big{\rangle}}\\\
\mathopen{\big{\langle}\overline{c_{1}}(y_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{2}}(y_{2})\big{\rangle}}\mathopen{\big{\langle}c_{2}\,y_{1}\big{\rangle}}\mathopen{\big{\langle}c_{1}\,y_{2}\big{\rangle}}\mathopen{\big{\langle}\overline{c_{1}}(z_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{2}}(z_{2})\big{\rangle}}\mathopen{\big{\langle}c_{2}\,z_{1}\big{\rangle}}\mathopen{\big{\langle}c_{2}\,m\big{\rangle}}\mathtt{tt}\end{array}$

In the strategy described by the formula above, the encrypted nonce sent by
the ePassport at the beginning of the protocol is replayed to two different
readers. The two readers are then used to authenticate each other, exploiting
the fact that the protocol is symmetric in the role of the reader and
ePassport. Authentication will only be successful if both readers have the
same keys, otherwise either reader will fail the check on the MAC at the final
step of the PACE protocol. Thus, assuming that a reader does something after
authentication, we learn whether both readers talked with the same ePassport.

The attack $\vartheta$ is quite different from attack $\xi$. Notice
$\vartheta$ requires two readers to be fully active during the attack, not
simply present in principle, as a choice in a game, suggesting that it may be
more difficult to exploit, despite being described as a trace. Also, notice
the attack can be mitigated in several ways, e.g., by initially responding to
the ePassport in the same way regardless of whether it authenticates or not,
hence, since an ePassport cannot also be authenticated at the same time, there
is no way to continue with the secure messaging phase. An alternative fix
preventing this attack is proposed in related work [HBD19], modifying the
protocol such that additional role specific information is added to the
handshake. However, these fixes will not mitigate the more serious problem
described in $\xi$, so do not really improve unlinkability.

##  6\. Related and future work

A closely related paper, that is not already covered by remarks in the body of
the paper was communicated in S&P’18 [CKR18]. That paper announces the
discovery of attacks on the BAC protocol using the bounded trace equivalence
checker DeepSec, but without further discussion. An interesting difference
between that paper and the current work is that, while we build on the
original formulation of unlinkability, as communicated in CSF’10 [ACRR10]; the
S&P’18 paper proposes another model where, instead of using a specification
process, unlinkability is modelled in terms of two systems where the number of
identical users in the system differ. In their alternative model, one process
models two sessions featuring the same ePassport twice, which is compared to
another process featuring two sessions each featuring a different ePassport.
That is, unlinkability is formulated such that the following two processes are
compared, using trace equivalence.

$\textit{Diff}\triangleq\begin{array}[t]{l}\mathopen{\nu ke.\nu
km.}\left(V_{\textit{BAC}}(c_{r},ke,km)\mathrel{\mid}P_{\textit{BAC}}(c_{p},ke,km)\right)\mathrel{\mid}\\\
\mathopen{\nu ke.\nu
km.}\left(V_{\textit{BAC}}(c_{r},ke,km)\mathrel{\mid}P_{\textit{BAC}}(c_{p},ke,km)\right)\end{array}$
$\textit{Same}\triangleq\begin{array}[t]{l}\mathopen{\nu ke.\nu
km.}\bigl{(}V_{\textit{BAC}}(c_{r},ke,km)\mathrel{\mid}P_{\textit{BAC}}(c_{p},ke,km)\mathrel{\mid}\\\
\phantom{\mathopen{\nu ke.\nu
km.xx}}V_{\textit{BAC}}(c_{r},ke,km)\mathrel{\mid}P_{\textit{BAC}}(c_{p},ke,km)\bigr{)}\end{array}$

In the above $c_{r}$ and $c_{p}$ are used as fixed channels for communications
with all ePassports or all readers respectively. Attack traces discovered
using the above method, communicated in S&P’18, can be used to confirm that
two sessions are certainly not with the same ePassport. In particular,
consider the following formula describing a trace that holds for the first
process but does not hold for the second process.

$\textit{Diff}\models\begin{array}[t]{l}\mathopen{\big{\langle}\overline{c_{p}}(n_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{p}}(n_{2})\big{\rangle}}\mathopen{\big{\langle}c_{r}\,n_{2}\big{\rangle}}\mathopen{\big{\langle}c_{r}\,n_{2}\big{\rangle}}\\\
\qquad\mathopen{\big{\langle}\overline{c_{r}}(m_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{r}}(m_{2})\big{\rangle}}\mathopen{\big{\langle}c_{p}\,m_{1}\big{\rangle}}\mathopen{\big{\langle}c_{p}\,m_{2}\big{\rangle}}\mathopen{\big{\langle}\overline{c_{p}}(e_{1})\big{\rangle}}\mathopen{\big{\langle}\overline{c_{p}}(e_{2})\big{\rangle}}\left(e_{1}=\textit{error}\wedge
e_{2}=\textit{error}\right)\end{array}$

In the first line of the above trace, the first two messages correspond to
sending two nonces, and only the second nonce is fed as an input to both
readers. On the second line of the formula, the protocol continues for both
sessions and the protocol ends with both ePassports sending error messages. If
both readers are using the same nonce, then both ePassports can only send
error messages at the last step if both ePassports are different; if both were
the same ePassport then one of the two sessions would successfully
authenticate, hence there could not have been two error messages. I.e., it is
impossible for Same to satisfy the above formula.

The limitation we see is the above mentioned approach communicated in S&P’18
discovers attack traces that cannot be used to positively confirm that two
sessions are with the same ePassport. What we mean is that there is no trace
that holds for the process Same that does not hold for the process Diff; but
for a trace-like attack on unlinkability we should surely be able to provide a
trace that links two sessions. Thus we should be careful interpreting the
above result — it does not mean that the above method discovers an attack on
unlinkability that is in the form of a trace.

Further discussion on the above model of unlinkability appears in the
conference version of this paper [FHMS19], where it is clarified that the
above limitation is due to modelling decisions and is not a feature of the
DeepSec tool that the S&P’18 paper showcases. The DeepSec tool can also be
used to verify finite formulations of the unlinkability problem using our
preferred “system v.s. specification” approach — in which case DeepSec
discovers no attacks that are in the form of a trace for the BAC protocol. In
particular, DeepSec can verify that Diff is trace equivalent to the following
process where either there is a choice between starting the second session
with the same keys as the first or with the new keys, which is a bounded
approximation of the system following established schemes for unlinkability.

$\mathopen{\nu ke.\nu
km.}\Big{(}\begin{array}[t]{l}V_{\textit{BAC}}(c_{r},ke,km)\mathrel{\mid}P_{\textit{BAC}}(c_{p},ke,km)\mathrel{\mid}\\\
\big{(}\begin{array}[t]{l}\left(V_{\textit{BAC}}(c_{r},ke,km)\mathrel{\mid}P_{\textit{BAC}}(c_{p},ke,km)\right)+\\\
\mathopen{\nu·ke,km.}\left(V_{\textit{BAC}}(c_{r},ke,km)\mathrel{\mid}P_{\textit{BAC}}(c_{p},ke,km)\right)~{}\big{)}~{}\Big{)}\end{array}\end{array}$

In the above process, $+$ is non-deterministic choice, which is easy to add to
the applied $\pi$-calculus.

An approach similar to the approach communicated in S&P’18, where two systems
are compared in which users in a system are permuted, has been thoroughly
investigated and demonstrated to be the preferable approach for formulating
voter privacy, which is a property of eVoting systems [DKR09]. We should
clarify that we are not arguing against using a “permutations of a system”
approach to voter privacy. What we are arguing is that the “system vs.
specification” approach adopted in the current paper and in the CSF’10 paper
is appropriate for unlinkability, since if an attack trace is discovered the
attack trace will be able to positively confirm that two sessions are with the
same ePassport, i.e., the sessions will be linked.

###  6.1.  A preliminary discussion on mitigation strategies

We summarise here three quite different mitigation strategies and present some
preliminary findings.

####  6.1.1. Timeouts

A mitigation strategy, which we have recommended to stakeholders, is to
guarantee that implementations of readers only hold ePassport keys for a short
period of time. This would render the reader useless in an attack strategy
where the goal is to reidentify someone in the future. In Fig. 11, the time to
keep small is indicated by $t$: the time between the reader being prepared
with they keys of a particular passport and the RFID session being triggered.
This eliminates use cases where an ePassport holder who has recently passed
through a checkpoint is reidentified, but might not mitigate other use cases.
For example, a user may be expected to approach a reader, e.g., to provide
their identity at a service desk, and hence the reader is loaded with a
particular key in a time window. In that case, an attacker may attempt to find
who was intended to be at the service desk without them being present. An
extensive study of use cases emerging we push to future work.

The above mitigation strategy can be modelled by imposing causal dependencies
in our model. A timeout built into the reader would allow a single run of an
ePassport to occur before the reader session times out. Thus the creation of a
new run of an ePassport causally depends on any events of an ongoing run of a
reader involving the same ePassport, which must first be completed. In
addition, we can assume that ePassport runs themselves are sequentially
ordered, by the nature of the chip. We may also assume that the readers are
loaded with the keys of a single ePassport sequentially, e.g., along a path
through checkpoints. Surprisingly, forcing all these causal assumptions would
still not be enough to prevent the attack $\varsigma$ on unlinkability
presented in Section 4.2, since we have not stipulated that a single ePassport
run can be held open for a length of time sufficient for the attacker to
choose between relaying message to one of two readers in a sequence, both of
which may successfully authenticate the ePassport. Thus there must be a fourth
causal dependency imposed to prevent attacks, which is not enforced by a
timeout for the reader: we should prevent a new reader from being initiated
before any run of an ePassport involving the same keys terminates. This does
not model a timeout imposed by the reader, but instead a timeout imposed in
practice by how long an attacker can keep a device in the vicinity of an
ePassport holder.

If we make all four causal assumptions in the paragraph above, the effect is
each run of an ePassport and its corresponding reader session are
sequentialised together, in parallel. That is, a run of an ePassport and a
reader must both be used entirely before any new run can be created involving
the keys of the same ePassport. This can be modelled by making use of a Kleene
star operator  ! , proposed in related work [Bae21], in the following
alternative scheme for the system.

$\mathopen{!}\mathopen{\nu\vec{k}.}\mathopen{\rotatebox[origin={c}]{180.0}{!}}\left(\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{passport}}}\left<c\right>}.\textit{Prover}(c,\vec{k})\mathrel{\mid}\mathopen{\nu
c.}\mathopen{\mathopen{\overline{\textit{reader}}}\left<c\right>}.\textit{Verifier}(c,\vec{k})\right)$

Our hypothesis is that the above process is bisimilar to the scheme for the
specification for both the BAC and PACE protocols. An account of the semantics
of  ! in this context and a proof of this claim are pushed to future work.

####  6.1.2. Obscuring messages.

Another alternative is to probabilistically encrypt the error message, or
produce random noise when the ePassport fails to authenticate the reader. Note
this is within the scope of the BAC protocol specification, since the
specification does not fix the form of the error message. Nevertheless, to our
best knowledge, real ePassports implementing the BAC protocol send errors as
constant plaintext messages. This mitigation strategy would only be effective
for use cases where the attacker cannot observe the consequences of using an
eDocument. For example, one may consider a “polite” registration system where
you are offered to register using your electronic identity, but choosing not
to or not succeeding to do so is permitted. Perhaps those who do not provide
their electronic identities will be picked up by other safety nets such as a
human attendant who later checks participants against a register rather than
as an immediate effect such as the opening of a gate.

Such a refinement of the BAC protocol where error messages are obscured, does
in fact satisfy unlinkability, as long as nothing happens after executing the
BAC protocol. We can model one such variant of the BAC protocol as follows.

$\begin{array}[]{rl}P_{\textit{BAC}}^{fixed}(c,ke,km)\triangleq&\begin{array}[t]{l}\nu
nt.\mathopen{\mathopen{\overline{c}}\left<nt\right>}.c(y).\\\
\texttt{if}\,\mathopen{\texttt{snd}}\left(y\right)=\mathopen{\texttt{missing}}{mac}\left(\mathopen{\texttt{fst}}\left(y\right),km\right)\,\texttt{then}\\\
\qquad\begin{array}[t]{l}\texttt{if}\,nt=\mathopen{\texttt{fst}}\left(\mathopen{\texttt{snd}}\left(\mathopen{\texttt{missing}}{dec}\left(\mathopen{\texttt{fst}}\left(y\right),ke\right)\right)\right)\,\texttt{then}\\\
\qquad\begin{array}[t]{l}\nu
kt.\texttt{let}\,m=\left\\{\left<{nt},\,{\left<{\mathopen{\texttt{fst}}\left(\mathopen{\texttt{missing}}{dec}\left(\mathopen{\texttt{fst}}\left(y\right),ke\right)\right)},\,{kt}\right>}\right>\right\\}_{ke}\,\texttt{in}\\\
\mathopen{\mathopen{\overline{c}}\left<m,\mathopen{\texttt{missing}}{mac}\left(m,km\right)\right>}\end{array}\\\
\texttt{else}\,\nu
r.\texttt{let}\,m=\left\\{\left<{r},\,{\textit{error}}\right>\right\\}_{ke}\,\texttt{in}\,\mathopen{\mathopen{\overline{c}}\left<m,\mathopen{\texttt{missing}}{mac}\left(m,km\right)\right>}\end{array}\\\
\texttt{else}\,\nu
r.\texttt{let}\,m=\left\\{\left<{r},\,{\textit{error}}\right>\right\\}_{ke}\,\texttt{in}\,\mathopen{\mathopen{\overline{c}}\left<m,\mathopen{\texttt{missing}}{mac}\left(m,km\right)\right>}\end{array}\end{array}$

Let $\textit{System}_{\textit{BAC}}^{fixed}$ and
$\textit{Spec}_{\textit{BAC}}^{fixed}$ denote, respectively, the system and
specification for unlinkability of BAC where the above model of the ePassport
role is used. For this model, we have a proof that unlinkability does hold,
i.e.,
$\textit{System}_{\textit{BAC}}^{fixed}\sim\textit{Spec}_{\textit{BAC}}^{fixed}$.
The publication of a proof for this claim is pushed to future work, in the
interest of focussing on attacks in this paper.

A problem with the above refinement of the BAC protocol satisfying
unlinkability is that making BAC unlinkable does not guarantee that the whole
ePassport protocol satisfies unlinkability. The BAC protocol is just for
authentication and establishing a session key. After authenticating the
ePassport proceeds with a secure messaging phase that uses the session key to
transmit personal data stored in the ePassport [MRT15]. Thus it is sufficient
for an attacker to look at whether the protocol proceeds with secure messaging
or not in order to determine whether authentication was successful. That
knowledge can be used to the same effect as observing whether or not an error
message was sent. Thus, for the above fix to be fully effective even in a
“polite” system, the secure messaging phase should proceed even if the
ePassport does not authenticate, transmitting dummy data indistinguishable to
an observer from the real data. Such a mitigation strategy is outside the
scope of the current ICAO specification and does not significantly improve
unlinkability for the standard use cases for ePassports.

####  6.1.3. Using one-time keys.

An arguably better mitigation strategy is to use Time-based One-time Passwords
(TOTP) to make the six-digit key for PACE change periodically, as explored in
the thesis of our student [Fil20]. Verification of that strategy is immediate,
since TOTP has the effect of generating a new key for every run of the
protocol, making the system and specification trivially bisimilar.
Implementing TOTP has further security and privacy advantages, forgoing other
attacks on the system, including some social attacks, and has been deployed in
card form for ePayments, so could be easily integrated into electronic ID
cards implementing the ICAO 9303 standard. The challenge for ePassports is
more likely to be at the policy level, since questions may be raised at
international checkpoints if countries do not agree that TOTP is acceptable
technology. Dissemination of the socio-technical evaluation of this mitigation
strategy we push to future work.

###  6.2. Further risks to unlinkability

There are many potential privacy risk for the PACE protocol that are not
directly captured by the symbolic models in this work. Some are simple to
exploit, such as the fact that the PACE protocol offers several different
operational modes. In order for a reader to determine the appropriate
operational model, before starting the protocol, the ePassport declares the
operational modes of the PACE protocol that it implements. In an environment,
such as an airport, where many different ePassports implementing different
operational modes coexist, a user may be tracked with a probability better
than a random guess.

The actual probability of guessing correctly that the same ePassport is
involved in two sessions depends on the number of different implementations of
ePassport and the expected movements of their holders. We expect the advantage
gained by such a strategy to be non-negligible and it is standard in security
and privacy models that gaining a non-negligible advantage counts as an
attack. Permitting may different implementations of protocols is an oversight
of the ICAO 9303 standard.

##  7\. Conclusion

This paper confirms there are attacks on the authentication protocols proposed
in the latest ICAO 9303 specification for ePassports. Both the BAC and PACE
protocols feature attacks that can be described as a distinguishing strategy
in a game played according to a specification of what it means to satisfy
unlinkability. Attacks on the BAC protocol, communicated in Theorem 1 and
Theorem 10, are interesting since the former resolves flawed claims that no
such attack exists according to a formulation of unlinkability dating back to
CSF’10; while the latter irons out limitations of that original model
concerning the capabilities of an attacker to distinguish messages from
different readers and ePassports.

An interesting aspect of the new attack we discover on the PACE protocol, as
formulated in Theorem 13, is that it is not mitigated by defensive strategies
that may be introduced to mitigate attacks previously discovered using trace
equivalence as communicated in the Journal of Computer Security [HBD19] (e.g.,
sequentialising reader sessions will not mitigate the newly discovered attack,
nor will adding role information distinguishing messages of the same form
originating from a reader and from an ePassport). Furthermore, the attacks
discovered previously using trace equivalence require two honest readers to
actively participate in the attack, whereas the new attack discovered using
bisimilarity requires only one honest reader to actively participate in the
attack, meaning that the attack can be realised in a broader range of
scenarios. This observation challenges claims communicated in the Journal of
Computer Security, where it is argued that bisimilarity is too strong and
hence trace equivalence should be employed. Their argument is provided to
support their model that relies on trace equivalence in order to prove that
unlinkability of the BAC protocol holds. Since their results lead to
contradictory advice compared to ours, differences are worth clarifying.

The crux of their argument is based on remarks communicated in CSF’10 [ACRR10]
claiming that bisimilarity may distinguish processes due to their internal
state — an argument we contest since bisimilarity is all about the games
played between the adversary and its environment using observations only; and
never can distinctions be made based on differences in internal state (that is
the point of such observational equivalences). Presenting multiple viewpoints
is healthy for academic debate; however, the fact that the attacks we discover
using bisimilarity are not spurious and furthermore are easier to realise is
evidence that trace equivalence is insufficient for verifying interactive
systems such as security protocols. To further support our argument that the
use of bisimilarity (or, as a compromise, a suitable notion of similarity, as
discussed in Sec. 4.4) is important for such security and privacy problems, we
remark that it should not be a surprise to cryptographers that the adversary
can play a strategy in a game to gain a non-negligible advantage, since
related assumptions about the adversary are standard in the long-established
school of computational security used to formally reason about cryptographic
primitives. We quote R.L. Rivest on the topic of games in cryptography
[MvOV96]:

> “Cryptography is also fascinating because of its game-like adversarial
> nature. A good cryptographer rapidly changes sides back and forth in his or
> her thinking, from attacker to defender and back. Just as in a game of
> chess, sequences of moves and countermoves must be considered until the
> current situation is understood.”

We argue that the above remark should also hold for the symbolic verification
of cryptographic protocols, which encompasses the methodology employed in this
work. In the setting of this work, the game is defined by a bisimilarity
problem specifying what it means for a protocol to satisfy unlinkability,
while attacks are strategies improving the chances of an attacker winning the
game. Such strategies can be conveniently described using modal logic
formulae.

The insight obtained, concerning the existence of unlinkability attacks on the
latest ePassport standards, is impactful for society, since ePassports and
electronic ID cards are used by the citizens of over 150 countries at the time
of writing. This amounts to an estimated 4 billion eDocuments in circulation
that implement the ICAO 9303 standard. The manufactures and operators of
readers should be made aware of mitigation strategies. Some preliminary ideas
on mitigation strategies are discussed in Sec. 6.1.

Further to uncovering the above mentioned attacks, this paper makes multiple
technical contributions. We proposed and justified a new scheme for
unlinkability problems in Sec. 4. We proposed a definition of open
bisimilarity for the applied $\pi$-calculus (Def. 3.1). Our formulations of
weak and strong early bisimilarity and similarity (Defs. 3, 4, and 4.4) for
the applied $\pi$-calculus are also new for the applied $\pi$-calculus,
incorporating minor improvements facilitating verification, such as the
adoption of a set of rules that make labelled transitions image finite. These
improvements are conventional from the perspective of established work on the
$\pi$-calculus; thus, in that direction, we simply modernise the applied
$\pi$-calculus with respect to advances in the $\pi$-calculus literature. The
formulation of the modal logic “classical $\mathcal{F}\\!\mathcal{M}$” is also
new, as is the rather short and neat proof (in Appendix B) of the fact that
classical $\mathcal{F}\\!\mathcal{M}$ characterises strong early bisimilarity
for the applied $\pi$-calculus (Theorem 8). The methodology of using a
classical $\mathcal{F}\\!\mathcal{M}$ formula to certify attacks is new, as is
the use of open bisimilarity to discover distinguishing strategies that are
transformed into attacks whenever the distinguishing strategy is not spurious.
A reformulation of unlinkability removing $\tau$-transitions has appeared in
related work [HBD19], but the proof that the new specification preserves the
original specification in terms of bisimilarity (Theorem 5) is new, as is the
observation that this transformation reduces the unlinkability problem to a
problem were image finiteness holds and strong notions of bisimilarity may be
applied. In short, in order to solve this problem, we have set up a rich tool
chain of methods that can be applied beyond the problem of analysing the
unlinkability of the ICAO 9303 standard.

#### Acknowledgements.

The formulation of the sequent calculus in Fig. 6 for calculating most general
recipes is new, but should be attributed to Alwen Tiu. He made the observation
that annotating deducibility constraints in a sequent calculus presentation
allows us to calculate the recipes required for an attacker to deduce a
message. We thank Davide Sangiorgi and the jury Luca Aceto, Jos Baeten,
Patricia Bouyer-Decitre, Holger Hermanns, and Alexandra Silva for the explicit
mention of the results communicated in this paper in the report on his CONCUR
2020 Test-of-Time Award [ABBD+20]. Last, but not least, we congratulate Jos
Baeten on the occasion of his retirement and dedicate this work to his
leadership in the field of concurrency.

## References

  * [ABBD+20] Luca Aceto, Jos Baeten, Patricia Bouyer-Decitre, Holger Hermanns, and Alexandra Silva.  CONCUR Test-Of-Time Award 2020 Announcement (Invited Paper).  In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1–5:3, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.  10.4230/LIPIcs.CONCUR.2020.5.
  * [ABF17] Martín Abadi, Bruno Blanchet, and Cédric Fournet.  The applied pi calculus: Mobile values, new names, and secure communication.  Journal of the ACM, 65(1):1:1–1:41, 2017.  10.1145/3127586.
  * [ABH+16] Gildas Avoine, Antonin Beaujeant, Julio Hernandez-Castro, Louis Demay, and Philippe Teuwen.  A survey of security and privacy issues in epassport protocols.  ACM Comput. Surv., 48(3):47:1–47:37, 2016.  10.1145/2825026.
  * [ABW06] Suzana Andova, Jos C. M. Baeten, and Tim A. C. Willemse.  A complete axiomatisation of branching bisimulation for probabilistic systems with an application in protocol verification.  In Christel Baier and Holger Hermanns, editors, CONCUR 2006 - Concurrency Theory, 17th International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006, Proceedings, volume 4137 of Lecture Notes in Computer Science, pages 327–342. Springer, 2006.  10.1007/11817949_22.
  * [ACRR10] Myrto Arapinis, Tom Chothia, Eike Ritter, and Mark Ryan.  Analysing unlinkability and anonymity using the applied pi calculus.  In 23rd IEEE Computer Security Foundations Symposium, pages 107–121, 2010.  10.1109/CSF.2010.15.
  * [AG99] Martin Abadi and Andrew D. Gordon.  A calculus for cryptographic protocols: The spi calculus.  Information and Computation, 148(1):1–70, 1999.  10.1006/inco.1998.2740.
  * [AHT17] Ki Yung Ahn, Ross Horne, and Alwen Tiu.  A characterisation of open bisimilarity using an intuitionistic modal logic.  In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 7:1–7:17, 2017.  10.4230/LIPIcs.CONCUR.2017.7.
  * [And21] Ross Anderson.  Security Engineering (third edition).  John Wiley & Sons, Inc., 2021.
  * [Bae21] David Baelde.  Contributions à la Vérification des Protocoles Cryptographiques.  habilitation thesis, Paris-Saclay, 2021.
  * [BB91] Jos C. M. Baeten and Jan A. Bergstra.  Real time process algebra.  Formal Aspects of Computing, 3(2):142–188, 1991.  10.1007/BF01898401.
  * [BB93] Jos C. M. Baeten and Jan A. Bergstra.  Non interleaving process algebra.  In Eike Best, editor, CONCUR’93, pages 308–323. Springer, 1993\.  10.1007/3-540-57208-2_22.
  * [BB98] Jos C. M. Baeten and Jan A. Bergstra.  Deadlock behaviour in split and ST bisimulation semantics.  In Ilaria Castellani and Catuscia Palamidessi, editors, Fifth International Workshop on Expressiveness in Concurrency, EXPRESS 1998, Satellite Workshop of CONCUR 1998, Nice, France, September 7, 1998, volume 16 of Electronic Notes in Theoretical Computer Science, pages 61–74. Elsevier, 1998.  10.1016/S1571-0661(04)00117-3.
  * [BBK87] Jos C. M. Baeten, Jan A. Bergstra, and Jan Willem Klop.  Ready-trace semantics for concrete process algebra with the priority operator.  Comput. J., 30(6):498–506, 1987.  10.1093/comjnl/30.6.498.
  * [BBMV91] Jos C. M. Baeten, Jan A. Bergstra, Sjouke Mauw, and Gert J. Veltink.  A process specification formalism based on static COLD.  In Jan A. Bergstra and Loe M. G. Feijs, editors, Algebraic Methods II: Theory, Tools and Applications, pages 303–335. Springer, 1991\.  10.5555/109462.109475.
  * [BFK09] Jens Bender, Marc Fischlin, and Dennis Kügler.  Security analysis of the PACE key-agreement protocol.  In Pierangela Samarati, Moti Yung, Fabio Martinelli, and Claudio A. Ardagna, editors, Information Security, pages 33–48. Springer, 2009.  10.1007/978-3-642-04474-8_3.
  * [BLMvT16] Jos C. M. Baeten, Bas Luttik, Tim Muller, and Paul van Tilburg.  Expressiveness modulo bisimilarity of regular expressions with parallel composition.  Mathematical Structures in Computer Science, 26(6):933–968, 2016\.  10.1017/S0960129514000309.
  * [BN07] Sébastien Briais and Uwe Nestmann.  Open bisimulation, revisited.  Theoretical Computer Science, 386(3):236–271, 2007.  j.tcs.2007.07.010.
  * [CDS20] Véronique Cortier, Stéphanie Delaune, and Vaishnavi Sundararajan.  A decidable class of security protocols for both reachability and equivalence properties.  Technical Report hal-02446170, Loria & Inria Grand Est; Irisa, 2020.  URL https://hal.inria.fr/hal-02446170/.
  * [CGIP12] Jean-Sébastien Coron, Aline Gouget, Thomas Icart, and Pascal Paillier.  Supplemental access control (PACE v2): Security analysis of PACE integrated mapping.  In David Naccache, editor, Cryptography and Security: From Theory to Applications - Essays Dedicated to Jean-Jacques Quisquater on the Occasion of His 65th Birthday, volume 6805 of Lecture Notes in Computer Science, pages 207–232. Springer, 2012.  10.1007/978-3-642-28368-0_15.
  * [CKR18] Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina.  DEEPSEC: Deciding equivalence properties in security protocols theory and practice.  In 2018 IEEE Symposium on Security and Privacy (S&P), pages 529–546, 2018.  10.1109/SP.2018.00033.
  * [CMdV06] Cas Cremers, Sjouke Mauw, and Erik P. de Vink.  Injective synchronisation: An extension of the authentication hierarchy.  Theoretical Computer Science, 367(1):139–161, 2006.  10.1016/j.tcs.2006.08.034.
  * [Cre08] Cas Cremers.  The Scyther tool: Verification, falsification, and analysis of security protocols.  In International Conference on Computer Aided Verification, pages 414–418. Springer, 2008.  10.1007/978-3-540-70545-1_38.
  * [CS10] Tom Chothia and Vitaliy Smirnov.  A traceability attack against e-passports.  In Radu Sion, editor, Financial Cryptography and Data Security, 14th International Conference, FC 2010, Tenerife, Canary Islands, Spain, January 25-28, 2010, Revised Selected Papers, volume 6052 of Lecture Notes in Computer Science, pages 20–34. Springer, 2010.  10.1007/978-3-642-14577-3_5.
  * [Del19] Uni researchers discover e-passport flaw.  Delano Magazine, Luxembourg, September 2019.  URL https://delano.lu/d/detail/news/uni-researchers-discover-e-passport-flaw/207929.
  * [DKR09] Stéphanie Delaune, Steve Kremer, and Mark Ryan.  Verifying privacy-type properties of electronic voting protocols.  Journal of Computer Security, 17(4):435–487, 2009.  10.3233/JCS-2009-0340.
  * [DvGHM08] Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan.  Characterising testing preorders for finite probabilistic processes.  Logical Methods in Computer Science, 4(4), 2008.  10.2168/LMCS-4(4:4)2008.
  * [FHMS19] Ihor Filimonov, Ross Horne, Sjouke Mauw, and Zach Smith.  Breaking unlinkability of the ICAO 9303 standard for e-passports using bisimilarity.  In Kazue Sako, Steve Schneider, and Peter Y. A. Ryan, editors, Computer Security – ESORICS 2019, pages 577–594. Springer, 2019.  10.1007/978-3-030-29959-0_28.
  * [Fil20] Ihor Filimonov.  Analysis of privacy attacks on ePassports and a mitigation strategy using TOTP.  master thesis, University of Luxembourg, 2020.
  * [HALT18] Ross Horne, Ki Yung Ahn, Shang-Wei Lin, and Alwen Tiu.  Quasi-open bisimilarity with mismatch is intuitionistic.  In Anuj Dawar and Erich Grädel, editors, In Proceedings of 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9-12, 2018, pages 26–35, 2018.  10.1145/3209108.3209125.
  * [HBD16] Lucca Hirschi, David Baelde, and Stéphanie Delaune.  A method for verifying privacy-type properties: the unbounded case.  In Security and Privacy (S&P), 2016 IEEE Symposium on, pages 564–581. IEEE, 2016.  10.1109/SP.2016.40.
  * [HBD19] Lucca Hirschi, David Baelde, and Stéphanie Delaune.  A method for unbounded verification of privacy-type properties.  Journal of Computer Security, 27(3):277–342, 2019.  10.3233/JCS-171070.
  * [HL95] Matthew Hennessy and Huimin Lin.  Symbolic bisimulations.  Theoretical Computer Science, 138(2):353–389, 1995.  10.1016/0304-3975(94)00172-F.
  * [Hor18] Ross Horne.  A bisimilarity congruence for the applied $\pi$-calculus sufficiently coarse to verify privacy properties.  CoRR, (arXiv:1811.02536), 2018.  URL https://arxiv.org/abs/1811.02536.
  * [Hüt03] Hans Hüttel.  Deciding framed bisimilarity.  Electronic Notes in Theoretical Computer Science, 68(6):1–18, 2003\.  10.1016/S1571-0661(04)80530-9.
  * [ISO18] Cards and security devices for personal identification — contactless proximity objects — part 3: Initialization and anticollision.  ISO/IEC 14443-3, 2018.  URL https://www.iso.org/standard/73598.html.
  * [Kri65] Saul A. Kripke.  Semantical analysis of intuitionistic logic I.  In J.N. Crossley and M.A.E. Dummett, editors, Formal Systems and Recursive Functions, volume 40 of Studies in Logic and the Foundations of Mathematics, pages 92–130. Elsevier, 1965.  https://doi.org/10.1016/S0049-237X(08)71685-9.
  * [Lab19a] Thierry Labro.  Une faille dans les passeports électroniques.  Paperjam, Luxembourg, September 2019.  URL https://paperjam.lu/article/faille-dans-passeports-electro.
  * [Lab19b] Thierry Labro.  Une faille qui devrait alerter les autorités.  Paperjam, Luxembourg, September 2019.  URL https://paperjam.lu/article/faille-qui-devrait-alerter-aut.
  * [LL12] Jia Liu and Huimin Lin.  A complete symbolic bisimulation for full applied pi calculus.  Theoretical Computer Science, 458:76–112, 2012.  https://doi.org/10.1016/j.tcs.2012.07.034.
  * [Low97] Gavin Lowe.  A hierarchy of authentication specifications.  In Proceedings 10th Computer Security Foundations Workshop, pages 31–43, June 1997.  10.1109/CSFW.1997.596782.
  * [MDBdV12] Jasen Markovski, Pedro R. D’Argenio, Jos C. M. Baeten, and Eric P. de Vink.  Reconciling real and stochastic time: the need for probabilistic refinement.  Formal Aspects of Computing, 24(4):497–518, 2012.  10.1007/s00165-012-0230-y.
  * [MPW93] Robin Milner, Joachim Parrow, and David Walker.  Modal logics for mobile processes.  Theor. Comput. Sci., 114(1):149–171, 1993.  10.1016/0304-3975(93)90156-N.
  * [MRT15] Machine readable travel documents. part 11: Security mechanisms for MRTDs.  International Civil Aviation Organization (ICAO), Doc 9303. Seventh Edition, 2015.  URL https://www.icao.int/publications/Documents/9303_p11_cons_en.pdf.
  * [MvOV96] Alfred Menezes, Paul C. van Oorschot, and Scott A. Vanstone.  Handbook of Applied Cryptography.  CRC Press, 1996.  10.1201/9781439821916.
  * [TD10] Alwen Tiu and Jeremy Dawson.  Automating open bisimulation checking for the spi calculus.  In 2010 23rd IEEE Computer Security Foundations Symposium, pages 307–321. IEEE, 2010.  10.1109/CSF.2010.28.
  * [TGD10] Alwen Tiu, Rajeev Gore, and Jeremy Dawson.  A Proof Theoretic Analysis of Intruder Theories.  Logical Methods in Computer Science, Volume 6, Issue 3, 2010\.  10.2168/LMCS-6(3:12)2010.
  * [Tiu07] Alwen Tiu.  A trace based bisimulation for the spi calculus: An extended abstract.  In Programming Languages and Systems. APLAS 2007, volume 4807 of Lecture Notes in Computer Science, pages 367–382. Springer, 2007.  10.1007/978-3-540-76637-7_25.
  * [TNH16] Alwen Tiu, Nam Nguyen, and Ross Horne.  SPEC: An equivalence checker for security protocols.  In Atsushi Igarashi, editor, Programming Languages and Systems. APLAS 2016, pages 87–95. Springer, 2016.  10.1007/978-3-319-47958-3_5.
  * [vDMR08] Ton van Deursen, Sjouke Mauw, and Sasa Radomirovic.  Untraceability of RFID protocols.  In Jose Antonio Onieva, Damien Sauveron, Serge Chaumette, Dieter Gollmann, and Constantinos Markantonakis, editors, Information Security Theory and Practices. Smart Devices, Convergence and Next Generation Networks, Second IFIP WG 11.2 International Workshop, WISTP 2008, Seville, Spain, May 13-16, 2008. Proceedings, volume 5019 of Lecture Notes in Computer Science, pages 1–15. Springer, 2008.  10.1007/978-3-540-79966-5_1.
  * [vG01] Rob van Glabbeek.  The linear time – branching time spectrum I.  In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 3 – 99. Elsevier Science, Amsterdam, 2001\.  https://doi.org/10.1016/B978-044482830-9/50019-9.
  * [vG21] Rob van Glabbeek.  Failure trace semantics for a process algebra with time-outs.  Logical Methods in Computer Science, 17(2):11:1–11:40, 2021.  10.23638/LMCS-17(2:11)2021.

##  Appendix A Reducing weak to strong bisimilarity

We provide here a proof for Lemma 2, which is used to prove that unlinkability
when expressed in terms of a strong bisimilarity problem, is equivalent to a
formulation of unlinkability in terms of weak bisimilarity (Theorem 5). In the
proof of the lemma below we employ equivariance, which simply allows names to
be swapped. Equivariance is the least congruence extending $\alpha$-conversion
such that $\nu x.\nu y.P\equiv\nu y.\nu x.P$, thereby allowing the order of
name binders to be ignored. Working up to equivariance has been shown to
significantly reduce the search space when constructing a bisimulation
[TNH16].

######  Lemma 14 (Lemma 2).

For any $P$ and $Q$ such that $c_{k}$ is fresh for $P$ and $Q$, we have

$\mathopen{\nu
c_{k}.}\left(\mathopen{!}c_{k}(\vec{k}).P\mathrel{\mid}\mathopen{!}\mathopen{\nu\vec{k}.}\mathopen{\mathopen{\overline{c_{k}}}\left<\vec{k}\right>}.Q\right)\approx\mathopen{!}\mathopen{\nu\vec{k}.}\left(P\mathrel{\mid}Q\right)$

######  Proof A.1.

Define $\mathcal{R}$ to be the least symmetric relation, upto equivariance,
such that for any $R_{i}$ and $S_{i}$ such that $c_{k}$ is fresh for $R_{i}$
and $S_{i}$ and $\vec{r}$ is fresh for $P$ and $Q$, we have that the following
extended process

$A\triangleq\begin{array}[t]{l}\mathopen{\nu
c_{k},\vec{k_{1}},\vec{k_{2}},\ldots\vec{k_{n}},\vec{r}.}\Big{(}~{}\sigma\mathrel{\mid}R_{1}\mathrel{\mid}\ldots
R_{n}\mathrel{\mid}!c_{k}(\vec{k}).P\mathrel{\mid}S_{1}\mathrel{\mid}\ldots
S_{n}\mathrel{\mid}{!\nu\vec{k}.\mathopen{\mathopen{\overline{c_{k}}}\left<\vec{k}\right>}.Q}~{}\Big{)}\end{array}$

is related by $\mathcal{R}$ to the following extended process

$B\triangleq\begin{array}[t]{l}\mathopen{\nu\vec{k}_{{f(1)}},\vec{k}_{{f(2)}},\ldots\vec{k}_{{f(m)}},\vec{r}.}\Big{(}~{}\sigma\mathrel{\mid}R_{f(1)}\mathrel{\mid}S_{f(1)}\mathrel{\mid}\ldots\mathrel{\mid}R_{f(m)}\mathrel{\mid}S_{f(m)}\mathrel{\mid}!\nu\vec{k}.\left(P\mathrel{\mid}Q\right)~{}\Big{)}\end{array}$

where $f\colon\left\\{1\ldots m\right\\}\rightarrow\left\\{1\ldots n\right\\}$
is injective and
$R_{i}=P\mathclose{\left\\{{}^{\vec{k_{i}}}\\!/\\!_{\vec{k}}\right\\}}$ and
$S_{i}=Q\mathclose{\left\\{{}^{\vec{k_{i}}}\\!/\\!_{\vec{k}}\right\\}}$ for
$i\in\left\\{1\ldots n\right\\}\setminus f(\left\\{1\ldots m\right\\})$.

There are two cases to pay attention to concerning extra $\tau$-transitions in
$B$. Firstly, consider

$A\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{12.0pt}{0.6pt}}\limits^{\tau}$}\mkern-7.0mu\blacktriangleright}\begin{array}[t]{l}\mathopen{\nu
c_{k},\vec{k_{1}},\vec{k_{2}},\ldots\vec{k_{n}},\vec{k_{n+1}},\vec{r}.}\Big{(}~{}\sigma\mathrel{\mid}\\\
\qquad R_{1}\mathrel{\mid}\ldots
R_{n}\mathrel{\mid}P\mathclose{\left\\{{}^{\vec{k_{n+1}}}\\!/\\!_{\vec{k}}\right\\}}\mathrel{\mid}!c_{k}(\vec{k}).P\mathrel{\mid}\\\
\qquad S_{1}\mathrel{\mid}\ldots
S_{n}\mathrel{\mid}{!\nu\vec{k}.\mathopen{\mathopen{\overline{c_{k}}}\left<\vec{k}\right>}.Q}~{}\Big{)}\end{array}$

This can be matched by $B$ by performing zero transitions, whilst staying in
the relation $\mathcal{R}$.

The second important case to consider is when for some $j\in\left\\{1\ldots
n\right\\}\setminus f(\left\\{1\ldots m\right\\})$ we have
$P\mathclose{\left\\{{}^{\vec{k_{j}}}\\!/\\!_{\vec{k}}\right\\}}$ or
$Q\mathclose{\left\\{{}^{\vec{k_{j}}}\\!/\\!_{\vec{k}}\right\\}}$ acts (or
indeed they interact), possibly extruding some active substitution $\sigma$
and fresh names $\vec{s}$, as follows.

$\\!\\!\\!\\!\begin{array}[t]{l}\begin{array}[t]{l}\mathopen{\nu
c_{k},\vec{k_{1}},\vec{k_{2}},\ldots\vec{k_{n}},\vec{r}.}\Big{(}~{}\sigma\mathrel{\mid}\\\
\qquad R_{1}\mathrel{\mid}\ldots
P\mathclose{\left\\{{}^{\vec{k_{j}}}\\!/\\!_{\vec{k}}\right\\}}\ldots\mathrel{\mid}R_{n}\mathrel{\mid}!c_{k}(\vec{k}).P\mathrel{\mid}\\\
\qquad S_{1}\mathrel{\mid}\ldots
Q\mathclose{\left\\{{}^{\vec{k_{j}}}\\!/\\!_{\vec{k}}\right\\}}\ldots\mathrel{\mid}S_{n}\mathrel{\mid}{!\nu\vec{k}.\mathopen{\mathopen{\overline{c_{k}}}\left<\vec{k}\right>}.Q}~{}\Big{)}\end{array}\\\
\quad\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{12.0pt}{0.6pt}}\limits^{\pi}$}\mkern-7.0mu\blacktriangleright}\begin{array}[t]{l}\mathopen{\nu
c_{k},\vec{k_{1}},\vec{k_{2}},\ldots\vec{k_{n}},\vec{r},\vec{s}.}\Big{(}~{}\sigma\mathrel{\mid}\theta\mathrel{\mid}\\\
\qquad R^{\prime}_{1}\mathrel{\mid}\ldots
R^{\prime}_{j}\ldots\mathrel{\mid}R^{\prime}_{n}\mathrel{\mid}!c_{k}(\vec{k}).P\mathrel{\mid}\\\
\qquad S^{\prime}_{1}\mathrel{\mid}\ldots
Q^{\prime}_{j}\ldots\mathrel{\mid}S^{\prime}_{n}\mathrel{\mid}{!\nu\vec{k}.\mathopen{\mathopen{\overline{c_{k}}}\left<\vec{k}\right>}.Q}~{}\Big{)}\end{array}\end{array}$

In this case, $B$ stays within relation $\mathcal{R}$ by using transition

$\begin{array}[]{l}B\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{12.0pt}{0.6pt}}\limits^{\pi}$}\mkern-7.0mu\blacktriangleright}\begin{array}[t]{l}\mathopen{\nu\vec{k}_{f(1)},\vec{k}_{f(2)},\ldots\vec{k}_{f(m)},\vec{k}_{f(m+1)},\vec{r},\vec{s}.}\Big{(}~{}\sigma\mathrel{\mid}\theta\mathrel{\mid}\\\
\qquad\qquad
R^{\prime}_{g(1)}\mathrel{\mid}S^{\prime}_{g(1)}\mathrel{\mid}\ldots\mathrel{\mid}R^{\prime}_{g(m)}\mathrel{\mid}S^{\prime}_{g(m)}\mathrel{\mid}R^{\prime}_{g(m+1)}\mathrel{\mid}S^{\prime}_{g(m+1)}\mathrel{\mid}!\nu\vec{k}.\left(P\mathrel{\mid}Q\right)~{}\Big{)}\end{array}\end{array}$

where $g\colon\left\\{1\ldots m+1\right\\}\rightarrow\left\\{1\ldots
n\right\\}$ such that $g(i)=\left\\{\begin{array}[]{lr}j&\mbox{if}~{}i=m+1\\\
f(i)&\mbox{otherwise}\end{array}\right.$, which is clearly injective. Note we
should also consider when two distinct $j,j^{\prime}\in\left\\{1\ldots
n\right\\}\setminus f(\left\\{1\ldots m\right\\})$ interact in $A$, which has
a similar pattern, except we require pairs of processes to be added to $B$
using the rule Rep-close.

##  Appendix B Classical $\mathcal{F}\\!\mathcal{M}$ characterises strong
early bisimilarity

In this paper, we prove that unlinkability properties are violated by
exhibiting a distinguishing formula in classical $\mathcal{F}\\!\mathcal{M}$.
A distinguishing formula is sufficient evidence to show that two processes
specifying the unlinkability property are not bisimilar, as long as the modal
logic characterises bisimilarity. Therefore the proof of soundness and
completeness of strong early bisimilarity with respect to classical
$\mathcal{F}\\!\mathcal{M}$ is critical for this work. Indeed, other parts of
our reasoning may be incomplete, e.g., using open bisimilarity to seek a
distinguishing strategy, but if our method discovers an attack that can be
described using an $\mathcal{F}\\!\mathcal{M}$ formula that we confirm is
distinguishing, then we are certain that unlinkability does not hold as
formulated.

We reiterate Theorem 8. The proof is standard for a classical Milner-Parrow-
Walker logic, for which reason it appears in this appendix. In fact, the use
of static equivalence simplifies the analysis compared to the $\pi$-calculus,
since there are no special cases for bound actions.

######  Theorem 15 (Theorem 8).

$P\sim Q$, whenever, for all $\phi$, we have $P\models\phi$ if and only if
$Q\models\phi$.

######  Proof B.1.

Let
$\mathcal{R}=\left\\{(A,B)\colon\forall\phi,A\models\phi\,\mbox{iff}\,B\models\phi\right\\}$.
We aim to prove $\mathcal{R}$ is a strong early bisimulation. Symmetry is
immediate. In the following cases assume $A\mathrel{\mathcal{R}}B$.

Case of static equivalence. By definition of $\mathcal{R}$ for any $M$ and
$N$, we can apply $\alpha$-conversion to $A$ and $B$ such that
$A=\nu\vec{x}.(\theta\mathrel{\mid}P)$ and
$B=\nu\vec{y}.(\sigma\mathrel{\mid}Q)$ and
$\left(\vec{x}\cup\vec{y}\right)\cap\left(\mathopen{\mathrm{fv}}\left(M\right)\cup\mathopen{\mathrm{fv}}\left(N\right)\right)=\emptyset$.
If $M\theta=N\theta$, then by definition of satisfaction, $A\models M=N$
hence, by definition of $\mathcal{R}$, $B\models M=N$, hence by definition of
satisfaction, $M\sigma=N\sigma$. Therefore $A$ and $B$ are statically
equivalent.

Case of actions. Suppose $A\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{12.0pt}{0.6pt}}\limits^{\pi}$}\mkern-7.0mu\blacktriangleright}A^{\prime}$.
Hence $A\models\mathopen{\big{\langle}\pi\big{\rangle}}\mathtt{tt}$, so by
definition of $\mathcal{R}$, we have
$B\models\mathopen{\big{\langle}\pi\big{\rangle}}\mathtt{tt}$ and hence for
some $B^{\prime}$ we have $B\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{12.0pt}{0.6pt}}\limits^{\pi}$}\mkern-7.0mu\blacktriangleright}B^{\prime}$.
By image-finiteness, there are finitely many $B_{i}$ such that
$B\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{12.0pt}{0.6pt}}\limits^{\pi}$}\mkern-7.0mu\blacktriangleright}B_{i}$.
Suppose for contradiction that $A^{\prime}\mathrel{\mathcal{R}}B_{i}$ does not
hold for all $i$. Then for all $i$, there exists $\phi_{i}$ such that
$A^{\prime}\models\phi_{i}$ and $B_{i}\not\models\phi_{i}$. Hence
$A\models\mathopen{\big{\langle}\pi\big{\rangle}}\left(\bigwedge_{i}\phi_{i}\right)$
but
$B\not\models\mathopen{\big{\langle}\pi\big{\rangle}}\left(\bigwedge_{i}\phi_{i}\right)$,
contradicting the assumption that $A\mathrel{\mathcal{R}}B$. Hence for some
$i$, $A^{\prime}\mathrel{\mathcal{R}}B_{i}$, as required.

Thus, $\mathcal{R}$ is a strong early bisimulation. Hence, if for any
processes $P$ and $Q$ it holds that, for all formula $\phi$, we have
$P\models\phi$ if and only if $Q\models\phi$, then we have
$P\mathrel{\mathcal{R}}Q$, and hence $P\sim Q$.

The converse direction follows by induction on the structure of $\phi$. Assume
$P\sim Q$, hence there is some strong early bisimulation $\mathcal{S}$ such
that $P\mathrel{\mathcal{S}}Q$. In the following, assume that
$A\mathrel{\mathcal{S}}B$ holds.

Case of equality. Consider when $A\models M=N$. By $\alpha$-conversion,
$A=\nu\vec{x}.(\theta\mathrel{\mid}P)$ such that
$\vec{x}\cap\left(\mathopen{\mathrm{fv}}\left(M\right)\cup\mathopen{\mathrm{fv}}\left(N\right)\right)=\emptyset$.
hence $M\theta=N\theta$. Now, by $\alpha$-conversion we have
$B=\nu\vec{y}.(\sigma\mathrel{\mid}Q)$ such that
$\vec{y}\cap\left(\mathopen{\mathrm{fv}}\left(M\right)\cup\mathopen{\mathrm{fv}}\left(N\right)\right)=\emptyset$.
So, by static equivalence, $M\sigma=N\sigma$; and hence $A\models M=N$, as
required.

Case of conjunction. Consider when $A\models\phi\wedge\psi$ hence
$A\models\phi$ and $A\models\psi$. So, by the induction hypothesis
$B\models\phi$ and $B\models\psi$ and hence $B\models\phi\wedge\psi$.

Case of negation. Consider when $A\models\neg\phi$, hence $A\not\models\phi$.
Hence, by the induction hypothesis, $B\not\models\phi$ hence
$B\models\neg\phi$.

Case of action. Consider when
$A\models\mathopen{\big{\langle}\pi\big{\rangle}}\phi$. Hence
$A\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{12.0pt}{0.6pt}}\limits^{\pi}$}\mkern-7.0mu\blacktriangleright}A^{\prime}$
such that $A^{\prime}\models\phi$. Since $\mathcal{S}$ is a strong early
bisimulation, there exists $B^{\prime}$ such that $B\mathrel{\raise
2.2pt\hbox{$\mathop{\rule{12.0pt}{0.6pt}}\limits^{\pi}$}\mkern-7.0mu\blacktriangleright}B^{\prime}$
and $A^{\prime}\mathrel{\mathcal{S}}B^{\prime}$. Hence, by the induction
hypothesis, $B^{\prime}\models\phi$. Hence
$B\models\mathopen{\big{\langle}\pi\big{\rangle}}\phi$.

Hence, by induction on the structure of $\phi$, for all formulae $\phi$, and
for all $A$, $B$ such that $A\mathrel{\mathcal{S}}B$, we have $A\models\phi$
iff $B\models\phi$; and hence $P\models\phi$ iff $Q\models\phi$, since
$P\mathrel{\mathcal{S}}Q$.