FutureDB: A Cryptacus and Popstar workshop on distance-bounding

FutureDB’s goals is to progress the area of distance-bounding, by first understanding the gaps between theory and practice in this field, and then join the different efforts and ideas herein into a happy medium.

Invited talks

Title: Secure distance measurement - Physical layer and implementation issues.

Slides: Download Srdjan Čapkun's slides from the talk.

Abstract: In this talk we will review physical layer and implementation issues of secure distance measurement and distance-bounding systems. We will describe one secure physical layer design and demo a system that uses it.

Finally, we will discuss the implications of physical layer considerations and implementation constraints on some of the results in the distance-bounding community.

Title: Modelling and analysis of a hierarchy of distance-bounding attacks.

Slides: Download Tom Chothia's slides from the talk.

Abstract: We extend the applied pi-calculus so that it can be used to model distance-bounding protocols and we use this framework to model security properties and attacks from the literature.

None of the existing distance-bounding security properties matches the attacker model for protecting devices such as contactless payment or car entry systems, which assumes that the prover being tested has not been compromised but other prover's may have been.

We enumerate possible distance-bounding security properties, show a partial order on these, and relate them to particular attacker models. In doing so we identify a property we call “uncompromised distance bounding” that captures the attacker model we require.

We encode our locations into the applied pi-calculus so that protocols can be automatically checked in ProVerif and we use this to analyse distance-bounding protocols from MasterCard and NXP. (This is joint work with Joeri de Ruiter and Ben Smyth).

Title: Proving physical proximity using symbolic models.

Slides: Download Alexandre Debant's slides from the talk.

Abstract: For many modern applications like e.g contactless payment, and keyless systems, ensuring physical proximity is a security goal of paramount importance. Formal methods have proved their usefulness when analysing standard security protocols.

However, existing results and tools do not apply to e.g. distance-bounding that aims to ensure physical proximity between two entities. This is due in particular to the fact that existing models do not represent  in a faithful way the locations of the participants, and the fact  that transmission of messages takes time.

In this work, we propose several reduction results: When looking for an attack, it is actually sufficient to consider a simple scenario involving at most four participants located at some specific locations.

An interesting consequence of our reduction results is that it allows one to reuse ProVerif, an automated tool developed for analysing standard security protocols. As an application, we analyse several distance-bounding protocols, as well as a contactless payment protocol.

Title: TREAD: A generic and provable distance bounding protocol for privacy.

Slides: Download David Gerault's slides from the talk.

Abstract: In this talk, we will present TREAD, a terrorist fraud resistant distance-bounding construction that can be instantiated with different choices of signature and encryption schemes for various degrees of privacy: Either a lightweight protocol with no privacy, a privacy preserving (with regards to eavesdropper) protocol, or a fully anonymous (even for a malicious verifier) protocol.

After introducing this construction, we will elaborate on its security proofs in the DFKO model, and highlight the differences between this model and the one from BMV.

Title: Distance-bounding channels: Thoughts on security properties of the physical layer.

Abstract: Distance-bounding combines cryptography and physical context to create a proof of proximity between two parties.

It has been shown that the security of protocols depends on the underlying channels used for the distance-bounding exchange. Even if protocols appear acceptable from a cryptographic perspective, naïve channel implementation could allow adversaries the opportunity to execute attacks undetected. Practical channel designs, which can be used to securely realise distance-bounding protocols offer interesting challenges.

This talk touches on some research ideas related to the security implications of channel implementation, including multi-state channels, error resilience and modelling channel security.

Title: The protocol lifecycle.

Abstract: In the early stages, a protocol design probably looks like an interaction diagram with messages. Then follows a proof sketch with reverse-engineered security assumptions, and a security model that is gradually refined to capture the properties of the protocol.

There are however still many challenges ahead in moving academic work to practice. Models, assumptions and proofs need refinements in many iterations; message formats and entity behaviour need to be formalised.

In this respect, standardisation could be interesting, so prepare for dealing with politics and even more formalisation and nitpicking. Implementations will have to deal with edge-cases, and error conditions might not be as easy to deal with as originally thought. And after all that is done, when a protocol actually gets deployed, maintenance and updates will come into play.

Or maybe the whole process will never get this far because the protocol, unfortunately, is solving an irrelevant problem. In this talk we address the many challenges in the steps towards a practical protocol and discuss some good and bad practices. We will also look at the specific challenges for distance bounding protocols due to the involvement of the physical layer.

Title: Authentication at the speed of light: From distance-bounding protocols to securing broadcast navigation signals.

Slides: Download Markus Kuhn's slides from the talk.

Abstract: Cryptographic protocols for securely establishing the relative position of communication partners may rely on a number of assumptions: That faster-than-light communication is impossible, that signal-to-noise limits at the receiving end prevent early detection of incoming symbols, or that the wave-fronts characteristic for certain transmitter positions are impractical to spoof.

Some attempt to remain compatible with exiting physical-layer standards, while others use their own specialized modulation schemes. A range of approaches have been proposed and demonstrated, with significant differences in resource requirements at either end, such the accuracy of locally available time or frequency references, or permitted antenna sizes.

This talk attempts an overview and outlook on some of these approaches, for both bi-directional and broadcast applications, what inks them and what trade-offs they make.

Title: Public-key DB and its application on contactless access control.

Slides: Download Handan Kılınç's slides from the talk.

Abstract: In some applications, using public-key distance-bounding protocols is practical as no pre-shared secret is necessary between the payer and the payee. However, public-key cryptography requires much more computations than symmetric key cryptography.

In this talk, I will show secure and private public-key DB protocols (Eff-pkDB and Eff-pkDB^p) which require very few public-key computations. Then, I will define an integrated security and privacy model for access control (AC) using DB.

I will show how a secure DB protocol can be converted to a secure contactless AC protocol. Regarding privacy, I will show that the conversion does not always preserve privacy in AC but it is possible to study it on a case by case basis.

Title: Selected security and privacy challenges of implementing and deploying distance-bounding protocols.

Slides: Download Kasper Rasmussen's slides from the talk.

Abstract: Distance-bounding protocols have the potential to revolutionize the way mobile devices communicate, by providing a way to accurately and securely measure the distance to a communication partner.

Such a primitive could be used for everything from providing location based services to avoiding MITM attacks. Despite the promises of distance-bounding, the primitive has been slow to be deployed and distance bounding is not yet commonly available in consumer devices.

This is due, in part, to a number of physics-based security and privacy challenges that implementations of distance bounding protocols must overcome in order to claim the theoretical guarantees that distance-bounding protocols offer.

In this talk we will look at two concrete examples of such problems, along with potential solutions. The first is a an inherent location privacy problem of distance-bounding protocols and the second is the problem of processing information in zero time.

Title: A practical countermeasure against relay attacks.

Slides: Download Pierre-Henri Thevenon's slides from the talk.

Abstract: Nowadays, identification systems based on contactless technologies such as RFID and NFC are extensively used worldwide. During the last few years, we have been accustomed to carry these devices to pay, to take public transportation, to cross a border or to enter a sensitive area.

However, the physical layer and the technological features of these contactless systems do not allow to reach the required level of security for payment applications or access control. Among the attacks on the physical layer, the relay attack is the most dangerous because it allows to modify the communication distance between the reader and the contactless card without the agreement of their owners. A relay attack is thoroughly transparent for current contactless systems and cryptographic protocols.

A possible countermeasure is the distance-bounding protocol which can add an upper bound for the distance between the two communicating devices. During this talk, we will discuss about the implementation of a countermeasure dedicated to contactless systems.

To better understand the potential of a relay attack, we will present three kinds of relay: A wired passive relay, a relay based on a wireless super-heterodyne system and a wireless relay with a complete demodulation of the signal.

To test our solution, these relays were developed by keeping in mind the concern of introducing a delay as low as possible. Then, we will analyse the weaknesses of current distance-bounding protocols and introduce a more adapted solution which uses the physical layer to carry out a delay assessment.

Finally, we will discuss about the security of this solution and talk about the improvements that can be made.

Title: Distance-bounding protocols: Computational vs. symbolic models.

Slides: Download Jorge Toro Pozo's slides from the talk.

Abstract: A relay attack is a type of man-in-the-middle in which the adversary simply relays the verbatim messages exchanged on the network. Such attack needs to be defended against particularly in applications where proximity is a fundamental security requirement.

Well-established countermeasures against relay attacks are distance bounding protocols, which are cryptographic protocols that securely establish an upper bound on the physical distance between the participants.

Distance-bounding protocols stand up well against relay attacks, however, more sophisticated attacks have emerged such as mafia fraud, distance fraud, distance hijacking, and terrorist fraud. Over the years, many distance-bounding protocols have been proposed, along with their security analyses; mainly done with probabilistic approaches built upon computational models.

Few other works show some progress towards symbolic security models for distance-bounding. Though those models are still not fully deployable on standard verification tools, mainly because physical properties (such as distance) are hard to model symbolically.

In this talk we address both approaches for verification of distance-bounding protocols. In the case of probabilistic security analysis, we provide an automata-based representation of protocols that allows us to study their generic properties, such as security lower bounds in relation to space complexity.

Further, we describe a novel family of protocols which resist well to mafia fraud attacks. Regarding symbolic verification, we introduce a causality-based characterization of secure distance-bounding that discards the notions of time and location. This allows us to verify the correctness of distance-bounding protocols with the Tamarin tool.

With our framework, we confirm known vulnerabilities in a number of protocols and discover unreported attacks against two recently published protocols.

Organisers' talks

Title: A primer on relay attacks and distance-bounding protocols.

Slides: Download Gildas Avoine's slides from the talk.

Abstract: In this talk, we will open the workshop with an introduction to relay attacks (and variants) and an overview of distance-bounding (DB) protocols.

After a historical reminder about DB protocols, we will highlight the gap between theory and practice in the design of such protocols.

We will conclude the talk with open questions that may feed the debate during the workshop.

Title: Provable-security models for distance-bounding.

Slides: Download Ioana Boureanu's slides from the talk.

Abstract: This will be an introduction to provable security for distance-bounding. As support, we will focus on symmetric key distance-bounding designs.

We will include the first model going towards provable-security in DB, i.e., a framework by Avoine, then the session-based by Fischlin et al., and finally the “interactive-proof-like” model by Boureanu et al.

Title: An introduction to formal symbolic models.

Slides: Download Stéphanie Delaune's slides from the talk.

Abstract: Formal symbolic models have proved their usefulness for analysing the security of protocols, and several automatic tools for protocol verification are  nowadays available, e.g. ProVerif, Tamarin, Avantssar platform.

Unlike the so-called computational approach, the symbolic approach  makes strong assumptions on cryptographic primitives but fully models interactions between the participants of the protocols.

Although less precise, this symbolic approach benefits from automation and can thus target more complex protocols and scenarios than those analysed using the computational approach.

In this talk, I will give a brief overview of the symbolic approach, explain the strengths of this approach, but also its limitations especially regarding the analysis of distance-bounding protocols.

Location and time   

This event took place at São Miguel Island, Azore Islands (co-located with Cryptacus 2018 Summer school) on 14-15 April 2018.

The sessions occurred at the Lince Azores Hotel in the City of Ponta Delgada.

 Organising committee

  • Gildas Avoine, University of Rennes, INSA Rennes, IRISA, Rennes, France
  • Ioana Boureanu, University of Surrey, Guildford, UK
  • Stéphanie Delaune, University of Rennes, CNRS,  IRISA, Rennes, France
  • Cristina Onete, University of Limoges, Limoges, France.

Contact us

Find us

Address
Surrey Centre for Cyber Security
University of Surrey
Guildford
Surrey
GU2 7XH