Modelling and Analysis of a Hierarchy of Distance Bounding Attacks

Explore a comprehensive analysis of distance bounding protocols in this 23-minute conference talk from USENIX Security '18. Delve into an extended applied pi-calculus model designed specifically for these protocols, and discover how various security properties can be encoded and ranked. Examine the relationship between security properties and attacker models, including a newly identified property called "uncompromised distance bounding." Learn about the compilation process that enables automatic protocol verification using the ProVerif tool, and see its application in analyzing real-world distance bounding protocols from MasterCard and NXP. Gain valuable insights into the security of contactless payment cards and car entry systems through this in-depth presentation by Tom Chothia from the University of Birmingham.