Computational and symbolic analysis of distance-bounding protocols

Open Access
Author:
Description:
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 ...
Publisher:
Unilu - University of Luxembourg
Contributors:
Mauw, Sjouke
Year of Publication:
2019-05-14
Document Type:
doctoral thesis ; http://purl.org/coar/resource_type/c_db06 ; info:eu-repo/semantics/doctoralThesis ; [Doctoral and postdoctoral thesis]
Language:
en
Subjects:
distance bounding ; security protocols ; computational analysis ; symbolic analysis ; RFID ; wireless security ; formal proofs ; access control ; contactless ; Engineering ; computing & technology ; Computer science ; Ingénierie ; informatique & technologie ; Sciences informatiques
DDC:
005 Computer programming, programs & data (computed)
Rights:
open access ; http://purl.org/coar/access_right/c_abf2 ; info:eu-repo/semantics/openAccess
Relations:
FNR10188265 - Symbolic Verification Of Distance-bounding And Multiparty Authentication Protocols, 2015 (01/06/2015-31/05/2019) - Jorge Luis Toro Pozo ; https://orbilu.uni.lu/handle/10993/39506 ; info:hdl:10993/39506
URL:
https://orbilu.uni.lu/handle/10993/39506
https://orbilu.uni.lu/bitstream/10993/39506/1/thesis-jorge.pdf
Content Provider:
University of Luxembourg: ORBilu - Open Repository and Bibliography  Flag of Luxembourg