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