Modelling and Analysis of a Hierarchy of Distance Bounding Attacks
summary
Extends the applied pi-calculus with location and start/stop timer actions to model distance‑bounding behavior, defines and orders five+ formal security properties, and introduces uncompromised distance bounding as a new, practically relevant property for payment cards and car fobs. Compiles models into the ProVerif tool for automated checking, applies this to MasterCard and an NXP‑patent protocol, and finds new relay/hijacking attacks including a practical weakness if NXP uses a shared key instead of per‑device keys.
AI-written summary · about
chapters (9)
- 0:00Introduction to protocol risks
- 1:20Real-world relay attack examples
- 3:03Analyzing payment protocols
- 6:32Proposed and patented defenses
- 8:26Modeling language and semantics
- 11:13Formalizing attack scenarios
- 15:07Comparing security properties
- 18:17Experimental results and conclusion
- 21:47Q&A on relay assumptions
related talks
51mSecure Applications, By Design
37mFirst Contact - Vulnerabilities in Contactless Payments
45mPadding Oracle Attacks on Smart Cards
40mUsing Threat Modeling to Improve Compliance
06mHuman-in-the-Loop for Secure Digital Wallets Transactions
50mBreaking Payment Points of Interaction (POI)
38mHow to read a PL-security paper
37mHacking a Cat — Going Beyond Traditional Attack Vectors