TU Darmstadt / ULB / TUprints

Security Aspects of Distance-Bounding Protocols

Onete, Maria Cristina :
Security Aspects of Distance-Bounding Protocols.
Technische Universität, Darmstadt
[Ph.D. Thesis], (2012)

Available under Creative Commons Attribution Non-commercial No Derivatives, 2.5.

Download (1MB) | Preview
Item Type: Ph.D. Thesis
Title: Security Aspects of Distance-Bounding Protocols
Language: English

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 information, namely whether they are in the verifier's proximity or not. For location privacy we require that no further information can be leaked from provers which are within proximity of the verifier. We show an impossibility result: namely that location privacy cannot be achieved in an information-theoretical sense, and furthermore it cannot even be computationally attained for strong adversaries, which are in practice able to triangulate signals and gauge signal strength. We also show how to achieve location privacy in a weaker model, at the cost of a larger communication complexity; in particular, our construction is a modification of the construction in \cite{RC07}.

We stress that we view distance bounding as an extension of authentication. In particular, we consider mafia and distance fraud resistance (as well as impersonation security) to be basic requirements of distance-bounding protocols. This contradicts the idea used by Rasmussen and \Capkun\ in their construction~\cite{RC07}: indeed, their protocol only attains distance fraud resistance. Our location private protocol in fact makes a modification in the original scheme in~\cite{RC07}, so as to thwart a mafia fraud attack against this scheme. We also describe this attack.

\paragraph{Mafia and Terrorist Fraud.} Having completed the three-tiered description of our model, we also look more in depth at mafia and terrorist fraud resistance. We show that, unlike previous frameworks, our model also captures so-called key-learning attacks, where the adversary interferes in a few time-critical rounds of otherwise honest prover-verifier communication, with the goal of learning some bits of the secret key. Such attacks are known for authentication, but they have never been considered in the distance-bounding setting. We also model an extension of key-learning attacks, which could appear in practice in the case of prover aborts. For the latter notion of terrorist fraud resistance we elaborate on our previous definition of terrorist fraud resistance. We explain that though most protocols in the literature do not attain this strong, simulation-based notion, our notion \emph{can} be achieved (and we describe a protocol that achieves it). We also define a game-based flavour of terrorist fraud resistance, which is the one most commonly achieved by protocols in the literature. The difference between the notions is roughly this. In our simulation-based model the prover may leak some information about his secret key to the adversary, as long as this information does not enable a simulator to authenticate \emph{with equal probability} in the future. In practice, the prover can then choose to leak only very little information about the secret key, thus ensuring that (i) the adversary does authenticate while the prover helps, and (ii) once the prover stops helping, the adversary's probability to succeed drops. By contrast, in the game-based mode, the prover is unwilling to leak \emph{any} information to the adversary: thus, the adversary is far more limited.

More in detail, for the topic of mafia fraud resistance, our model extends previous mafia fraud models to account for key-learning attacks as outlined above. Such attacks are particularly useful against protocols aiming to achieve terrorist fraud resistance. We also introduce an extension to the mafia fraud definition (called strong mafia fraud \strMaf) to account for adversaries that can hijack honest authentication sessions and thus authenticate from an aborting prover. We also show that \strMaf\ security is strictly stronger than mafia fraud resistance.

We also note that the simulation-based model of terrorist fraud resistance \ourSim\ is, on the one hand, very strong (in fact we prove that some prominent schemes in the literature addressing this attack are insecure in our framework). On the other hand, however, this model does not cover all adversarial capabilities (since the prover only interacts with the adversary offline). Thus, we introduce both a stronger simulation-based notion \strSim\ and a more relaxed, game-based notion \gameTF\ security. The former extension provides an even higher degree of security, whereas the latter allows for more efficient constructions (while at the same time eliminating obvious attacks). We prove the well-known construction of Bussard and Bagga \cite{BusBagga05}, which is \ourSim\ \emph{in}secure, to be \gameTF\ secure. In fact, most protocols in the literature claiming to achieve terrorist fraud resistance, are actually \gameTF\ secure, and not \ourSim\ secure. We argue that whereas the \gameTF\ notion seems to achieve a minimal degree of terrorist fraud resistance, it is very restrictive and may enable attacks, particularly in scenarios where the dishonest prover is prepared to yield a few bits of the secret key if the result is that the adversary can then authenticate.

\paragraph{Constructions and Compilers.} As far as constructions are concerned, we (i) show the first provably secure \ourSim-secure protocol, and show that it is also \strSim-secure, and (ii) we design the first provably-secure location private protocol in the literature. Furthermore, we show compilers to turn mafia fraud resistant schemes into \strMaf\ secure constructions. Moreover, our compiler also works if the underlying protocol need not be fully maifa fraud resistant, but could be susceptible to key-learning attacks (which is a particular form of mafia fraud). This compiler uses a final lazy authentication step, which prevents adversaries from hijacking aborted prover-verifier sessions. Both compilers can be run, with several optimizations, on most distance-bounding constructions in the literature. We furthermore show several other handy tricks, both in the modelling department (where we show how to prove various notions in our model) and for construction purposes (we show how to easily achieve impersonation security and how mutual authentication can be used towards delegating some computational burden on the verifier).

Future topics include (i) modelling extended scenarios for distance-bounding protocols, with multiple provers and a single verifier, or multiple provers and multiple verifiers, formalizing previous work by \Capkun\ et al. \cite{CapDefTsu11}; (ii) investigating how far ou

Alternative Abstract:
Alternative AbstractLanguage
Protokolle zur Authentisierung sind Protokolle mit 2 Teilnehmern, einem sogenannten ``Prover'', dem Beweiser, der sich authentisieren will, und dem Verifizierer, der die Authentizit{\"{a}}t des Provers feststellen m{\"{o}}chte. Protokolle dieser Art sind ein elektronisches Mittel der Zugangsbeschr{\"{a}}nkung und finden zum Beispiel Anwendung in Logistik, {\"{o}}ffentlichem Nahverkehr oder pers{\"{o}}nlicher Identifikation. Ein Authentisierungsprotokoll nennen wir sicher, wenn ein Angreifer sich nicht als legitimer Prover ausgeben kann. Ein solcher Angreifer darf zu diesem Zweck Authentisierungsprotokolle des Provers beobachten und mit einem oder beiden interagieren, einen Man-In-The-Middle (MITM)-Angriff ausf{\"{u}}hren, allerdings ohne dass er ausschlie{\ss}lich Nachrichten zwischen dem Prover und dem Verifizierer weiterleitet (siehe auch Abbildung~\ref{fig:models} (a)). Distance-bounding (Abstandsbeschr{\"{a}}nkung, -approximierung) ist eine Eigenschaft von Authentisierungsprotokollen, die dar{\"{u}}ber hinaus MITM-Angriffe verhindert, bei denen nur Nachrichten zwischen dem Prover und dem Verifizierer weitergeleitet werden, ohne dass der Prover oder der Verifizierer den Angriff bemerken. Das Ziel des Angreifers ist es, sich gegen{\"{u}}ber dem Verifizierer als legitimer Prover auszugeben. Um diesen Angriff tats{\"{a}}chlich auszuf{\"{u}}hren, teilt sich der Angreifer in zwei Teilnehmer aus, einen sogenannten ``Leech'', der dem Prover gegen{\"{u}}ber die Rolle des Verifizierers einnimmt und einem ``Ghost'', der sich dem Verifizierer gegen{\"{u}}ber als Prover ausgibt, siehe Abbildung~\ref{fig:models}. Gem{\"{a}}{\ss} dem urspr{\"{u}}nglichen Artikel von Desmedt~\cite{Des88}, hei{\ss}en Angriffe, bei denen nur Nachrichten weitergeleitet werden, \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} Distance-Bounding-Protokolle wurden 1993 von Brands und Cham~\cite{BrandsChaum93} eingef{\"{u}}hrt, indem der Verifizierer eine Uhr implementiert, sodass er den Zeitabstand zwischen dem Senden einer Challenge und dem Empfangen einer Antwort messen kann. Dadurch, dass reines Weiterleiten durch den MITM-Angreifer eine Verz{\"{o}}gerung verursacht, kann der Verifier nun den tats{\"{a}}chlichen mit dem erwarteten Zeitabstand \tmax\ vergleichen (Diese obere Schranke \tmax\ f{\"{u}}r den Zeitabstand entspricht dem gr{\"{o}}{\ss}tm{\"{o}}glichen, erlaubten Abstand zwischen dem Prover und dem Verifizierer). Wenn Daten{\"{u}}bertragung constante Zeit ben{\"{o}}tigt (und sehr schnell ist), dann authentisiert der Verifizierer den Prover, sofern (i) der Verifier sich von der Legitimit{\"{a}}t des Provers {\"{u}}berzeugt hat, und (ii) der Prover sich innerhalb des mit \tmax\ assoziierten H{\"{o}}chstabstandes befindet. Derartige Distance-Bounding-Protokollen wurden k\"{u}rzlich von Rasmussen und \Capkun~\cite{Rasmussen2010} und Ranganathan et al.~\cite{Ranganathan2012} implementiert. Die meisten existierenden Distance-Bounding-Protokolle f{\"{u}}hren die Prover-Verifizierer-Kommunikation in mehreren Runden aus, oder Phase, die entweder als \emph{zeitkritisch} bezeichnet werden, wenn der Verifizierer die Gesamtzeit der Protokollausf{\"{u}}hrung misst, oder \emph{lazy}, wenn der Verifizierer seine Uhr nicht verwendet. Es gibt aber auch Protokolle, die nicht rundenbasiert sind. Hier ist zum Beispiel das Protokoll von Rasmussen and \Capkun~\cite{RC07} zu nennen. Es gibt drei klassische Angriffe, die Distance-Bounding-Protokolle im Allgemeinen abdecken sollen: \begin{enumerate} \item \textbf{Mafia Fraud:} Hier versucht der Angreifer, sich dem Verifizierer gegen{\"{u}}ber in der Anwesenheit des Provers zu legitimieren (Allerdings verhindert die Uhr des Verifizierers reine Weiterleitungsangriffe). Beide Teilnehmer, der Prover und der Verifizierer, sind sich des Angriffes nicht bewusst. \item \textbf{Terrorist Fraud:} Hier unterst{\"{u}}tzt der unehrliche Prover den Angreifer auf beschr{\"{a}}nkte Weise, sodass der Angreifer sich dem Verifizierer gegen{\"{u}}ber authentisieren kann. Die Hilfe des Provers ist allerdings insofern beschr{\"{a}}nkt, als dass er dem Angreifer keine Informationen zur Verf{\"{u}}gung stellt, die es ihm erm{\"{o}}glicht, sich anschlie{\ss}end auch ohne weitere Hilfe des Provers dem Verifizierer gegen{\"{u}}ber zu authentifizieren. Intuitiv ist ein Terrorist Fraud Angriff dann erfolgreich, wenn der Angreifer sich mithilfe des Provers authentisieren kann, aber nicht ohne dessen Hilfe. \item \textbf{Distance Fraud:} In diesem Angriffsszenario ist der Angreifer ein unehrlich Prover, der vom Verifizierer weit entfernt befindet (das hei{\ss}t, au{\ss}erhalb des mit \tmax assoziierten Abstandes). Das Ziel des Angreifers ist es, sich zu authetisieren und die Uhr des Verifizierers zu t{\"{a}}uschen. \end{enumerate} Ein vierter Sicherheitsbegriff, der sehr viel sp{\"{a}}ter von Avoine und Tchamkerten \cite{AvTcham09} eingef{\"{u}}hrt wurde, ist der Angriff klassischer Impersonifizierungssicherheit, wo der Angreifer entweder mit dem Prover oder mit dem Verifizierer interagiert (aber nicht in einem MITM Angriff) und gewinnt, wenn er sich erfolgreich authentifiziert. Dieser Angriff ist besonders gef{\"{a}}hrlich f{\"{u}}r Implementierungen auf Ressource-beschr{\"{a}}nkten Ger{\"{a}}ten, z.B. RFID Tags, bei denen der Prover (Tag) nur eine kleine Anzahl zeitkritischer Runden unterst{\"{u}}tzt. Daher ist die Resistenz des Protokolls gegen Mafia Fraud Angriffe (die von der Anzahl der zeitkritischen Runden abh{\"{a}}ngt) sehr niedrig. Der wichtigste Beitrag dieser Arbeit ist die Einf{\"{u}}hrung eines unit{\"{a}}ren, dreischichtigen, formalen Frameworks, um die Sicherheit von Distance-Bounding-Protokollen zu beweisen. Die wichtigste Schicht dieses Frameworks ist die mittige Schicht, die ein statisches Modell beschreibt, in welchem der Prover und der Verifizierer einen gemeinsamen, geheimen Schl{\"{u}}ssel teilen, der nicht aktualisiert wird. Vor diesem Hintergrund definieren wir die fundamentalen Angriffe gegen Distance-Bounding-Protokolle, n{\"{a}}mlich: Mafia, Terrorist und Distance Fraud, und Impersonifizierungssicherheit. Dar{\"{u}}ber hinaus verfeinern wir die Definition der Resistenz gegen Mafia und Terrorist Fraud, in dem wir Mafia Fraud auf Angriffe ausweiten, bei dem der Angreifer eine Sitzung \"{u}bernimmt wo der Prover abgebrochen hat. Die zwei verbleibenden Schichten unseres Modells besch{\"{a}}ftigen sich mit Aspekten der Privatsph{\"{a}}re von Distance-Bounding-Protokollen: In unserer obersten Schicht betrachten wir die Geheimhaltung des Aufenthaltsortes, w{\"{a}}hrend unsere unterste Schicht sich mit der Geheimhaltung der Authentisierung selbst besch{\"{a}}ftigt. Ein weiterer, ebenfalls sehr wichtiger Beitrag ist die Beschreibung zweier Konstruktionen: Wir geben die erste Konstruktion f{\"{u}}r ein Protokoll, welches beweisbar sicher gegen Terrorist Fraud ist, und die erste Konstruktion, die beweisbar Geheimhaltung aller Informationen {\"{u}}ber Aufenthaltsort erh{\"{a}}lt (mehr Details weiter unten). Auch sehr wichtig sind die drei Compiler, die wir beschreiben, welche Black-Box-Transformationen von jeder der drei Schichten des Frameworks zu jeder anderen erreichen. Konkret sind unsere Beitr{\"{a}}ge wie folgt: \paragraph{Fundamentales Modell} Die mittlere, fundamentale Schicht dieses Frameworks deckt alle vier oben genannten Standardangriffe ab, was existierende Arbeit von Avoine et al~\cite{AvoBinKarLauMar09} erweitert und formalisiert. Die Modelle beinhalten exakte Schranken f{\"{u}}r den Grad der Resistenz gegen Mafia, Terrorist, und Distance Fraud sowie f{\"{u}}r Impersonifizierungssicherheit f{\"{u}}r beliebige rundenbasierte Protokolle; wir vergleichen die Sicherheitsbegriffe und zeigen, dass keine die andere impliziert. Dies steht im Gegensatz zu einer weit verbreiteten Ueberzeugung sowie der Arbeit \cite{AvoBinKarLauMar09}. Da dies die fundamentale Schicht unseres Modells ist, ist es von zentraler Bedeutung, die Sicherheit von existierenden Distance-Bounding-Protokollen in unserem Modell zu analysieren. Wir betrachten die promintenten Protokolle von Brands und Chaum~\cite{BrandsChaum93}, Hancke und Kuhn~\cite{HanKuhn05}, Avoine und Tchamkerten~\cite{AvTcham09}, Kim und Avoine~\cite{KimAvo09}, Reid et al.~\cite{ReidGonzTangSen07}, Bussard und Bagga~\cite{BusBagga05}, sowie das Schweizer-Messer-Protokoll von Kim et al.~\cite{KimAvoKoeStaPer09}. Hierbei zeigen wir einen generischen Angriff gegen die Resistenz gegen Terrorist Fraud der Protokolle in~\cite{BusBagga05,KimAvoKoeStaPer09,ReidGonzTangSen07}, wodurch wir zeigen, dass sie eine andere, in vielerlei Hinsicht schw{\"{a}}chere Variante von Resistenz gegen Terrorist Fraud erreichen. Die mittlere Schicht unseres Models betrachtet nur statische Schl{\"{u}}ssel. Dahingegen erweitern wir das Angriffsszenario, um auch Aspekte der Privatsph{\"{a}}re miteinzuschlie{\ss}en, sowohl bez{\"{u}}glich Authentisierung (in der unteren Schicht unseres Modells) als auch bez{\"{u}}glich des Aufenthaltsortes des Provers (obere Schicht unseres Modells). Hier definieren wir Geheimhaltung der Authentisierung im Sinne von Vaudenay~\cite{Vau07}, das hei{\ss}t, verschiedene Distance-Bounding-Sitzungen sollen nicht in Verbindung gebracht werden k{\"{o}}nnen, also ``unlinkable'' sein. Der Angreifer in diesem Angriffsszenario darf Prover korrumpieren und ihren internen Zustand erfahren (das hei{\ss}t, den secret key); anh{\"{a}}ngig von der St{\"{a}}rke des Angreifers kann der Angreifer zus{\"{a}}tzlich mit anderen Provern interagiern, oder auch nicht. Wenn der Angreifer das Ergebnis eines Authentisierungsprotokolls zwischen einem Prover und einem Verifizierer nicht bestimmen kann, sprechen wir von \emph{narrow privacy}; ansonsten bezeichnen wir die Eigenschaft als \emph{wide privacy}. Vaudenays Modell ist gut erforscht bez{\"{u}}glich RFID Authentisierung, wohingegen es bislang nicht auf Distance-Bounding angewandt wurde. Um Privacy zu erreichen, erweitern wir das fundamentale, statische Modell der mittleren Schicht, um auch Schl{\"{u}}sselaktualisierungen abzudecken, sodass der Prover und der Verifizierer verschiedene Schl{\"{u}}ssel pro Protokollausf{\"{u}}hrung verwenden k{\"{o}}nnen. Dar{\"{u}}ber hinaus konstruieren wir Compiler, die die Sicherheitseigenschaften des statischen Modells (also den Grad ihrer Resistenz gegen Mafia und Distance Fraud, und Impersonifizierungssicherheit) auch bei Schl{\"{u}}sselaktualisierungen erhalten. Dar{\"{u}}ber hinaus transformieren sie Distance-Bounding-Protokolle, die narrow-weak private sind (im Sinne von \cite{Vau07}) in Protokolle, welche narrow-destructive private sind. Wir erinnern uns daran, dass narrow privacy die Eigenschaft beschreibt, dass der Angreifer das Ergebnis von Protokollausf{\"{u}}hrungen nicht erf{\"{a}}hrt. F{\"{u}}r Verfahren mit symmetrischen Schl{\"{u}}sseln ist dies die st{\"{a}}rkste Eigenschaft, die erreicht werden kann, da \cite{Vau07} zeigt, dass narrow-strong privacy einen sicheren Schl{\"{u}}sselaustausch bedingt. In unserem compiler aktualisiert der Prover seinen Zustand fr{\"{u}}hzeitig, nach der unitialen lazy Authentisierungsphase, wohingegen der Verifizierer seinen Zustand er nach der Authentisierung des Provers aktualisiert. Dar{\"{u}}ber hinaus kann der Verifizierer den Prover ``einholen'', indem man zu Beginn eine Phase der Zustandserkennung ausf{\"{u}}hrt. Um allerdings sicherzustellen, dass der Verifizierer nicht keine unendliche iterativen Schleife beginnt, sodass man einen ``Denial of Service'' (DoS) Angriff durchf{\"{u}}hren kann, teilen wir den Zustand des Provers in zwei Teile: Einen, der bei jedem Authentisierungsversucht aktualisiert wird und einen anderen, der nur aktualisiert wird wenn die Authentisierung erfolgreich ist. Das letztere Fragment des Zustandes erm{\"{o}}glicht dem Verifizierer, einen DoS-Angriff abzuwehren. Die obere Schicht unseres Modells, Geheimhaltung des Aufenthaltsortes, wurde bereits von Rasmussen und \Capkun~\cite{RC07} betrachtet. Allerdings formulierten sie ihr Sicherheitsmodell nicht formal, sodass wir sogar zeigen k{\"{o}}nnen, dass das von ihnen vorgeschlagene Protokol \emph{nicht} Geheimhaltung des Aufenthaltsortes erreicht. Man sollte beachten, dass bei Distance-Bounding im Gegensatz zu Authentisierung, wo Geheimhaltung des Aufenthaltsortes im Allgemeinen verwendet wird, um zu sagen, dass keine Informationen {\"{u}}ber den Aufenthaltsort preisgegeben werden, es so ist, dass Distance-Bounding notwenigerweise zumindest etwas Information {\"{u}}ber den Aufenthaltsort preisgibt, n{\"{a}}mlich, ob der Prover sich in der N{\"{a}}he befindet oder nicht. F{\"{u}}r die Geheimhaltung des Aufenthaltsortes im Zusammenhang mit Distance-Bounding ist die Bedingung, dass keine dar{\"{u}}ber hinausgehende Information preisgegeben wird. Wir zeigen ein Unm{\"{o}}glichkeitsresultat: Geheimhaltung des Aufenthaltsortes kann n{\"{a}}mlich nicht im informationstheoretischen Sinne erreicht werden, und dar{\"{u}}ber hinaus kann es auch im computational Sinne nicht erreicht werden, sofern der Angreifer stark ist, die Signale triangulieren und die Signalst{\"{a}}rke bestimmen k{\"{o}}nnen. Wir zeigen ebenfalls, wie Geheimhaltung des Aufenthaltsortes in einem schw{\"{a}}cheren Modell erreicht werden kann, wenn man bereit ist, die Kommunikationskomplexit{\"{a}}t zu erh{\"{o}}hen; insbesondere ist unserer Konstruktion eine Modifikation der Konstruktion aus\cite{RC07}. Wir wollen hervorheben, dass Distance-Bounding f{\"{u}}r uns eine Erweiterung von Authentisierung ist. Insbesondere betrachten wir Resistenz gegen Mafia und Distance Fraud (als auch Impersonifizierungssicherheit) als grundlegende Anforderungen an Distance-Bounding-Protokolle. Dies widerspricht der Idee von Rasmussen und \Capkun\ und ihrer Konstruktion~\cite{RC07}: Tats{\"{a}}chlich erreicht ihr Protokoll nur Resistenz gegen Distance-Fraud. Unser Protokoll f{\"{u}}r die Geheimhaltung des Aufenthaltsortes modifiziert also das urspr{\"{u}}ngliche Protokoll aus~\cite{RC07}, um einen Mafia Fraud Angriff auf dieses Protokoll auszuschlie{\ss}en. Wir beschreiben diesen Angriff. \paragraph{Mafia und Terrorist Fraud.} Nachdem wir unser dreischichtiges Modell vollst{\"{a}}ndig definiert haben, analysieren wir Mafia und Terrorist Fraud tiefergehend. Wir beweisen, dass unser Modell im Gegensatz zu vorherigen Modellen auch sogenannte key-learning (Schl{\"{u}}ssel-lernende) Angriffe abdeckt, bei denen der Angreifer aktive Angriffe auf die wenigen zeitkritischen Runden einer sonst ehrlichen Prover-Verifizierer-Sitzung ausfuehren darf. Das Ziel des Angreifers ist, einige wenige Bits des Schl{\"{u}}ssels zu lernen. Diese Art des Angriffs sind im Zusammenhang mit Authentisierung schon bekannt. Im Zusammenhang mit Distance-Bounding sind sie jedoch bislang nicht betrachtet worden. Wir modellieren eine erweiterte Variante von Key-Learning Angriffen, welche praktisch relevant sind im Falle, dass der Prover die Ausfuehrung des Protokolls vorzeitig beendet. In Bezug auf Resistenz gegen Terrorist Fraud erweitern wir unsere urspr{\"{u}}ngliche Definition von Resistenz gegen Terrorist Fraud. Wir zeigen, dass, obwohl die meisten Protokolle in der Literatur nicht resistet gegen Terrorist Fraud sind (bez{\"{u}}glich dieser simulationsbasierten Definition), es sehr wohl m{\"{o}}glich ist, Resistenz gegen Terrorist Fraud gem{\"{a}}{\ss} dieser Definition zu erreichen. Insbesondere geben wir ein Protokoll an, welches Resistenz gegen Terrorist Fraud erreicht. Dar{\"{u}}ber hinaus geben wir eine spielbasierte Definition f{\"{u}}r Resistenz gegen Terrorist Fraud an, welche von den meisten existierenden Protokollen erreicht wird. Im Gro{\ss}en und Ganzen kann man den Unterschied zwischen den beiden Definitionen wie folgt zusammenfassen. In userem Simulation-basierten Modell kann der Prover Informationen {\"{u}}ber seinen Schl{\"{u}}ssel an den Angreifer weitergeben, solange diese Informationen einem Simulator nicht helfen, mit gleicher Wahrscheinlichkeit in der Zukunft zu authentizieren. In der Praxis kann der Prover aber nur sehGerman
Place of Publication: Darmstadt
Classification DDC: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Divisions: 20 Department of Computer Science
Date Deposited: 17 Dec 2012 15:07
Last Modified: 28 Jun 2016 12:17
URN: urn:nbn:de:tuda-tuprints-30404
Referees: Fischlin, Prof. Dr. Marc and Katzenbeisser, Prof. Dr. Stefan
Refereed: 20 June 2012
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/3040
Actions (login required)
View Item View Item


Downloads per month over past year