Cryptology ePrint Archive: Report 2020/1000
Precise and Mechanised Models and Proofs for Distance-Bounding and an Application to Contactless Payments
Ioana Boureanu and Constantin Catalin Dragan and François Dupressoir and David Gerault and Pascal Lafourcade
Abstract: Distance-bounding protocols provide a means for a verifier (e.g., an RFID reader) to estimate his relative distance to a prover (e.g., a bankcard), in order to counteract relay attacks. We propose FlexiDB, a new cryptographic model for DB, parameterised over fine-grained corruptions. It allows to consider trivial cases, classical cases but also new, generalised scenarios in which we show manipulating differently-corrupt provers at once leads to new attacks. We propose a proof-of-concept mechanisation of FlexiDB in the interactive cryptographic prover EasyCrypt, and use it to prove a flavour of man-in-the-middle security on a variant of MasterCard's contactless-payment protocol.
Category / Keywords: distance-bounding, security formalism, mechanised-proof, easycrypt
Date: received 18 Aug 2020
Contact author: c dragan at surrey ac uk, i boureanu@surrey ac uk
Available format(s): PDF | BibTeX Citation
Version: 20200818:172838 (All versions of this report)
Short URL: ia.cr/2020/1000
[ Cryptology ePrint archive ]