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.
Category / Keywords: cryptographic protocols / Date: received 30 Dec 2018, last revised 5 Mar 2019, withdrawn 19 Aug 2020 Contact author: icboureanu at gmail com Available format(s): (-- withdrawn --) Version: 20200819:095109 (All versions of this report) Short URL: ia.cr/2018/1243