Security Aspects of Distance-Bounding Protocols
Maria Cristina Onete · Technischen Universität Darmstadt · 2012
Authentication protocols, run between a so-called prover and a so-called verifier, enable the verifier to decide whether a prover is legitimate or not. Such protocols enable access control, and are used in e.g.~logistics, public transport, or personal identification. An authentication protocol is considered secure if an adversary cannot impersonate a legitimate prover. Such an adversary may eavesdrop authentication attempts between a legitimate prover and a legitimate verifier, interact with either of the two honest parties, or perform a man-in-the-middle (MITM) attack, but without purely relaying messages between the honest parties (see Figure~\ref{fig:models} (a)). Distance-bounding is a feature that enables authentication protocols to also withstand MITM \emph{relay attacks}, where an adversary forwards information between the prover and verifier such that neither honest party is aware of the attack. The goal of the adversary is to be authenticated by the verifier as a legitimate prover. In practice, the adversary consists of two parties, a \emph{leech}, which impersonates the verifier to the prover, and a \emph{ghost}, which impersonates the prover to the verifier. This is also depicted in Figure~\ref{fig:models}. Following the initial paper by Desmedt~\cite{Des88}, pure relay attacks are called \emph{mafia fraud}. \begin{figure}[H] \centering \includegraphics[height=5.0cm]{Presentation2.pdf} \caption{Adversary models in (a) authentication and (b) mafia fraud.} \label{fig:models} \end{figure} In distance-bounding protocols, introduced by Brands and Chaum in 1993 \cite{BrandsChaum93}, a clock is mounted on the verifier, such that it can measure the time-of-flight between sending a challenge and receiving a response. Following the idea that pure relay introduces a processing delay in the MITM adversary, a verifier now compares the measured time-of-flight with a pre-set value \tmax\ (in practice, an upper bound associated with the maximum trusted communication distance). If the communication speed is constant (and very fast), the verifier authenticates the prover if (i) the verifier is convinced that the prover is legitimate, and (ii) the prover is within the maximum distance associated with \tmax. Such protocols were recently implemented by Rasmussen and \Capkun~\cite{Rasmussen2010} and Ranganathan et al.~\cite{Ranganathan2012}. In most distance-bounding protocols in the literature, the prover-verifier communication is run in multiple rounds, or \emph{phases}, which are classified as either \emph{time-critical} if the verifier's clock measures the roundtrip time, or \emph{lazy} if the clock is not used. Note, however, that e.g.~the protocol due to Rasmussen and \Capkun~\cite{RC07} is not round-based. There are three classical attacks that distance-bounding protocols should in general address: \begin{enumerate} \item \textbf{Mafia Fraud:} Here, an adversary attempts to authenticate to the verifier in the presence of an honest prover (however, the verifier's clock prevents pure relay). Both honest parties are unaware of the attack. \item \textbf{Terrorist Fraud:} Here the dishonest prover provides some limited help to the adversary, such that the adversary is able to authenticate to the honest verifier. However, the prover should not forward any information that allows the adversary to authenticate without the prover's help. Intuitively, a terrorist fraud attack is successful if the adversary is successful in authenticating with the prover's help, but not without it. \item \textbf{Distance Fraud:} The adversary in this scenario is a dishonest prover placed far from the verifier (i.e.~outside the range associated with \tmax). The goal of the adversary is to authenticate, thus fooling the verifier's clock. \end{enumerate} A fourth security notion (suggested much later by Avoine and Tchamkerten \cite{AvTcham09}) is that of classical impersonation security, where the adversary interacts with either the prover or the verifier (but not in a MITM attack) and wins if it authenticates successfully. This attack is particularly dangerous for implementations on resource-constrained devices, e.g. RFID tags, where the provers (tags) only support a small number of time-critical rounds. Thus, the mafia fraud resistance of the protocol (which hinges on the number of time-critical rounds) is very low. The main contribution of this thesis is to introduce a unitary, three-layered, formal framework for proving security of distance-bounding protocols. The main layer of this model is the central layer and captures a static model, where the prover and verifier share a secret key, which is never updated. In this context, we define the fundamental threats to distance-bounding protocols, namely: mafia, terrorist, and distance fraud, and impersonation security. Additionally, we take a closer look at mafia and terrorist fraud resistance, extending mafia fraud to capture prover aborts, and describing three flavours of terrorist fraud resistance, depending on how much information a dishonest prover is willing to pass to the adversary. The two remaining layers of our model discuss privacy aspects of distance-bounding protocols: in our top layer we include location privacy, whereas our bottom layer concerns privacy in authentication. A second very important contribution is to describe two constructions: the first provable-secure terrorist fraud resistant, and the first provably location-private distance-bounding protocol in the literature (see more details below). Also very important are the three compilers we describe, which enable black-box transformations from either one tier of the main framework to another, or from one degree of mafia fraud resistance to another. More concretely, we proceed in the following directions. \paragraph{Fundamental Model.} The central, fundamental layer of this framework includes the four standard attacks enumerated above, extending and formalizing previous work due to Avoine et al. \cite{AvoBinKarLauMar09}. The models account for exact bounds for the levels of mafia, terrorist, and distance fraud resistance, and for impersonation security of any round-based distance-bounding protocol; having compared the notions, we prove them to be independent, contrary to popular belief and to the results of \cite{AvoBinKarLauMar09}. As this is the fundamental layer of our model, we consider it paramount to assess the security properties of several distance-bounding protocols in the literature. We choose the more prominent schemes of Brands and Chaum~\cite{BrandsChaum93}, Hancke and Kuhn~\cite{HanKuhn05}, Avoine and Tchamkerten~\cite{AvTcham09}, Kim and Avoine~\cite{KimAvo09}, Reid et al.~\cite{ReidGonzTangSen07}, Bussard and Bagga~\cite{BusBagga05}, and the Swiss-Knife protocol due to Kim et al.~\cite{KimAvoKoeStaPer09}. In so doing we give a generic attack against the terrorist fraud resistance of the schemes in~\cite{BusBagga05,KimAvoKoeStaPer09,ReidGonzTangSen07}, showing that they attain a different, in many ways more relaxed notion of terrorist fraud resistance. The central layer of our model considers static keys only. However, we extend this scenario to also include privacy aspects, both in authentication (the bottom layer of our model) and with respect to the prover's location (the upper layer of the model). Here, we define privacy in authentication in the sense of Vaudenay~\cite{Vau07}, i.e.~distance-bounding sessions should be unlinkable. The adversary in this scenario is also allowed to corrupt provers and learn their internal states (i.e.~the secret key); depending on the adversary strength, the adversary may then be able to interact with other provers or not. If the adversary is unable to learn the result of an authentication protocol between a prover and the verifier, we speak of \emph{narrow} privacy; else, we speak of \emph{wide} privacy. Though Vaudenay's model is well studied for RFID authentication, it has not been applied to distance-bounding. In order to achieve privacy, we extend the fundamental, static model in our central layer to account for key updates, such that the prover and verifier use different keys to generate their responses during each protocol run. We also give compilers which preserve the static-key model properties of a scheme (i.e. their levels of mafia and distance fraud resistance, and impersonation security) in the key-update model, furthermore transforming narrow-weak private distance-bounding protocols (in the sense of \cite{Vau07}) into narrow-destructive private schemes. Recall that narrow privacy refers to the fact that the adversary does not learn the verifier output for protocol runs. Note that in the symmetric-key scenario this is the most one can achieve, since \cite{Vau07} proves that narrow-strong privacy requires key agreement. In our compiler, the prover updates state early, after an initial lazy authentication phase, whereas the verifier updates state only after authenticating the prover. Furthermore, the verifier can ``catch up'' with the prover by means of an initial state-recognition phase. However, in order to ensure that the verifier does not enter an infinite iterative process, resulting in a denial of service (DoS) attack, we split the prover state into two parts, one which is updated at each authentication attempt, and another which is only updated upon verifier authentication. This latter state fragment then enables the verifier to bypass DoS attacks. The upper layer of our model, location privacy, was already addressed in the literature by Rasmussen and \Capkun~\cite{RC07}. However, they did not formally define their security model and in fact, we can prove that their proposed scheme is \emph{not} location private in our definition. Note that, as opposed to authentication, where location privacy is generally used to mean that no location data is leaked by provers in authentication sessions, in distance bounding provers necessarily leak one piece of informati