Mini-workshop on Distance-Bounding Protocols
Mini-workshop on Distance-Bounding Protocols (14 May 2019)
On May 14th, 2019, SaToSS organized a mini-workshop on distance-bounding protocols, featuring four invited talks by prominent researchers in the field.
List of invited talks
| Applying Formal Symbolic Verification to Distance-Bounding Protocols |
| Stéphanie Delaune, IRISA Rennes, France |
| Abstract: The shrinking size of microprocessors as well as the ubiquity of wireless communication have led to the proliferation of portable computing devices with novel security requirements. Whereas traditional security protocols achieve their security goals relying solely on cryptographic primitives like encryptions and hash functions, the protocols employed to secure these devices establish and rely in addition on properties of the physical world. For instance, they may use, as basic building blocks, protocols for ensuring physical proximity, secure localisation, or secure neighbourhood discovery. The research community in logics, program verification, and security has already a long tradition in developing techniques and tools to analyse key establishment and authentication protocols. However, distance-bounding protocols which are used to provide secure proximity control, raise new research challenges, and cannot be analysed today using off-the-shelf symbolic verification tools (e.g. ProVerif). In this talk, we will describe and discuss some recent results we have developed to automatically analyse distance-bounding protocols. |
| Making Contactless Payments Robust Against Collusive Relaying |
| Ioanna Boureanu, University of Surrey, UK |
| Abstract: In this talk, we will discuss the aspect of rogue contactless-payment readers/terminals taking part in relay attacks. We call this notion collusive relaying. We will show three novel proximity-checking protocols that protect contactless payments against collusive relaying. They are hierarchical, with respect to the protection level, but also w.r.t. the level of change required for them to be adopted on top of the ubiquitous EMV infrastructure for e-payments. (This talk is based on a Financial Crypto 2019 paper). |
| Limiting Man-in-the-Middle Attackers via Proximity Verification |
| Rolando Trujillo-Rasua, Deakin University, Australia |
| Abstract: There exist many communication protocols that operate under the assumption that the prover may be dishonest. This makes it hard for the security analyst to prove that the protocol achieves the intended security goals against a Dolev-Yao attacker. We will discuss in this talk the claim that, when the prover is physically close to the verifier, man-in-the-middling is thwarted. We will use memory erasure as the application domain and showcase protocols that aim to counteract man-in-the-middle attackers via proximity verification. |
| Breaking and Fixing the ICAO 9303 Standard for Basic Access Control using Bisimilarity |
| Ross Horne, University of Luxembourg, Luxembourg |
| Abstract: The ICAO 9303 standard for e-passports includes a basic access control (BAC) mechanism that protects the user from skimming by attackers who do not have physical access to the e-passport. It should also protect the user from being traced from one reader session to another. While, it is well known that there are attacks on privacy, allowing an attacker to link multiple uses of the same passport, due to differences in implementation; it is still debated whether there is an attack on unlinkability on the protocol in the standard itself. This paper clarifies the nature of the debate, and sources of confusion. We demonstrate that some assumptions previously made are flawed and uses the bisimilarity technique to uncover an attack on unlinkability. Furthermore, we propose a fix for the protocol that is within the scope of standard, and prove that it is correct, again by using bisimilarity. We also showcases a state-of-the-art approach to bisimilarity and its characteristic modal logic. |