Reference : Computational and symbolic analysis of distance-bounding protocols
Dissertations and theses : Doctoral thesis
Engineering, computing & technology : Computer science
Security, Reliability and Trust
Computational and symbolic analysis of distance-bounding protocols
Toro Pozo, Jorge Luis mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > >]
University of Luxembourg, ​Esch-sur-Alzette, ​​Luxembourg
xii, 129
Mauw, Sjouke mailto
Le Traon, Yves mailto
Trujillo Rasúa, Rolando mailto
Boureanu, Ioana mailto
Delaune, Stéphanie mailto
[en] distance bounding ; security protocols ; computational analysis ; symbolic analysis ; RFID ; wireless security ; formal proofs ; access control ; contactless
[en] Contactless technologies are gaining more popularity everyday. Credit cards enabled with contactless payment, smart cards for transport ticketing, NFC-enabled mobile phones, and e-passports are just a few examples of contactless devices we are familiar with nowadays. Most secure systems meant for these devices presume physical proximity between the device and the reader terminal, due to their short communication range. In theory, a credit card should not be charged of an on-site purchase if the card is not up to a few centimeters away from the payment terminal. In practice, this is not always true. Indeed, some contactless payment protocols, such as Visa's payWave, have been shown vulnerable to relay attacks. In a relay attack, a man-in-the-middle uses one or more relay devices in order to make two distant devices believe they are close. Relay attacks have been implemented also to bypass keyless entry and start systems in various modern cars.

Relay attacks can be defended against with distance-bounding protocols, which are security protocols that measure the round-trip times of a series of challenge/response rounds in order to guarantee physical proximity. A large number of these protocols have been proposed and more sophisticated attacks against them have been discovered. Thus, frameworks for systematic security analysis of these protocols have become of high interest. As traditional security models, distance-bounding security models sit within the two classical approaches: the computational and the symbolic models. In this thesis we propose frameworks for security analysis of distance-bounding protocols, within the two aforementioned models.

First, we develop an automata-based computational framework that allows us to generically analyze a large class of distance-bounding protocols. Not only does the proposed framework allow us to straightforwardly deliver computational (in)security proofs but it also permits us to study problems such as optimal trade-offs between security and space complexity. Indeed, we solve this problem for a prominent class of protocols, and propose a protocol solution that is optimally secure amongst space-constrained protocols within the considered class.

Second, by building up on an existing symbolic framework, we develop a causality-based characterization of distance-bounding security. This constitutes the first symbolic property that guarantees physical proximity without modeling continuous time or physical location. We extend further our formalism in order to capture a non-standard attack known as terrorist fraud. By using our definitions and the verification tool Tamarin, we conduct a security survey of over 25 protocols, which include industrial protocols based on the ISO/IEC 14443 standard such as NXP's MIFARE Plus with proximity check and Mastercard's PayPass payment protocol. For the industrial protocols we find attacks, propose fixes and deliver security proofs of the repaired versions.
Fonds National de la Recherche - FnR
Symbolic verification of distance-bounding and multiparty authentication protocols
Researchers ; Professionals ; Students
FnR ; FNR10188265 > Jorge Luis Toro Pozo > > Symbolic verification of distance-bounding and multipartyauthentication protocols > 01/06/2015 > 31/05/2019 > 2015

File(s) associated to this reference

Fulltext file(s):

Open access
thesis-jorge.pdfthesisAuthor postprint1.99 MBView/Open

Additional material(s):

File Commentary Size Access
Limited access
jorge-slides.pdfSlides for the defence1.02 MBRequest a copy

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.