Modelling and Analysis of a Hierarchy of Distance Bounding Attacks

This course aims to teach learners how to model distance bounding protocols using an extension of the applied pi-calculus. The course covers encoding various security properties in the model, proving a partial order between them, and relating security properties to different attacker models. The teaching method involves demonstrating how to compile the new calculus into the applied pi-calculus for automatic protocol checks using the ProVerif tool. The course is intended for individuals interested in understanding and analyzing security properties of distance bounding protocols, particularly in the context of protecting devices like contactless payment cards or car entry systems.