# Modelling and Analysis of a Hierarchy of Distance Bounding Attacks
Tom Chothia
University of Birmingham
Birmingham, UK, Joeri de Ruiter
Radboud University
Nijmegen, The Netherlands, Ben Smyth
University of Luxembourg,
Luxembourg
## Abstract
We present an extension of the applied pi-calculus that can be used to model distance bounding protocols. A range of different security properties have been suggested for distance bounding protocols; we show how these can be encoded in our model and prove a partial order between them. We also relate the different security properties to particular attacker models. In doing so, we identify a new property, which we call *uncompromised distance bounding*, that captures the attacker model for protecting devices such as contactless payment cards or car entry systems, which assumes that the prover being tested has not been compromised, though other provers may have been. We show how to compile our new calculus into the applied pi-calculus so that protocols can be automatically checked with the ProVerif tool and we use this to analyse distance bounding protocols from MasterCard and NXP.
# Introduction
Contactless payment cards and “keyless” car entry systems aim to make life easier. However, they also make it possible to wirelessly-pickpocket a victim (Chothia et al. 2015) or even steal their car (Francillon, Danev, and Capkun 2011). Such exploits are not merely theoretical; criminal gangs are using such attacks to steal cars (BBC, n.d.). Thieves relay signals from a victim’s key fob (located inside the victim’s house) to the victim’s car (parked outside), which enables the thieves to unlock the car, start the engine, and drive away.
Distance bounding protocols (Brands and Chaum 1994) use round trip times to establish an upper-bound on the distance between a “prover”, e.g., a contactless payment card or key fob, and a “verifier”, e.g., a payment machine or car. This can be used to enforce that a prover is co-located with a verifier. Hence, they can be used to prevent the aforementioned attacks. Round trip times are sometimes bounded by the speed of light (Brands and Chaum 1994) and sometimes by the lag introduced by relaying equipment (EMVCo 2016).
A distance bounding attack occurs when a verifier is deceived into believing they are co-located with a prover, when they are not. Attackers may relay, replay and alter messages, as well as trying to predict or preempt timed challenges. Some distance bounding protocols also aim to defend against a “dishonest prover” attacker , i.e., an attacker that knows all of the secret values of a normal prover, but will misuse them to try to trick a verifier. Other attacker models consider a weaker “terrorist prover,” i.e., a dishonest prover that will not reveal its long term keys. The literature on symbolic verification of distance bounding protocols includes five different types of attacks, each of which uses some combination of basic, unprivileged attackers, dishonest prover attackers, and terrorist fraud attackers. We describe these in detail in the next section.
In this paper, we extend the applied pi-calculus (Abadi and Fournet 2001) to distinguish between co-located processes and processes at distinct locations, and we restrict communication between locations using timers. In particular, when a location’s timer is active, processes at that location may only receive input from co-located processes (they cannot receive input from a remote process, i.e., a process at a different location). Our extended calculus allows us to model distance bounding protocols. Indeed, we can consider an attacker, some provers and a verifier in various locations. Moreover, timers capture bounded round trip times, in particular, a verifier cannot receive any input from a remote attacker whilst a timer is active at the verifier’s location. Thus, the calculus allows us to check for and detect each of the different types of attack against distance bounding protocols. Furthermore, we define a compiler that encodes the calculus into the standard applied pi-calculus, which enables automated analysis using tools such as ProVerif (Blanchet et al. 2018).
Industrial distance bounding protocols such as Mastercard’s RRP protocol (EMVCo 2016) and NXP’s “proximity check” (De et al. 2011; Janssens 2017) aim to protect payments and access tokens from relay attacks. These protocols need not defend against attacks requiring dishonest provers, because if an attacker gets access to the secret keys, they can clone the cards or key fobs, and make payments or gain access without a need to relay the original device, i.e., protection is only needed for an uncompromised device.
However, we expect some devices (e.g., EMV cards or car fobs) may be compromised at some point, and we would like to ensure that the compromise of a particular prover would not lead to an attacker being able to successfully attack other provers. None of the commonly considered distance bounding security properties (which are presented in the next section) match this attacker model.
Using our calculus, we are able to consider all possible combinations of verifiers, provers and dishonest provers and so enumerate all possible distance bounding attack scenarios. Defending against each of these attack scenarios gives us a security property, and under reasonable assumptions (which we detail in Section 5) we can equate many of these distance bounding attack scenarios and impose a partial order on the others so creating a hierarchy of distance bounding attacks. Different parts of this hierarchy relate to different attacker models, and each attacker model is dominated by a single security property (this ordering is presented in Figure [fig:order] on page ). Our ordering shows that, under reasonable assumptions, “assisted distance fraud” attacks (Cremers et al. 2012) are more powerful than all other properties. Moreover, it shows that when an attacker can only act remotely, protection against “distance hijacking” attacks (Cremers et al. 2012) is the most powerful property needed. Details of these attacks are given in the next section.
From our hierarchy of distance bounding protocols we identify a new distance bounding attack scenario and security property, which we call *uncompromised distance bounding* security. In an uncompromised distance bounding attack the provers being targeted are remote from the verifier and the attacker acts at both the location of the prover and the verifier. Additionally, the attacker may have compromised a number of other provers at both locations, and use these in the attack. An uncompromised distance bounding attack exists if the attacker can cause the verifier to believe that one of the uncompromised, remote targeted provers is in fact local to the verifier. Defending against this kind of attack is the strongest security property needed for protocols such as MasterCard’s RRP to protect contactless payment cards or NXP’s proximity check when being used to protect, e.g., access to buildings.
We demonstrate the applicability of our results by analysing MasterCard’s RRP protocol for distance bounding of contactless EMV (EMVCo 2016), and a distance bounding protocol from NXP (De et al. 2011; Janssens 2017). These protocols have not been studied before. In these protocols the prover will send information about how long replies are expected to take and the verifier will use this information to set the time limits used in the distance bounding protocol. If attackers can alter these time limits then they can succeed in a relay attack by telling the verifier to wait long enough to relay the messages. As our calculus is based on the applied pi-calculus we are also able to check that the protocols ensure the authenticity of the timing information to confirm that attacks on it are not possible.
**Contributions:** Our contributions are as follows:
- An extension of the applied pi-calculus with locations and timer actions (Section 3).
- Formalizations of security properties for distance bounding protocols (Section 4).
- A hierarchy of our security properties, relations to particular attacker models, and identification of a new security property (Section 5).
- A practical, automatic tool for the analysis of distance bounding protocols, based on compiling our calculus into the applied pi-calculus (Section 6).
- Formal analysis of distance bounding protocols, including from MasterCard and NXP (Section 7).
Our models, compiler and full paper (with proofs) are on our project website
**Related work:** Some prior work on the verification of distance bounding protocols has used manual reasoning, e.g., (Meadows et al. 2007; Schaller et al. 2009) in the symbolic model, (Gildas Avoine et al. 2011; Boureanu, Mitrokotsa, and Vaudenay 2015; Boureanu and Vaudenay 2015; Dürholz et al. 2011) in the computational model and (Cremers et al. 2012; Schaller et al. 2009) using theorem provers.
Some previous work on automatic analysis of distance bounding protocols has been based on the applied pi-calculus: Malladi et al. (Malladi, Bruhadeshwar, and Kothapalli 2010) analyse single runs, Chothia et al. (Chothia et al. 2015) analyse an arbitrary number of runs for relay attacks, and Debant et al. (Debant, Delaune, and Wiedling 2018) provide a model with a formal correctness proof, which uses a definition of relay attack that is close to our definition of uncompromised distance bounding.
Nigam et al. (Nigam, Talcott, and Urquiza 2016) introduce an extension to strand spaces to model security protocols that include time and Kanovich et al. (Kanovich et al. 2014) consider a multiset rewriting model and compare discrete and continuous time. A contribution of our paper is to show that you do not need to explicitly consider the time of actions to meaningfully analyse distance bounding protocols. Mauw et al. (Sjouke Mauw et al. 2018) improves on the framework of (Schaller et al. 2009) looking at causality between actions to make a framework for automatically testing distance fraud and terrorist fraud.
None of the previous papers on symbolic checking of distance bounding protocols consider the full range of distance bounding properties or makes comparisons between them.
A recent survey (G. Avoine et al. 2017) gives many examples of distance bounding protocols and attacks. Two notable protocols missing from this survey are MasterCard’s RRP protocol for contactless EMV cards and NXP’s “proximity check”, which we both consider in this paper. MasterCard’s RRP is a variant of the PaySafe protocol, which we have previously proposed for contactless EMV (Chothia et al. 2015).
Past papers (Debant, Delaune, and Wiedling 2018; Sjouke Mauw et al. 2018; Nigam, Talcott, and Urquiza 2016) have reported an attack against PayWave when the prover is dishonest. However, as we discuss in Section 5, if an EMV card has been compromised, then there is no need to relay it, hence such “distance fraud attacks” are not the correct attacker model for contactless EMV. In contrast, we relate distance bounding security properties to particular attacker models.
# Distance bounding protocols and attacks
Distance bounding protocols aim to let a verifier place an upper-bound on the distance to a prover by timing how long it takes for certain challenges to be answered. Cryptography is used to ensure that the responder had to know the challenge before replying. Often the time taking to perform complex cryptography will vary between runs, therefore it is difficult to time cryptographic actions, and the challenge-response mechanism is typically limited to a simple exchange of nonces, with the cryptography performed before or afterwards.
**Example 1**. *As a running example we consider the following distance bounding protocol, in which the verifier and all provers share the same symmetric key.*
**\[msc diagram omitted\]**
*The verifier receives the identifier of the prover, generates nonces $chal$ and $resp$, and sends the encrypted nonces to the prover. Once the prover indicates that it has decrypted the nonces, the verifier activates a timer, and sends nonce $chal$ to the prover. The prover waits for nonce $chal$ before revealing nonce $resp$, hence, the nonce is only revealed once the verifier’s timer is running.*
This protocol is not vulnerable to relay fraud because only the prover can decrypt the challenge and response, and an honest prover will not release the response until it receives the challenge, i.e., the attacker cannot learn the response until the timer has started, and then, if the prover is remote from the verifier, it will be impossible to get this response to the prover without the timer expiring.
Our example protocol does *not* defend against a dishonest prover that tries to trick the verifier, i.e., a prover can convince the verifier that it is nearer than it really is. Such a dishonest prover could be a hardware device that has been compromised by an attacker, or the owner of a device trying to mislead the verifier. Indeed, the prover can send the response early, before receiving the challenge, so the verifier receives the response just after it transmits the challenge. This will lead to a short delay between the challenge and response, making the verifier incorrectly believe that the prover is nearby.
The right security property for a distance bounding protocol, will depend on the use case. Common security properties considered in the literature on symbolical of checking distance bounding protocols include:
- Relay/Mafia Fraud (Desmedt, Goutier, and Bengio 1987): The verifier and the prover are remote from each other. Attackers act at the same location as both the verifier and prover, and may relay, alter or replay messages, to trick the prover into believing that the prover is in fact local.
- Distance Fraud (Desmedt 1988)/Lone Distance Fraud (Cremers et al. 2012): A dishonest prover, which may deviate from the protocol, is at a location remote from the verifier. This dishonest prover misleads the verifier into believing that it is local.
- Distance Hijacking (Cremers et al. 2012): A dishonest prover remotely authenticates to a verifier, as in Distance Fraud, but there are also other honest provers at the same location as the verifier, which the dishonest prover may make use of.
- Terrorist Fraud (Desmedt 1988): A terrorist fraud attack involves one attacker acting locally to the verifier along with a remote dishonest prover, with the goal of making the verifier believe that the remote dishonest prover is in fact local. This kind of attack always assumes that the prover has a secret key that identifies it and that the prover does not send this key to any process which is local to the verifier.
- Assisted Distance Fraud (Cremers et al. 2012): A terrorist prover remotely authenticates to a verifier, assuming the cooperation of another dishonest prover that is co-located with the verifier.
We can stop our example protocol being vulnerable to distance fraud attacks by adding a new nonce that is sent with the challenge, and also needs to be included with the response. However, such a protocol would still be vulnerable to terrorist fraud attacks, because a remote dishonest terrorist fraud prover could decrypt the challenge and response and send them to an accomplice attacker that is local to the verifier, which can then use them to answer the verifier’s challenge within the time limit.
This terrorist fraud attack can be stopped by, for instance, requiring the prover to hash the response with their secret key. Thereby providing evidence to the verifier that some local party did indeed know the secret key. However, if the same key is used by multiple provers then the protocol is vulnerable to distance hijacking and assisted distance fraud, because the dishonest prover could send the challenge and response to some honest prover that is co-located with the verifier. This honest prover would answer the verifiers challenge, which the verifier believed was the dishonest prover.
To protect against these attacks, we could require every prover to use a unique key with the verifier, thereby making it impossible for the dishonest prover to encrypt a message for some other honest prover.
**Example 2**. *Making the additions described above to the protocol from Example 1 we get a protocol that is secure against all the attacks listed above:*
**\[msc diagram omitted\]**
*This protocol uses a lightweight hash function, which needs to be computed before the timer expires.*
# Timer location calculus: A language for modelling distance bounding protocols
The timer location calculus syntax
Our *timer location calculus* extends the applied pi-calculus (Abadi, Blanchet, and Fournet 2017; Abadi and Fournet 2001; Blanchet, Abadi, and Fournet 2008; Ryan and Smyth 2011) with timers and locations. We first present the calculus syntax, illustrating this using the protocol from Example 1. We then present the semantics and explain how this captures the behaviour of timed communications.
**Syntax:** Each protocol role is written as a process, using the syntax of our language (Figure 1). Communication between roles is modelled by the *input* and *output* commands. The semantics, presented below, will substitute the term sent by an output command for the variable named in an enabled input. We assume that the attacker controls the network, so processes are not able to ensure that a particular output goes to a particular input.
*Parallel composition* ($P \mid Q$) represents two processes running concurrently, and process *replication* ($!P$) represents an arbitrary number of copies of a process running in parallel. The *new* command creates a new value that then represents, for instance, a nonce, a key or a process identity. This value will not be known to the attacker unless it is output on a public channel.
**Example 3**. *The following process models an arbitrary number of provers with different ids each running an arbitrary number of times*
*$$\begin{array}{lcl}
\mathit{ExProvers(id)} &\!\!\!\!=\!\!\!\!& !new\ id.!PRole(id)\\
%\\
%System2 &=& \new{k_C}. [!\new finished.Reader2] \\
%&&\mid [!Card2 \mid !\new n.Reader2\{n/finished\}]
\end{array}$$*
*We define $PRole(id)$ in the next example to model a single run of the protocol with identity “id”, so $!PRole(id)$ represents an arbitrary number of runs of the protocol with a particular id. The “$!new\ id$” term at the front of the process generates an arbitrary number of new process ids.*
Cryptography is modelled using constructors and destructors, e.g., symmetric key encryption can be modelled using a binary constructor $enc(m,k)$ to represent the message $m$ encrypted with the key $k$ and a binary destructor function $dec$ with the rewrite rule $dec(enc(m,k),k) = m$. Functions can be public, i.e., available for use by the attacker, or private meaning that they cay only be used by processes specified as party of the protocol. Private functions are useful, for instance, to look up private keys which should only be known to protocol participants.
Functions are applied using the let statement, e.g., “$\textnormal{let } pt=dec(ct,k) \textnormal{ in } P \textnormal{ else }Q$" tries to decrypt cipher text $ct$ with key $k$, and acts as $P$ if decryption succeeds and $Q$ otherwise. Term evaluation in the let statement can also be used to define projections on tuples, and equality checks on names. As syntactic sugar we write “$in(=\!\!a).P$", for a process that receives an input and then acts as the process $P$ if that input value is equal to $a$. We refer the reader to (Abadi and Fournet 2001) for more details on functions in the applied pi-calculus.
**Example 4**. *A single run of the prover role of the protocol informally described in Example 1, with identity $id$, can be modelled as the process: $$\begin{array}{lcl}
\mathit{PRole(id)} &\!\!\!\!=\!\!\!\!& out(id)\mathrel.in(x)\mathrel.\\
&& \textnormal{let } (chal,resp)=dec(x,k) \textnormal{ in }\\
&& out(ready)\mathrel.in(=\!\!chal)\mathrel.out(resp) \\
%\\
%System2 &=& \new{k_C}. [!\new finished.Reader2] \\
%&&\mid [!Card2 \mid !\new n.Reader2\{n/finished\}]
\end{array}$$*
Events are used to annotate the protocol for automated checking. For instance, below we will add an event to the protocol to signal that the verifier believes it has correctly verified a particular prover. The syntax presented so far is from the applied pi-calculus. Next, we present our additions, namely, locations and timers.
The process $startTimer.P$ represents starting a timed challenge and $stopTimer.P$ represents ending a challenge. We require that every start timer action is matched by exactly one stop timer action along all possible paths, and replication and parallel composition are forbidden between start and stop timer actions.
**Example 5**. *The verifier role of the protocol informally described in Example 1 can be modelled as the process: $$\begin{array}{lcl}
\mathit{ExVerifiers} &= &!in(id)\mathrel.new\ chal\mathrel.new\ resp.\\
&&out(enc((chal,resp),k))\mathrel.in(ready).\\
&& startTimer\mathrel. out(chal)\mathrel.in(=\!\!resp)\mathrel.\\
&& stopTimer\mathrel. \textnormal{event}(\textnormal{verify}(id))
\end{array}$$*
Locations are written $\left[ \mathcal{P} \right]_{r}$, where $\mathcal{P}$ are (co-located) processes and $r$ denotes the number of active timers. We abbreviate $\left[ \{P_1,\dots,P_n\} \right]_{r}$ as $[P_1,\dots,P_n]_{r}$ and $\left[ \{P_1,\dots,P_n\} \right]_{0}$ as $[P_1,\dots,P_n]$. Our model assumes that processes are either co-located or at distinct locations, and we abstract away from precise distances between provers and verifiers when modelling. We assume that there is a known maximum round trip time for communication between “local” processes, i.e., co-located processes, and the timer enforces this. Hence, it will not be possible for a message to travel to processes at different locations, and back again before the timer expires.
*represents our example provers and verifiers running at the same location, i.e., it is possible for the prover to answer the challenge within the time limit and be verified. The declaration of the key $k$ as new means that this is a new unique value, known only in the $\mathit{ExProvers}$ and $\mathit{ExVerifiers}$ processes.*
*By comparison, the system*
*represents the verifiers and provers at different locations. Hence, in the latter system, it should not be possible for the prover to answer the timed challenge within the time limit, therefore a correct distance bounding protocol will not allow the prover to be verified.*
**Semantics:** Dynamic behaviour of processes (which model protocols) can be examined using the semantics of our language (Figure [fig:semantics]), which is defined over *system configurations*, denoted $E,\mathcal L$, where that $E$ is a set of free names and $\mathcal L$ is a finite multiset of systems.
The set $E$ keeps track of the names that have been assigned so far, making it possible for the new command to pick fresh previously unused names, this is done by the $\mbox{\sc (New)}$ rule. The $\mbox{\sc (Repl)}$ rule creates a copy of a replicated process, the $\mbox{\sc (Let 1)}$ rule can be used to apply functions, e.g., for decryption, and the $\mbox{\sc (Let 2)}$ rule selects the else branch when no function reductions are possible (this, for instance, allows us to define equality tests). These rules are a direct extension of existing applied pi-calculus rules (e.g., (Abadi, Blanchet, and Fournet 2017; Ryan and Smyth 2011)) with our syntax for locations.
The rules we have created for our modelling language define the behaviour for timers and for communication between locations. The $\mbox{\sc (Start)}$ rule increments the number of timers running at a location, and the $\mbox{\sc (Stop)}$ rule reduces the number of running timers. The restriction placed upon processes ensures that the number of running timers never becomes negative. Rule $\mbox{\sc (I/O Local)}$ defines local communication, which allows messages to be exchanged between co-located processes, regardless of whether timers are running.
**Example 7** (Local communication). *As an example we consider a verifier that sends a challenge, denoted `a`, to a prover, to which the prover replies with a function `f` applied to this and some other value `b`:*
**\[msc diagram omitted\]**
*We can write these roles as processes: $$\begin{aligned}
P_V &= startTimer.out(a).in(x).stopTimer.P'_V\\
P_P &= in(x).out(f(x,b)).P'_P
\end{aligned}$$ such that processes $P'_V$ and $P'_P$ do not contain variable $x$ (hence, we need not consider substitutes for $x$ in these processes). Moreover, consider system configuration $\mathcal C_1 = E, \left\{ \left[ P_V, P_P \right]_{0} \right\}$ that co-locates those processes. Hence, we can observe traces in which the timed challenge succeeds. Indeed, $\mathcal C_1$ reduces by rule $\mbox{\sc (Start)}$ two applications of rule $\mbox{\sc (I/O Local)}$ rule, and rule $\mbox{\sc (Stop)}$: $$\begin{aligned}
\mathcal C_1
\rightarrow &E, \left\{ \left[ out(a).in(x).stopTimer.P'_V, P_P \right]_{1} \right\}\\
\rightarrow &E, \left\{ \left[ in(x).stopTimer.P'_V, out(f(a,b)).P'_P %\{a/x\}
\right]_{1} \right\}\\
\rightarrow &E, \left\{ \left[ stopTimer.P'_V%\{f(a,b)/x\}
, P'_P %\{a/x\}
\right]_{1} \right\}\\
\rightarrow &E, \left\{ \left[ P'_V%\{f(a,b)/x\}
, P'_P %\{a/x\}
\right]_{0} \right\}
\end{aligned}$$ By comparison, the processes cannot complete the challenge from distinct locations. Indeed, although $$\begin{gathered}
E, \left\{ \left[ P_V\right]_{0}, \left[ P_P\right]_{0}\right\} \rightarrow^* \\
E, \left\{ \left[ in(x).stopTimer.P'_V, \right]_{1},\left[ out(f(a,b)).P'_P %\{a/x\}
\ \right]_{0} \right\},
\end{gathered}$$ the semantics do not allow any further reduction.*
Rule $\mbox{\sc (Global)}$ allows an output to arrive at a new location, if no timers are active at that location. In implemented systems, it is only possible to receive outputs at particular times, yet rule $\mbox{\sc (Global)}$ allows outputs to be received at any time (in particular, after other processes have reduced). In this sense, the rule might be considered an over-approximation. However, for any communication allowed by our semantics, there exists a corresponding system execution (that takes communication and processing times into account). Thus, the rule accurately captures system behaviour, in particular, all possible interactions with an attacker are considered.
**Example 8** (Preemption). *A remote process may communicate with a timed process by preempting the messages needed. For instance, consider configuration $\mathcal C_3 = E, \left\{ \left[ P_V\right]_{0}, \left[ in(x).P'_P,out(f(p,b))\right]_{0}\right\}$ and reduction $$\begin{aligned}
%\mathcal C_3\\
%\rightarrow & \Ecal, \left\{ \ltag{ \{P_V\}}{0}, \ltag{ \{\In{x}.P'_P,\Out{f(p,b)}\}}{0}\right\}\ben{I can't see any reduction?}\\
&\mathcal C_3 \rightarrow\phantom{^*} E, \left\{ \left[ P_V,out(f(p,b))\right]_{0}, \left[ in(x).P'_P\right]_{0}\right\}\\
%\ben{This surely leaves a floating zero?}\tom{Comment added to say we don't write null processes}\\
&\rightarrow\phantom{^*} E, \{ \left[ out(a).in(x).stopTimer.P'_V,out(f(p,b))\right]_{1}, \\
&~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\left[in(x).P'_P\right]_{0}\}\\
%\rightarrow & \Ecal, \{ \ltag{ \{\In{x}.\stopTimer.P'_V,\Out{f(p,b)}\}}{1} \ltag{\{\Out{a},\In{x}.P'_P\}}{0}\}\\
%\rightarrow & \Ecal, \{ \ltag{ \{\In{x}.\stopTimer.P'_V,\Out{f(p,b)}\}}{1} \ltag{\{P'_P\{a/x\}\}}{0}\}\\
&\rightarrow^* E, \{ \left[ stopTimer.P'_V%\{f(p,b)/x\}
\right]_{1} \left[P'_P%\{a/x\}
\right]_{0}\}\\
&\rightarrow\phantom{^*} E, \{ \left[ P'_V%\{f(p,b)/x\}
\right]_{0} \left[P'_P%\{a/x\}
\right]_{0}\}
%
%\rightarrow &\Ecal, \left\{ \ltag{ \{ \Out{a}.\In{x}.\stopTimer.P'_V, \Out{f(p,b)}{1}, \ltag{P_P}{0} \right\}\\
%\rightarrow &\Ecal, \left\{ \ltag{ \{ \In{x}.\stopTimer.P'_V,\Out{p} \Out{b}}{1}. \ltag{P'_P\{a/x\}\} }{0} \right\}\\
%\rightarrow &\Ecal, \left\{ \ltag{ \{ \stopTimer.P'_V\{b/x\}}{1}, \ltag{\Out{b}.P'_P\{a/x\}\} }{0} \right\}\\
%\rightarrow &\Ecal, \left\{ \ltag{ \{ P'_V\{b/x\}}{1}, \ltag{\Out{b}.P'_P\{a/x\}\} }{0} \right\}\\
\end{aligned}$$ Note that the message received by $P_V$ uses the name $p$ rather than the challenge name $a$, hence, when using preemption there is no way in which the answer to the response to a timed challenge can be based on the message outputted as part of that challenge.*
Rule $\mbox{\sc (Async)}$ defines asynchronous communication, which prevents processes from blocking when they are ready to output. We could also avoid blocking by replacing instances of $out(M).P$ with $out(M).0 \mid P$, but introducing parallel composition reduces readability. Moreover, for purposes of compilation (Section 6), it is useful to consider only linear processes.
# Modelling DB protocols and attacks
We define distance bounding protocols as follows:
**Definition 1** (Distance bound protocol specification). *A distance bounding protocol specification is a tuple $(P(id),V,{\tilde{n}})$, where*
- *$P(id) = {!} new\ id. !Q$ for some process $Q$;*
- *$V = {!}V'$ for some process $V'$ that contains an event $\textnormal{event}(\textnormal{verify}(id))$.*
- *${\tilde{n}}$ is a list of names known only to $Q$ and $V$.*
*We require that no further events are used in either process and the only free names (i.e., names not declared as new or bound by an input) used are those in ${\tilde{n}}$ and the public channel $c$.*
Process $Q$ models a single run of a prover with the identity $id$ and $P(id)$ represents arbitrarily many distinct provers, each of which can run arbitrarily many times. Similarly, process $V'$ models a single run of a verifier and $V$ models arbitrarily many runs. Event “$\textnormal{event}(\textnormal{verify}(id))$” signifies a successful execution of the verifier with a prover that uses identity $id$. Anonymous protocols can use a dummy $id$ value. It is important to note that the “verify” event does not mean that we have verified that the protocol is secure, rather it means that the verifier believes it has completed a run of the protocol. This could be because there is a prover at the same location as the verifier, or it could be because an attacker has performed a successful attack and tricked the verifier.
The names ${\tilde{n}}$ are secrets known to the verifier and all provers; many well designed protocols will have no such secrets, in which case ${\tilde{n}}$ will be the empty list, nonetheless many commercial devices continue to use global shared secrets (see e.g. (Garcia et al. 2016) for one of many examples).
**Example 9**. *The protocol informally described in Example 1 can be modelled as specification $(\mathit{ProverE(id)},\allowbreak\mathit{VerifierE},\langle k \rangle)$, where $\mathit{ProverE(id)}$ and $\mathit{VerifierE}$ are as described above, and $k$ is the global shared key.*
Since attackers can be present at a number of different locations, we introduce *system contexts* as systems with “holes,” in which a process may be placed. These holes denote the locations in a system where the attacker can act, and we write them as $A$. E.g., the system context $C_1 = new\ k.[VerifierE~ \mid A~]\mid [~ProverE(id) \mid A~]$ represents a scenario in which the attacker can be co-located with the verifier $V$, and co-located with the prover $Q$, whereas $C_2 = new\ k.[~VerifierE~]\mid[~ProverE(id) \mid A~]$ represents a scenario in which the attacker is co-located with the prover and is remote from the verifier. When the context is applied to a process the $A$ symbol is replaced with that process, to give a system. E.g., $C_2[P_A] = new\ k.[~VerifierE~]\mid[~ProverE(id) \mid P_A~]$.
Using our calculus, and system contexts, we can formulate the five types of attacks against distance bounding protocols described in Section 2, in which verifiers are deceived into believing they are co-located with provers. We formulate attacks as reachability requirements over traces that represent executions of distance bounding protocols. In particular, our formulations require an execution of a verifier, with a remote prover, which ends in a verify event for a particular id.
The following definition tells us if an attacker process can be found that leads to a context performing a verify event.
**Definition 2**. *Given a name $id$ and a system context $C$, we write $\textnormal{verified}(id)\!\!:\!\!C$ if there exists a process $P_A$ and a trace: $$\begin{array}{lll}
\{c\} , C[P_A]& \!\!\!\!\!\! \xrightarrow{}^*\!\!\!\!\!\! &E, \mathcal L\cup \{\left[\mathcal P\cup \{new\ id.P\}\right]_{r}\} \\
& \!\!\!\!\!\! \xrightarrow{}\!\!\!\!\!\! &E\cup\{id'\}, \mathcal L\cup\{\left[ \mathcal P\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $id'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $id$}}\}\}\right]_{r}\}\\
& \!\!\!\!\!\! \xrightarrow{}^* \!\!\!\!\!\! &E',\mathcal L' \cup \{\left[\mathcal P' \cup \{\textnormal{event}(\textnormal{verify}(id')).P'\}\right]_{r'}\}
%\mathcal P \cup \{\phase{t}{P\activesubst{n'}{n}}\}\\
%&\reduc^*& E',\mathcal P' \cup \{\phase{s}{\Out{n'}.P'}, \phase{s}{\In{x}.Q'}\} \\
%&\reduc& E',\mathcal P'\cup\{\phase{s}{P'},\phase{s}{Q'\activesubst{n'}{x}}\}
\end{array}$$ where the only free name in $P_A$ is the public channel name $c$ and $P_A$ does not contain timers nor events.*
It follows from our definition that $\textnormal{verified}(id)\!\!:\!\!C$ denotes a successful execution of a verifier, therefore we would expect it to hold for any context that places a verifier and prover, with the identity $id$, at the same location. By comparison, we would not expect $\textnormal{verified}(id)\!\!:\!\!C_1$, for the aforementioned context $C_1$, which places the verifier and prover at different locations, unless the protocol being modelled is insecure.
Using this we can now formally define the different types of distance bounding attacks.
**Definition 3**. *Distance bound protocol specification ($P(id),V,{\tilde{n}}$) is vulnerable to *relay (or mafia) fraud*, if $\textnormal{verified}(id)\!\!:\!\!new\ {\tilde{n}}.[~V \mid A~]\mid[P(id) \mid A]$.*
It follows from the definition that a relay attack is possible if the prover and verifier are at different locations, and an attacker process is co-located with each of the prover and verifier. Such an attack typically involves the attacker process co-located with the verifier answering the timed challenges, using messages passed from the other location. To keep our definitions simple we require the same attacker process at both locations, though different parts of this process can act at each location. E.g., an attacker process $P_{PA} \mid P_{VA}$ might define process $P_{PV}$ to interact with the verifier and $P_{AV}$ to interact with the prover.
**Example 10**. *There is no process $P_A$ such that $\textnormal{verified}(id)\!\!:\!\![~VerifierE \mid P_A~]\mid[ProverE(id) \mid P_A]$, i.e., no attacker can trick the verifier into believing that it has verified $id$ when the provers are at a different location. We informally reasoned why this protocol is safe from relay attacks in Section 2 and we will verify this result automatically in Section 7.*
Relay/mafia fraud considers an attacker that does not have the secret values of a normal prover. A more powerful “dishonest prover” attacker has access to such secrets.
**Definition 4**. *Distance bound protocol specification ($P(id),V,{\tilde{n}}$) is vulnerable to:*
- **distance fraud*, if $\textnormal{verified}(id)\!\!:\!\!new\ {\tilde{n}}.[~V~]\mid[~DP{\text -}A(id)~]$*
- **distance hijacking*, if $\textnormal{verified}(id)\!\!:\!\!new\ {\tilde{n}}.[~V\mid P(id')~]\mid[~DP{\text -}A(id)~]$*
*where $P(id) = ~ ! new\ id. !Q$ and $DP{\text -}A(id)$ denotes $! new\ id.\allowbreak out(id).\allowbreak Q'\mid\allowbreak A$, where $Q'$ outputs bound and free names of $Q$ (including names in ${\tilde{n}}$, which are otherwise hidden from the attacker)*
*and the results of any private function applications in $Q$,*
*and $A$ is the context hole.*
The process $DP{\text -}A(id)$ reveals all the secret values of a normal prover to the attacker, which captures a dishonest prover attacker.
**Example 11**. *Specification $(\mathit{ProverE(id)},\mathit{VerifierE},\langle k \rangle)$ is vulnerable to distance fraud. The prover process does not declare new names, and there are no private functions used therefore: $$\mathit{DP{\text -}A(id)} =~ !new\ id.out(id).out(k)\mid A$$ We define $P_A$ as the process that receives the key $k$ from process $DP{\text -}A$, uses the key to decrypt the challenge and response, and sends the response, without waiting for the challenge: $$P_A = in(k). in(x).
\textnormal{let } (chal,resp)=dec(x,k) \textnormal{ in }
out(resp)$$ Since the response is sent before the timer starts, it has time to make it to the verifier before the timer is active. Hence, $[~\mathit{VerifierE}~]\mid[~!new\ id.out(id).out(k)\mid P_A~]$ can reduce such that the verifier can perform the $verified$ event, which means that $\textnormal{verified}(id)\!\!:\!\![~\mathit{VerifierE}~]\mid[~\mathit{DP{\text -}A}(id)~]$ holds and the attack is possible.*
*The attack works because the attacker can preempt the challenge. This can be prevented if the challenge must be observed before a response can be provided, which can be achieved by including a nonce in the challenge and requiring that nonce to be included in a response. Hence, we considered the revised specification ($\mathit{ProverE2(id)}, \mathit{VerifierE2}, \langle k \rangle$), where $$\begin{array}{lcl}
\mathit{VerifierE2} &= &!in(id).new\ chal.new\ resp.\\
&&out(enc((chal,resp),k)).~~~~~~~\\
&& new\ c2. startTimer.\\
&& out(chal,c2).in(=\!\!resp,=\!\!c2).\\
&& stopTimer. \textnormal{event}(\textnormal{verify}(id))
\end{array}$$ $$\begin{array}{lcl}
\mathit{ProverE2(id)} &\!\!\!\!=\!\!\!\!& !new\ id.!out(id)in(x).\\
&& \textnormal{let } (chal,resp)=dec(x,k) \textnormal{ in }\\
&& in(=\!\!chal,x).out(resp,x) \\
%\\
%System2 &=& \new{k_C}. [!\new finished.Reader2] \\
%&&\mid [!Card2 \mid !\new n.Reader2\{n/finished\}]
\end{array}$$ It can be shown that this fix suffices to defend against distance fraud attacks. Intuitively, the nonce $c2$ is only sent when the timer is running, so the attacker can never return this in time if not co-located with the verifier.*
Terrorist provers are less powerful than dishonest provers, because they will not send their secret values to a third party. Nevertheless, by considering terrorist provers working with another attacker that is co-located with the verifier, we can identify further attacks.
**Definition 5**. *Distance bound protocol specification ($P(id),V,{\tilde{n}}$) is vulnerable to:*
- **terrorist fraud*, if $\textnormal{verified}(id)\!\!:\!\!new\ {\tilde{n}}.[~V\mid A~]\mid[~TP{\text -}A(id)~]$*
- **assisted distance fraud*, if $\textnormal{verified}(id)\!\!:\!\!new\ {\tilde{n}}.[~V \mid DP{\text -}A(id')~]\mid[~TP{\text -}A(id)~]$*
*where $P(id) = ~ ! new\ id. !Q$, $DP{\text -}A(id')$ is as specified in Definition 4, and $TP{\text -}A(id)$ denotes $! new\ id. out(id).!Q'\mid A$, where $Q'$ is the process that acts as an oracle with all relevant functions for all bound and free names and private function applications in $Q$, and $A$ is the context hole.*
The process $TP{\text -}A$ will perform operations on behalf of the attacker, e.g., signing, encrypting and decrypting any values the attacker wishes, but it will not reveal secret values.
**Example 12**. *Specification ($\mathit{ProverE2(id)},$ $\mathit{VerifierE2},$ $\langle k \rangle$) is vulnerable to terrorist fraud attacks. We have $$\begin{array}{lcl}
TP{\text -}A(id) &\!\!\!\!=\!\!\!\!& ! (new\ id.out(id)\\
&& \mid in(x). \textnormal{let } y=dec(x,k) \textnormal{ in }out(y)\\
&& \mid in(x).out(enc(x,k))) \mid A\\
\end{array}$$ This process can receive the encrypted challenge from the verifier, decrypt it, and send the resulting plaintext to an attacker process co-located with the verifier, all before the timer is started. At the verifier’s location we consider the following attacker process $P_A = in(chal,resp).in(=chal,x).out(resp,x)$, this process can receive the challenge information from the terrorist prover process, and then use it to complete the verifier’s challenge. This suffices to show $\textnormal{verified}(id)\!\!:\!\!new\ k.[~V \mid A~]\mid[~TP{\text -}A(id)~]$, hence, the specification is vulnerable to terrorist fraud.*
**Example 13**. *The second, more secure, protocol in Example 2 can be modelled in our calculus as $(V2,P2,\langle \rangle)$ where: $$\begin{array}{lcl}
\mathit{P2(id)} &\!\!\!\!=\!\!\!\!& !new\ id\mathrel.!out(id)\mathrel.in(x)\mathrel.\\
&& \textnormal{let } (chal,resp)=dec(x,lookup(id)) \textnormal{ in }\\
&& out(ready)\mathrel.in(=\!\!chal,nonce)\mathrel.\\
&&out(xor(nonce,lookup(id)),resp) \\
%\\
%System2 &=& \new{k_C}\mathrel. [!\new finished\mathrel.Reader2] \\
%&&\mid [!Card2 \mid !\new n\mathrel.Reader2\{n/finished\}]
\end{array}$$*
*$$\begin{array}{lcl}
\mathit{V2} &= &!in(id)\mathrel.new\ chal\mathrel.new\ resp\mathrel.\\
&&out(enc((chal,resp),lookup(id)))\mathrel.~~~~~~~\\
&&in(ready)\mathrel.new\ nonce\mathrel.\\
&& startTimer\mathrel. out(chal,nonce)\mathrel.in(xb,=\!\!resp)\mathrel.\\
&& stopTimer\mathrel. \textnormal{let } xb=h(nonce,lookup(id))\\
&&~~~~~~~~~\textnormal{in } \textnormal{event}(\textnormal{verify}(id)) \textnormal{ else }0
\end{array}$$ and $\mathit{lookup}$ is a private function used to find a unique key shared between one particular prover and the verifier, and $h$ is a public hash function.*
*We show in Section 7 that there does not exist any attacker process that can make any of the system contexts that model the attacker perform a verify event for the id being tested. Therefore this protocol is secure against all of these possible, different distance bounding attacks.*
We only consider two locations when capturing different types of attacks against distance bounding protocols. More attack scenarios would be possible by considering attackers at other locations, however, these scenarios are strictly weaker than those presented, so they would not lead to interesting definitions.
# A hierarchy of attacks
We have modelled five types of attack against distance bounding protocols by considering various scenarios in which verifiers are deceived into believing they are co-located with provers. These scenarios consider the following terms:
- $V\mid A$, a verifier co-located with a basic attacker (relay fraud and terrorist fraud);
- $V$, a verifier in isolation (distance fraud);
- $V\mid P(id')$, a verifier co-located with honest provers (distance hijacking);
- $V\mid DP{\text -}A(id')$, a verifier co-located with dishonest provers (assisted distance fraud);
- $P(id)\mid A$, remote provers co-located with an attacker (relay fraud);
- $DP{\text -}A(id)$, remote dishonest provers in isolation (distance fraud and distance hijacking); and
- $TP{\text -}A(id)$, remote terrorist provers in isolation (terrorist fraud and assisted distance fraud).
Yet, numerous combinations of these terms were not considered by the definitions in the previous section, e.g., we have not considered a verifier co-located with a basic attacker and some other prover, along with a remote prover and a basic attacker: $[V\mid A \mid P(id')] ~\mid~[P(id) \mid P(id)]$. We also have not considered co-location of remote dishonest provers, e.g., $DP{\text -}A(id') \mid TP{\text -}A(id)$.
We now consider a more general setting whereby a verifier is co-located with zero or more of a basic attacker $A$, honest provers $P(id')$, terrorist provers $TP{\text -}A(id')$, and dishonest provers $DP{\text -}A(id')$. These provers all use identifiers that are distinct from the identifier $id$, which is being used in an attempt to deceive the verifier. Moreover, at a distinct, remote location, we consider one or more of honest provers $P(id)$, terrorist provers $TP{\text -}A(id)$, and dishonest provers $DP{\text -}A(id)$. Furthermore, the remote location may additionally include one or more of a basic attacker $A$, honest provers $P(id')$, terrorist provers $TP{\text -}A(id')$, and dishonest provers $DP{\text -}A(id')$. This gives way to $2^4\cdot 2^3 \cdot 2^4 = {2\,048}$ scenarios. Albeit, we can disregard scenarios in which identifier $id$ is absent (since without this any attack will be an attack on authentication, rather than a distance bounding attack, and authentication attacks can be found using a range of other well established methods, e.g. (Abadi, Blanchet, and Fournet 2017)). This gives us $2^4 \cdot (2^3-1) \cdot 2^4 = {1\,792}$ scenarios to consider, significantly more than the five scenarios that have been identified in the literature.
We can reduce the number of scenarios we need to consider by observing that there is a strict order on the capabilities of the different attacker processes:
**Lemma 1**. *For any distance bounding protocol specification $(P(id),V,{\tilde{n}})$, from which we derive $DP{\text -}A$ and $TP{\text -}A$, and for all system contexts $C$, sets of names $E$ and names $x\in\{id,id'\}$, we have $$\begin{aligned}
%&\verifiedE{C[0]}{id}{E}\\
%&\quad \Rightarrow
%&\verifiedE{C[A]}{id}{E}\\
%&\quad \Rightarrow
&\textnormal{verified}(id)\!\!:\!\!C[A\mid P(x)]\\
&\quad \Rightarrow \textnormal{verified}(id)\!\!:\!\!C[TP{\text -}A(x)] \\
&\quad \Rightarrow \textnormal{verified}(id)\!\!:\!\!C[DP{\text -}A(x)]
%
%\intertext{and}
%&\verifiedE{C[0]}{id}{E}\\
%&\quad \Rightarrow \verifiedE{C[\prover(x)]}{id}{E} \\
%&\quad \Rightarrow \verifiedE{C[A\mid\prover(x)]}{id}{E}
\end{aligned}$$ Moreover, no reverse implication holds.*
By filling a context’s hole with a process containing a hole (as above), we derive a context (which is required by the verified predicate).
It follows from Lemma 1 that we need not consider more than one of the terms $P(x)$, $DP{\text -}A(x)$, or $TP{\text -}A(x)$ at a particular location. For instance, the verifier can perform the verify event in the context ${[ V ]} \mid {[P(id)\mid A \mid DP{\text -}A(id)]}$ if and only if it can perform the event in the context ${[ V ]} \mid {[DP{\text -}A(id)]}$. Hence, we need not consider both these contexts; we need only consider the latter, simpler context.
Honest and dishonest provers represent an arbitrary number of provers. (The bound name used as the id of these provers will be substituted for another value by the $\mbox{\sc (New)}$ rule.) Hence, we have:
**Lemma 2**. *For any distance bounding protocol specification $(P(id),V,{\tilde{n}})$, from which we derive $DP{\text -}A$ and $TP{\text -}A$, and for any system contexts $C[\_]$, sets of names $E$, names $id$ and $id'$, and $X \in\{P,DP{\text -}A,TP{\text -}A\}$, we have: $$\begin{gathered}
\textnormal{verified}(id)\!\!:\!\!C[X(id')\mid X(id)] \Leftrightarrow \textnormal{verified}(id)\!\!:\!\!C[X(id)]
\end{gathered}$$*
It follows from Lemma 2 that if process $X(id)$ is present, then it is not necessary to consider the corresponding $X(id')$ process as well.
When there is a dishonest prover at a different location to a basic attacker process, the dishonest prover could send all of its secrets to the basic attacker process enabling it to also act as a dishonest prover:
**Lemma 3**. *For any distance bounding protocol specification $(P(id),V,{\tilde{n}})$, from which we derive $DP{\text -}A$, and for all processes $P$ and $Q$, names $id$, tuple of names ${\tilde{n}}$, and sets of names $E$, and all names x (including $x=id$), we have that*
*$~\textnormal{verified}(id)\!\!:\!\! new\ {\tilde{n}}.[P \mid A ] \mid [DP{\text -}A(x) \mid Q]$
$\Leftrightarrow \textnormal{verified}(id)\!\!:\!\! new\ {\tilde{n}}.[P \mid DP{\text -}A(x) ] \mid [DP{\text -}A(x) \mid Q]$
$\Leftrightarrow \textnormal{verified}(id)\!\!:\!\! new\ {\tilde{n}}.[P \mid DP{\text -}A(x) ] \mid [A \mid Q]$*
Our observations reduce the number of interesting, distinct, system contexts to 27, each of which models a different distance bounding attack scenario, and protection against which offers a distinct security property. These 27 contexts are given in the figure in the Appendix.
Lemma 1 lets us order contexts in terms of the strength of the security properties they represent. For instance, if we replace $TP{\text -}A(id)$ with $DP{\text -}A(id)$, then the attacker is strictly more powerful, and the security properties they represent are stronger. Additionally, we note that adding processes to a context will not affect the verified, predicate, e.g., $\textnormal{verified}(id)\!\!:\!\!C[A] \Rightarrow \textnormal{verified}(id)\!\!:\!\!C[A\mid P(x)]$. The partial order this leads to is shown in the figure in the Appendix.
For any protocol, if it is secure against an attack scenario in this ordering then it is also secure against the attack scenarios directly below it. Additionally, we can find examples to show that all the attack scenarios are different, and that attack scenario that are not directly above or below each other are unrelated.
This partial ordering of attack scenarios the Appendix tells us that protection against distance hijacking attacks is strictly stronger than security against distance fraud attacks, and that security against assisted distance fraud is stronger than security against terrorist fraud attacks, which in turn is a stronger property than security against relay attacks. However, distance hijacking and assisted distance fraud are not directly comparable properties. To illustrate this we could consider a verifier with an override mode: if a process sent it the secret key of a prover then it would accept it as local. Such a protocol could be secure against assisted distance fraud but would not be secure against distance hijacking.
On the other hand we could consider a verifier that would correctly distance bound a process and would then accept any identity from that local process. Such a protocol could be secure against distance hijacking but not against assisted distance fraud. Therefore, the strongest property that a distance bounding protocol can have is protection from both distance hijacking and assisted distance fraud.
To separate many of the distance bounding properties we need to consider a verifier that will verify any process that sends it a secret key. This is the difference between what a dishonest prover and a terrorist prover can do, however there are currently no proposals for distance bounding protocols with this behaviour. Therefore, it is a safe assumption that for any proposed distance bounding protocol, if there is no local attacker process, then the ability to send a secret key does not add any additional power. This means that:
**Assumption 1**. *Distance bounding protocols will not be designed so that a correct prover could send their secret key to the verifier. I.e.,*
*$~~~\textnormal{verified}(id)\!\!:\!\! new\ {\tilde{n}}.[V] \mid [DP{\text -}A(id)]$
$~~~~~~~~~~~~~~~~~~~~~~~ \Leftrightarrow \textnormal{verified}(id)\!\!:\!\! new\ {\tilde{n}}.[V] \mid [TP{\text -}A(id)]$*
All examples of distance bounding protocols we have seen in the literature do not distance bound the verifier to the prover. This would mean that the attacker does not gain any additional power by being local to the prover, rather than local to the verifier. This further reduces the number of interesting cases we need to consider.
**Assumption 2**. *In the protocols we consider the prover does not also distance bound the verifier. I.e., $\textnormal{verified}(id)\!\!:\!\! new\ {\tilde{n}}.[V \mid A] \mid [P(id)]$
$~~~~~~~~~~~~~~~~~~~~~~~~ \Leftrightarrow \textnormal{verified}(id)\!\!:\!\! new\ {\tilde{n}}.[V \mid A] \mid [P(id) \mid A]$*
These assumption, along with the lemmas above, leave us with 14 distance bounding attack scenarios, which can be ordered using the lemmas above. This ordering is shown in Figure [fig:order].
**Discussion:** With the assumption that transmitting the secret key does not matter, assisted distance fraud becomes the most powerful distance bounding property. If a distance bounding protocol is secure against this attack scenario, then none of the other attacks are possible. However, this property is very strong; industrial distance bounding protocols such as MasterCard’s RRP or NXP’s proximity check do not have this property nor do they need it: If a bank card or key fob has been fully compromised, then an attacker may send all key information from this device to the same location as the verifier and so pass the verification.
The lines which dissect Figure [fig:order] each represent different possible attacker models, and each area is dominated by a single property, which, if checked, will prove security for that particular attacker model. Assisted distance fraud, and all of the other attack scenarios that require a terrorist fraud attacker process (as indicated by the red dotted line in Figure [fig:order]), rely on the terrorist fraud attacker simply deciding not to send their key. While such an attacker could exist, there is nothing to stop an attacker, that has compromised a device, from sharing the secret key. Therefore, the additional protection provided by protecting against a terrorist attacker is questionable in some attacker models.
The brown, large dashed lines separates the properties in which the verifier is checking a compromised prover from an uncompromised prover. Many of the use cases for distance bounding protocols aim to protect a device against relay attack, thereby preventing criminals from taking a victim’s car or making a payment with the victim’s EMV card, for instance. In this attacker model, if the attackers have compromised the device, then they can simply clone it, making the distance bounding attack unnecessary. In this model, checking $\textnormal{verified}(id)\!\!:\!\![V \mid DP{\text -}A(id') \mid A] \mid [P(id) \mid DP{\text -}A(id')]$ ensures that all of the possible relevant security properties hold. For this security property to hold, the attacker should not be able to pretend to be an uncompromised device, regardless of how many other devices are compromised. We define this property as uncompromised distance bounding:
**Definition 6** (Uncompromised Distance Bounding attack). *Given a name $id'$ and a distance bounding protocol ($V,P(id),{\tilde{n}}$), from which we derive a dishonest prover $DP{\text -}A(id')$, we say that the protocol is vulnerable to an uncompromised distance bounding attack if: $\textnormal{verified}(id)\!\!:\!\!new\ {\tilde{n}}.[V \mid DP{\text -}A(id')] \mid [P(id) \mid DP{\text -}A(id')]$ otherwise we say that it is safe from this attack.*
As we are dealing with dishonest provers, by Lemma 3: $$\begin{aligned}
&\textnormal{verified}(id)\!\!:\!\!new\ {\tilde{n}}.[V \mid DP{\text -}A(id')] \mid [P(id) \mid DP{\text -}A(id')]\\
& \Leftrightarrow \textnormal{verified}(id)\!\!:\!\!new\ {\tilde{n}}.[V \mid A] \mid [P(id) \mid DP{\text -}A(id')]\\
&\Leftrightarrow \textnormal{verified}(id)\!\!:\!\!new\ {\tilde{n}}.[V \mid DP{\text -}A(id')] \mid [P(id) \mid A]
\end{aligned}$$ therefore any of these system contexts could be used to represent uncompromised distance bounding attacks. We choose the one that makes it clear that the dishonest prover can act at both locations.
The purple dot-dashed line separates the attack scenarios that have only a remote attacker from those that let the attacker act both locally to the verifier and remotely. In the case where transmissions from the verifier can be picked up remotely and the attacker can only act remotely, the strongest possible property is distance hijacking. However, in many applications the messages from the verifier are limited to the local area (e.g. due to the RFID technology as used by contactless EMV cards), therefore the attacker must be able to act locally to the verifier and these attack scenarios do not apply.
The green small dashed line marks out the attack scenarios that assume trusted hardware from those that allow some provers to be compromised. Our ordering shows that $\textnormal{verified}(id)\!\!:\!\! new\ {\tilde{n}}.[V \mid P(id) \mid A] \mid [P(id) \mid A]$ is the most powerful property that can be tested in this category. This attacker corresponds to, for instance, a relay attack against an EMV card, which uses another, different EMV card at the verifier’s location. The use of this other EMV card that is co-located with the verifier makes it a more powerful attacker than a basic relay attack, but it is still less powerful than an uncompromised distance bounding attack, because it does not require any cards to be compromised. We do not believe this particular attack scenario has been identified before, as a distinction from relay attacks, so we call this “relay hijacking”.
In summary, our ordering tells us that:
- If the protocol is aiming to defend against terrorist fraud attackers, then it should be checked against *assisted distance fraud*.
- If the attacker model does not include terrorist fraud attackers, then the strongest protection a protocol can have is against both *distance hijacking* and *uncompromised distance bounding* attacks.
- If the attacker model does not require protection for a compromised prover, then the strongest attack that needs to be defended against are *uncompromised distance bounding* attacks.
- If a distance bounding protocol assumes trusted hardware devices, then the strongest attack that needs to be defended against is *relay hijacking*: $\textnormal{verified}(id)\!\!:\!\![V \mid P(id') \mid A] \mid [P(id) \mid A]$.
- If the attacker model only considers attackers that are remote from the verifier, then the strongest attack that needs to be defended against is *distance hijacking*.
# Automated reasoning
To enable automated reasoning, we define a compiler from our timer location calculus to a dialect of the applied pi calculus with phases (Blanchet, Abadi, and Fournet 2008), which can be automatically reasoned with using the ProVerif tool (Blanchet et al. 2018). Phases are used to define an ordering on reduction, e.g., processes in phase 1 can only be executed before the processes in phase 2, which come before the processes in phase 3, etc. Beyond phases, the applied pi-calculus adds named communication channels, e.g., $out(c,m)$ outputs message $m$ on the channel $c$. Channels can be public or private, and the attacker can only send and receive messages on public channels. The applied pi-calculus does not have timers or locations, and our compiler encodes the start timer, stop timer and locations using other primitives. Thus, compilation enables distance bounding protocols to be verified automatically using ProVerif.
We restrict compilation to extended linear processes that contain at most one timer:
**Definition 7**. *A *linear process* is a process without parallel composition or replication. Moreover, an *extended linear process* is a process $new\ {\tilde{n}}.\allowbreak L_1 \mid \allowbreak \dots \mid \allowbreak L_i \mid\allowbreak !L_{i+1} \mid\allowbreak \dots \mid\allowbreak !L_n$, where $L_1,\allowbreak\dots,\allowbreak L_n$ are linear processes.*
Linear processes allow us to express all distance bounding protocols from the literature, so they do not reduce the usefulness of our method.
Using linear processes, we introduce a technique to simplify the detection of vulnerabilities and define a compiler that allows us to take advantage of that technique.
**Proof technique:** It follows from Definition 2 that: if $\textnormal{verified}(id)\!\!:\!\!new\ {\tilde{n}}.[! L_1 \mid L_2 \mid A ] \mid [ L_3 \mid A ]$ such that only $L_1$ contains a timer, then there exists a successful execution of $L_1$. Moreover, the following lemma shows that it is sufficient to consider $L_1 \mid ! \textnormal{blind}(L_1)$ in place of $!L_1$, where $\textnormal{blind}(L_1)$ is $L_1$ after removing timer actions ($startTimer$ and $stopTimer$) and events, hence, it suffices to isolate timers and events to a single instance of $L_1$.
**Lemma 4**. *For all system contexts $new\ {\tilde{n}}.[! V_L \mid L_v \mid A ] \mid [ L_p \mid A ]$, sets of names $E$ and name $id$, such that $V_L$, $L_v$ and $L_p$ are linear processes and only $V_L$ contains a timer, we have: $\textnormal{verified}(id)\!\!:\!\!new\ {\tilde{n}}.[! V_L \mid L_v \mid A ] \mid [ L_p \mid A ]
\Rightarrow
\textnormal{verified}(id)\!\!:\!\!new\ {\tilde{n}}.[ V_L \mid ! \textnormal{blind}(V_L)\mid L_v\mid A ] \mid [ L_p \mid A ]$.*
It follows from Lemma 4 that distance bounding attacks can be detected by checking whether a single instance of the verifier is deceived. Moreover, we need only consider a single unreplicated timer.
**Our compiler:** Intuitively, the goal of our compiler is to encode a single timer using phases. In particular, all processes should initially be in phase 0, hence, all processes are initially active. Once the timer is activated, we advance all processes at the same location as the timer to phase 1, hence, only processes at the timer’s location are active. Finally, once the timer is deactivated, we advance all processes to phase 2, hence, all processes are active. Thus, compilation encodes timers as phases.
Encoding the activation and deactivation of timers as phases is straightforward, indeed, we merely replace $startTimer.P$ with $1\!:\!P$ and $stopTimer.Q$ with $2\!:\!Q$. But, encoding the advancement of other processes at the same location as the timer from phase $0$ to phase $1$ is problematic, as is advancing processes at different locations from phase 0 to phase 2, because we cannot know when processes should advance. We overcome this problem by over-approximating advancement.
We over-approximate by ensuring processes can advance between phases at any time. It suffices to consider advancements just before input operations, because processes ready to output can be reduced by an attacker that receives those outputs before an advancement and replays the messages received afterwards, and other processes do not produce communications, so it does not matter whether they happen before or after an advancement. We define the following function to produce all ways in which advancements can be inserted into a process before inputs.
**Definition 8**. *Given a timer location calculus process $P$, and a non-empty list of integers $ds$, we define the function $phases$, to applied pi-calculus processes, as follows $$phases(P,ds) = !P_1 \mid !P_2 \mid \dots \mid !P_n$$ where $\{P_1,\dots,P_n\} = phasesSet(P',ds)$, $P'$ equals $P$ with every in(x) replaced with in(,x) and every out(M) replaced with out(,M) and function $phasesSet$ is defined as follows:
$phasesSet(P,[d])$
$~~~~~~~~~~~~ = \{ C[d\!:\!in(M,x).P'] ~:~ P = C[in(M,x).P']\} \cup \{ P \}$
$~~~~~phasesSet(P,d_1\!::\!d_2\!::\!ds)$
$~~~~~~~~~~~~ = \{ C[d_1\!:\!in(M,x).P''] ~:~ P = C[in(M,x).P']~ \land P'' \in$
$~~~~~~~~~~~~~~~phasesSet(P',d_2\!::\!ds) \} \cup phasesSet(P,d_2\!::\!ds)$
*
Using function $phases$, we define our compiler, first for systems with verifiers co-located with attackers and then for systems with remote attackers.
**Definition 9**. *Given a system context $S = new\ {\tilde{n}}.([! V_L \mid L_v \mid A] \mid [ !new\ id.!P_L \mid L_p \mid A ])$ and name $id$, we define the $compile(id,S)$ as $$\begin{gathered}
new\ {\tilde{n}}.(tToPh(V_L) \mid \\
phases(\textnormal{blind}(V_L),[1,2]) \mid phases(L_v,[1,2]) \mid \\
!new\ id.phases(P_L,[2])\mid phases(L_p,[2]))
\end{gathered}$$ where $tToPh(L)$ is $L$ after replacing $startTimer.P$ with $1\!:\!P$ and $stopTimer.Q$ with $2\!:\!Q$ and every in(x) replaced with in(,x) and every out(M) replaced with out(,M)*
Timers limit communication between locations. Hence, once timers have been encoded as phases, we no longer require locations. Thus, our compiler also removes locations. (Once locations are removed, we can consider a single hole, rather than multiple holes. Such a hole can be left implicit, because it will be introduced by Definition 11, below.) It follows that our compiler outputs processes in the applied pi calculus with phases, which can be automatically reasoned with using ProVerif.
When the verifier and attacker are not co-located, we must prevent the attacker communicating with the verifier’s location whilst the timer is running.
To do this, we replace the public channel “$c$” with a private channel “$priv$” between phase 1 and 2 (i.e., whilst the timer is active), thereby denying the attacker access to the communication channel.
To maintain equivalence between compiled processes in the applied pi-calculus with phases and the original process in the timer location calculus, compilation introduces the following processes:
- $!in(\defaultchannel,x).1\!:\!out(priv,x)$, respectively $!1\!:\!in(priv,x).\allowbreak2\!:\!out(\defaultchannel,x)$, which allows messages sent on public channel $c$ in phase 0 (before the timer starts), respectively private channel $priv$ in phase 1 (whilst the timer is running), to be received on private channel $priv$ in phase 1, respectively public channel $c$ in phase 2 (after the timer stops).
The first process permits preemption, whereby a message is sent before a timer starts and received when the timer is running, and the second permits a message sent whilst a timer is running to be received after the timer stops.
- $!1\!:\!in(priv,x).out(priv,x)$, which allows messages sent on private channel $priv$ to be buffered, i.e., received and relayed.
This final process ensures that any reduction by the $\mbox{\sc (Async)}$ rule on private channel $priv$ in our timer location calculus can be mapped to a reduction in the applied pi-calculus, which has no such rule (a similar processes isn’t required for reductions by the $\mbox{\sc (Async)}$ rule on public channel $c$, because the attacker process can simulate such reductions).
**Definition 10**. *Given a system context $S=new\ {\tilde{n}}.[! V_L \mid L_v ] \mid [ !new\ id.!P_L\mid L_p\mid A ]$ and a name $id$, we define $compile(id,S)$ as
$new\ priv.new\ {\tilde{n}}.(renameC(priv,tToPh(V_L)$
$~~\mid~renameC(priv,phases(\textnormal{blind}(V_L),[1,2]))$
$~~\mid~renameC(priv,phases(L_v,[1,2]))$
$~~\mid~ !new\ id.(phases(P_L,[2]))\mid phases(L_p,[2])$
$~~\mid~!in(\defaultchannel,x).1\!:\!out(priv,x)\mid!1\!:\!in(priv,x)2\!:\!out(\defaultchannel,x)$
$~~\mid~!1\!:\!in(priv,x).out(priv,x)$
where $tToPh(L)$ is defined above and $renameC(a,P)$ is process $P$ with every occurrence of the channel $c$ used for input and output between all $1\!:\!$ and $2\!:\!$ actions replaced with the channel $priv$.*
The ProVerif tool (Blanchet et al. 2018) can test to see if there exists an attacker process that can make an event reachable. In this paper we only require events that are a function application to new names, which can be defined as follows. Although ProVerif can test such properties, the corresponding definition has not previously been formally defined, we do so here:
**Definition 11**. *We write $\textnormal{ev}(f(a_1,\dots,a_i)),\mathit{Init}\!:\!P$ if there exists a process $Q$ such that the free names of $Q$ are a subset of the names $Init$ and $Q$ does not contain any events, and a trace:*
*$\mathcal{T} = \mathit{Init},\{P | Q\} \rightarrow^* E,\{\textnormal{event}(f(b_1,\dots,b_i)).P'\}\cup \mathcal P$*
*and for $1\leq j \leq i$ the trace $\mathcal{T}$ contains the reductions:*
*$E_j,\mathcal P_j \cup \{new\ a_j.P_j \} \rightarrow E_j\cup\{b_j\}, \mathcal P_i \cup \{ P_j\{b_j/a_j\}\}$*
The following theorem tells us that we can check the compiled system in the applied pi-calculus and concluded security results about the system with locations:
**Theorem 1**. *Given a system context $S = new\ {\tilde{n}}.[! V_L \mid L_v \mid A] \mid [ !new\ id.!P_L\mid L_p\mid A ]$ or $S = new\ {\tilde{n}}.[! V_L \mid L_v ] \mid [ !new\ id.!P_L\mid L_p\mid A ]$, and a name $id$, we have*
*$not~ev(\textnormal{verify}(id)),\{c\}\!:\!compile(id, S)$
$~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \Rightarrow \textnormal{$\neg$ verified}(\{c\},id)\!\!:\!\!S$*
# Case studies
We have implemented the compiler introduced in the previous section. Using this tool and ProVerif we analysed various distance bounding protocols. The tool and all of the model files mentioned in this section are available on the website given in the introduction.
**Contactless payment protocols:** Smart cards use the EMV protocol to perform contact-based and contactless payments via payment terminals (EMVCo 2011, 2016). EMV Contactless cards make use of ISO/IEC 14443 for the communication between the card and terminal. ISO/IEC 14443 is a standard that specifies near-field communication at 13.56 MHz. This standard is widely used for bank cards and cards for access control (e.g. for buildings) and public transport. Due to its physical characteristics it is not possible to communicate over a long distance using ISO/IEC 14443. Even with a very powerful antenna active communication is only possible up to around a meter (Habraken et al. 2015).
The EMV protocol comprises of an exchange of transaction data and then the card generates a MAC (called the Application Cryptogram or AC) using a session key based on a key shared between the smart card and the card issuer and the Application Transaction Counter (ATC), which equals the number of times the card has been used and will provide freshness to the transaction. The AC is used for verification of the transaction by the card issuer. As the payment terminal cannot read the AC, the card also signs the transaction data, known as the Signed Dynamic Application Data (SDAD) and the payment terminal uses this to verify the transaction.
MasterCard’s Relay Resistance Protocol (RRP) (EMVCo 2016), as part of an EMV transaction, is presented in Figure 2. RRP is an extension of the EMV protocol, for which a new command is added, namely the *EXCHANGE RELAY RESISTANCE DATA* command. In a regular EMV session, a transaction is initiated by executing the *SELECT* command, to select the EMV applet on the smart card, and then the *GET PROCESSING OPTIONS* command to provide information about the capabilities of the terminal to the card.
[msc diagram omitted]
MasterCard’s Relay Resistance Protocol
The card will typically respond to the *GET PROCESSING OPTIONS* message with the Application Interchange Profile (AIP) and Application File Locator (AFL), used to indicate the capabilities of the card and the location of data files respectively. To finalise a transaction the *GENERATE AC* command is used. This command includes a nonce, known as the Unpredictable Number (UN), to provide freshness to the transaction, and an AC, and if the card supports it the SDAD, are them returned.
The new command added in RRP is the *EXCHANGE RELAY RESISTANCE DATA* command, which will be timed and is typically executed after the *GET PROCESSING OPTIONS* command. The terminal will send a nonce (*Terminal Relay Resistance Entropy*), which will also be used as the Unpredictable Number for the rest of the transaction. The card will respond with another nonce (*Device Relay Resistance Entropy*) and three timing estimates (minimum time for processing, maximum time for processing and estimated transmission time). The maximum time serves as an upper bound for the terminal’s timer. Both random numbers and the timing information are included in the SDAD. If the card does not respond in time, it is assumed that it is not actually present at the current location and the data may be relayed.
MasterCard’s RPP is similar to PaySafe (Chothia et al. 2015), though PaySafe makes fewer changes to the previous EMV specification. No new commands are introduced; rather than sending the nonce using the *EXCHANGE RELAY RESISTANCE DATA* as in RRP, it is included in the *GET PROCESSING OPTIONS* command and a nonce is added in the corresponding response. This exchange is timed to detect possible relay attacks.
Mauw et al. (Sjouke Mauw et al. 2018) looked at PaySafe and observed that it is vulnerable to distance fraud attacks and suggested adding the UN nonce to the timed response to protect against this. We note that the same weakness to distance fraud applies to MasterCard’s protocol. Due to the physical characteristics of ISO/IEC 14443, we consider distance fraud attacks not to be applicable to protocols using this standard, as it will always be necessary to have a local adversary in order to be able to communicate with the local reader. Furthermore, once a card is compromised, it should not lead to a compromise of other cards but the compromised card should be considered lost as the information on it can be used to clone the card, as discussed in Section 5. This means that we do not consider attacks such as terrorist fraud or distance hijacking applicable to these protocols.
**NXP’s distance bounding protocols:** NXP’s Mifare Plus cards are used in, for example, public transport and for building access control and also make use of the ISO/IEC 14443 specification for contactless communication. The cards use a proprietary distance bounding protocol. It is not publicly known what protocol is used.
Nevertheless, NXP have been granted a patent (Janssens 2017) and have filed a further patent application (De et al. 2011) for distance bounding technology.
We present the protocol from the granted patent (Janssens 2017) in Figure 3. As with any protocol on top of ISO/IEC 14443, the session starts with the reader sending a *SELECT* command to the card and the card responding with its ID. The distance bounding check will be initialised by sending a *PREPARE PROXIMITY CHECK* command. The card generates a random 8-byte number $n_P$ and sends timing information to the reader indicating how long a reply to the distance bounding check should take. After receiving the timing information the reader generates its own random 8-byte number ($n_V$), sends this to the card using a *PROXIMITY CHECK* command and starts its timer.
In reply to the *PROXIMITY CHECK* command the card sends its own random number and on receiving this the reader stops its timer and checks the time against the timing information previously sent by the card. These steps can send the whole 8-byte nonces in one message, or the nonces can be split into up to eight exchanges of 1 byte each, so giving multiple time measurements.
Finally, the reader sends a *VERIFY PROXIMITY CHECK* with a MAC of the nonces and the timing information. The card checks whether the nonces and timing information are correct, and if so the card replies with a MAC of its own, again including the nonces and timing information. The card and readers MAC are distinguished by the inclusion of a different constant in each. The reader checks the card’s MAC, and if it is correct it verifies the card as being at the same location.
[msc diagram omitted]
NXP’s patented distance bounding protocol. The timed step can be repeated up to 8 times
NXP’s other patent application (De et al. 2011) presents the same protocol but without the timing information (we refer to this as NXP’s variant 1 below). It also presents a variant of the protocol in which the reader does not include a MAC with the *PROXIMITY CHECK* command (we refer to this as NXP’s variant 2 below). Similar protocols are claimed which use encryption rather than MACs. It is not specified whether there is a unique key per card, or a global key that is shared between many cards.
**Checking prover provided timing information:** In the protocols above the prover sends the verifier information about how long responses should take. When testing security properties for these protocols we also need to ensure that the timing information is correctly authenticated.
The authentication for the timing information should be independent of how the information is used, or the location of the processes, therefore we may reasonably over-approximate the correctness of the timing information by removing the timer actions and running all processes in parallel in the applied pi-calculus, along with any required dishonest provers. The ProVerif tool lets us check the authenticity of information by checking correspondences between events. For protocols that strongly authenticate the prover’s identity we check the authenticity of the timing information by adding an $\textnormal{event}(start(ti,id))$ to the start of the prover being tested, where $it$ is a name representing the timing information, and $id$ is the identity of the prover. We add an $\textnormal{event}(end(ti,id))$ to the verifier at the point it accepts the timing information as valid for prover $id$. For protocols that are anonymous, or do not authenticate the prover’s identity, we replace the $id$ in the event with the session nonces. We check that every end event has a corresponding start event, i.e., the verifier only accepts timing information as valid for a prover if the prover also performed a session with that timing information.
**Analysis and results:** We modelled MasterCard’s RRP, PaySafe, NXP’s protocols and several protocols from the literature as well as our example protocols in our calculus. Using our tool we compiled these to the applied pi-calculus with phases, and analyzed the resulting models with ProVerif. Table 1 summarizes the results of our analysis for the different protocols and attack scenarios. The compiled models can be significantly larger, as they scale linearly with the number of input operations. For example, the PayWave model becomes about 4 times longer than the original model when checking it for mafia fraud. For the results in Table 1, the verification with ProVerif finishes within a second on a system with an Intel Core i7-4550U and 8GB of RAM. For the protocols from the literature we used similar abstractions to model these as used in (Sjouke Mauw et al. 2018) and (Debant, Delaune, and Wiedling 2018). All models are available online. For the protocols from the literature (Gildas Avoine and Tchamkerten 2009; Hancke and Kuhn 2005; S. Mauw, Toro-Pozo, and Trujillo-Rasua 2016; Meadows et al. 2007; Rasmussen and Čapkun 2010; Trujillo-Rasua, Martin, and Avoine 2010; Čapkun, Buttyán, and Hubaux 2003) our analysis did not find any new results, so we focus on the industrial protocols.
We found that all the payment protocols protect against relay attacks and are safe in the uncompromised distance bounding scenario. It follows that your bank card is safe from relay attacks, even if someone else’s card is compromised. PaySafe and MasterCard’s RRP protocol do not defend against distance fraud, but Mauw et al.’s extension does. However, as noted above, distance fraud attacks are not applicable to protocols using ISO/IEC 14443, as it is always required to have a local adversary in order to communicate with the payment terminal. All of the protocols fail to protect against terrorist fraud attacks but, as discussed, we do not consider these applicable to the EMV attacker model. Therefore, we can conclude that all of the payment protocols meet their security goals with regard to relay attacks.
NXP’s protocols with a unique key for every device provide the same security against relay attacks as MasterCard’s RRP and PaySafe. Here we again consider both distance and terrorist fraud attacks not applicable due to the underlying ISO/IEC 14443 protocol. However, if we assume that a global key is shared across a range of devices then security against relay attacks holds, but uncompromised distance bounding security does not. This is due to the fact that the compromise of one device is equal to the compromise of the complete system. This would represent a major security risk with, for example, a single compromised key fob putting all cars at risk.
The only property that can distinguish the case where one compromised device leads either to an attack only on this one device or to the compromise of the complete system, is our proposed uncompromised distance bounding property. None of the properties suggested in previous papers can detect the difference between a global and unique key used in the NXP protocol, so highlighting the need for our work.
Regarding the authentication of timing information, our analysis shows that MasterCard’s RRP, PaySafe and NXP’s protocols with unique keys correctly bind the identity to the timing information. As NXP’s protocol with a global key does not authenticate the identity, we check the timing information against the session nonces, and find that it correctly binds these. Therefore, for these protocols, attacks aimed at the timing information will not work.
Results of our verification. The last four protocols use the same underlying distance bounding method.
Hancke and Kuhn (Hancke and Kuhn 2005)
Poulidor (Trujillo-Rasua, Martin, and Avoine 2010)
Tree-based (Gildas Avoine and Tchamkerten 2009)
Uniform (S. Mauw, Toro-Pozo, and Trujillo-Rasua 2016)
& OK & OK & OK & OK & N/A
Results of our verification. The last four protocols use the same underlying distance bounding method.
# Conclusion
We have presented an applied pi-calculus based modelling framework for distance bounding protocols and attacks. We built a hierarchy of distance bounding attack scenarios, and we have identified a new scenario for protocols that do not aim to protect against a compromised prover. We have defined a compiler from our calculus to the applied pi-calculus and use this compiler to analyse several distance bounding protocols, including protocols by MasterCard and NXP. We have also shown how the timing profiles used in these protocols can be verified.
#### Acknowledgements
This work has been supported by the Netherlands Organisation for Scientific Research (NWO) through Veni project 639.021.750. We would like to thank Ioana Boureanu and Sjouke Mauw for useful comments on a draft of this paper.
# References
Abadi, Martı́n, Bruno Blanchet, and Cédric Fournet. 2017. “The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication.” *JACM* 65 (1).
Abadi, Martı́n, and Cédric Fournet. 2001. “Mobile Values, New Names, and Secure Communication.” In *POPL’01*.
Avoine, G, MA Bingol, Ioana Boureanu, S Capkun, G Hancke, S Kardas, CH Kim, et al. 2017. “Security of Distance-Bounding: A Survey.” *CSUR* 4.
Avoine, Gildas, Muhammed Ali Bingöl, Süleyman Kardaş, Cédric Lauradoux, and Benjamin Martin. 2011. “A Framework for Analyzing RFID Distance Bounding Protocols.” *JCS* 19 (2).
Avoine, Gildas, and Aslan Tchamkerten. 2009. “An Efficient Distance Bounding RFID Authentication Protocol: Balancing False-Acceptance Rate and Memory Requirement.” In *ISC’09*.
BBC. n.d. “Car Theft ’Relay’ Devices Seized in Birmingham.” .
Blanchet, Bruno, Martı́n Abadi, and Cédric Fournet. 2008. “Automated Verification of Selected Equivalences for Security Protocols.” *JLAP*.
Blanchet, Bruno, Ben Smyth, Vincent Cheval, and Marc Sylvestre. 2018. “ProVerif 2.00: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial.”
Boureanu, Ioana, Aikaterini Mitrokotsa, and Serge Vaudenay. 2015. “Practical and Provably Secure Distance-Bounding.” *JCS* 23 (2).
Boureanu, Ioana, and Serge Vaudenay. 2015. “Optimal Proximity Proofs.” In *Inscrypt’14*. Vol. 8957. LNCS.
Brands, Stefan, and David Chaum. 1994. “Distance-Bounding Protocols.” In *EUROCRYPT’93*.
Čapkun, Srdjan, Levente Buttyán, and Jean-Pierre Hubaux. 2003. “SECTOR: Secure Tracking of Node Encounters in Multi-Hop Wireless Networks.” In *SASN’03*.
Chothia, Tom, Flavio D. Garcia, Joeri de Ruiter, Jordi van den Breekel, and Matthew Thompson. 2015. “Relay Cost Bounding for Contactless EMV Payments.” In *FC’15*. Vol. 8975. LNCS.
Cremers, Cas J. F., Kasper Bonne Rasmussen, Benedikt Schmidt, and Srdjan Capkun. 2012. “Distance Hijacking Attacks on Distance Bounding Protocols.” In *S&p’12*. IEEE.
De, J. H., P. Hubmer, B. Murray, H. Neumann, S. Stern, and P. Thueringer. 2011. “Decoupling of Measuring the Response Time of a Transponder and Its Authentication.”
Debant, Alexandre, Stéphanie Delaune, and Cyrille Wiedling. 2018. “Proving physical proximity using symbolic models.” Research Report. Univ Rennes, CNRS, IRISA, France. .
Desmedt, Yvo. 1988. “Major Security Problems with the ’Unforgeable’ (Feige)-Fiat-Shamir Proofs of Identity and How to Overcome Them.” In *SECURICOM*.
Desmedt, Yvo, Claude Goutier, and Samy Bengio. 1987. “Special Uses and Abuses of the Fiat-Shamir Passport Protocol.” In *CRYPTO*. Vol. 293. LNCS.
Dürholz, Ulrich, Marc Fischlin, Michael Kasper, and Cristina Onete. 2011. “A Formal Approach to Distance-Bounding RFID Protocols.” In *ISC’11*.
EMVCo. 2011. “EMV – Integrated Circuit Card Specifications for Payment Systems, Version 4.3.”
———. 2016. “EMV Contactless Specifications for Payment Systems, Version 2.6.”
Francillon, Aurélien, Boris Danev, and Srdjan Capkun. 2011. “Relay Attacks on Passive Keyless Entry and Start Systems in Modern Cars.” In *NDSS’11*.
Garcia, Flavio D., David Oswald, Timo Kasper, and Pierre Pavlidès. 2016. “Lock It and Still Lose It on the (in)security of Automotive Remote Keyless Entry Systems.” In *USENIX Security’16*. USENIX. .
Hancke, Gerhard, and Markus Kuhn. 2005. “An RFID Distance Bounding Protocol.” In *SecureComm’05*, 67–73. IEEE.
Janssens, P. 2017. “Proximity Check for Communication Devices.”
Kanovich, Max, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov, and Carolyn Talcott. 2014. “Towards Timed Models for Cyber-Physical Security Protocols.” In *FCS-FCC’14*.
Malladi, Sreekanth, Bezawada Bruhadeshwar, and Kishore Kothapalli. 2010. “Automatic Analysis of Distance Bounding Protocols.” *CoRR* abs/1003.5383.
Mauw, Sjouke, Zach Smith, Jorge Toro-Pozo, and Rolando Trujillo-Rasua. 2018. “Distance-Bounding Protocols: Verification Without Time and Location.” In *S&p’14*.
Mauw, S., J. Toro-Pozo, and R. Trujillo-Rasua. 2016. “A Class of Precomputation-Based Distance-Bounding Protocols.” In *EuroS&p’16*.
Meadows, Catherine A., Radha Poovendran, Dusko Pavlovic, LiWu Chang, and Paul F. Syverson. 2007. “Distance Bounding Protocols: Authentication Logic Analysis and Collusion Attacks.” In *Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks*.
Nigam, Vivek, Carolyn Talcott, and Abraão Aires Urquiza. 2016. “Towards the Automated Verification of Cyber-Physical Security Protocols: Bounding the Number of Timed Intruders.” In *ESORICS’16*.
Rasmussen, Kasper Bonne, and Srdjan Čapkun. 2010. “Realization of RF Distance Bounding.” In *USENIX Security’10*.
Ryan, Mark D., and Ben Smyth. 2011. “Applied pi calculus.” In *Formal Models and Techniques for Analyzing Security Protocols*. IOS.
Schaller, Patrick, Benedikt Schmidt, David Basin, and Srdjan Capkun. 2009. “Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks.” In *CSF’09*.
Trujillo-Rasua, Rolando, Benjamin Martin, and Gildas Avoine. 2010. “The Poulidor Distance-Bounding Protocol.” In *RFIDSec’10*.