Paper 2018/1243

BoxDB: Realistic Adversary Model for Distance Bounding

Ioana Boureanu, David Gerault, and Pascal Lafourcade

Abstract

Recently, the worldwide-used EMVCo standard for electronic payments included the “EMV RRP (Europay Mastercard Visa Relay-Resistant Protocol)” protocol. This uses distance bounding to counteract relay attacks in contactless payments. Last year, EMV RRP was widely analysed by symbolic verification methods, with several distance-bounding attacks and fixes proposed. Yet, one version of EMV RRP was found secure by all such formal analyses. Contrary to this, we exhibit an attack on this version of EMV RRP. Moreover, we exhibit similar vulnerabilities on another EMV RRP variant and on 13 distance-bounding protocols. We then propose a secure version of the EMV RRP protocol, called PayPass+, and prove its security, in a strong adversary model. Our attacks stem from a new, fine-grained corruption model. We formalise it in a provable-security model, called BoxDB. In BoxDB, we express traditional as well as new DB security-properties. All our positive and negative security results are given in this formal model. Also, to fill a gap in computer-aided verification of security, BoxDB is designed specifically to lay the foundations for machine-checked cryptographic proofs for protocols based on distance bounding. The threat model in BoxDB is modular and can be tailored to different applications. Importantly, the corruption model in BoxDB also leads us to show that the strongest threat against DB protocols, namely terrorist frauds, need not be considered in formal DB-security models.