Paper 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.
Metadata
- Available format(s)
- Publication info
- Preprint. MINOR revision.
- Keywords
- distance-boundingsecurity formalismmechanised-proofeasycrypt
- Contact author(s)
-
c dragan @ surrey ac uk
i boureanu @ surrey ac uk - History
- 2021-05-20: last of 2 revisions
- 2020-08-18: received
- See all versions
- Short URL
- https://ia.cr/2020/1000
- License
-
CC BY