Paper 2020/1000

Mechanised Models and Proofs for Distance-Bounding

Ioana Boureanu, Constantin Catalin Dragan, François Dupressoir, David Gerault, and Pascal Lafourcade

Abstract

In relay attacks, a man-in-the-middle adversary impersonates a legitimate party and makes it this party appear to be of an authenticator, when in fact they are not. In order to counteract relay attacks, distance-bounding protocols provide a means for a verifier (e.g., an payment terminal) to estimate his relative distance to a prover (e.g., a bankcard). We propose FlexiDB, a new cryptographic model for distance bounding, parameterised by different types of fine-grained corruptions. FlexiDB allows to consider classical cases but also new, generalised corruption settings. In these settings, we exhibit new attack strategies on existing protocols. Finally, we propose a proof-of-concept mechanisation of FlexiDB in the interactive cryptographic prover EasyCrypt. We use this to exhibit a flavour of man-in-the-middle security on a variant of MasterCard's contactless-payment protocol.

Metadata
Available format(s)
PDF
Publication info
Published elsewhere. Minor revision. IEEE Computer Security Foundations Symposium 2021
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
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2020/1000,
      author = {Ioana Boureanu and Constantin Catalin Dragan and François Dupressoir and David Gerault and Pascal Lafourcade},
      title = {Mechanised Models and Proofs for Distance-Bounding},
      howpublished = {Cryptology ePrint Archive, Paper 2020/1000},
      year = {2020},
      note = {\url{https://eprint.iacr.org/2020/1000}},
      url = {https://eprint.iacr.org/2020/1000}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.