Symbolic verification of distance bounding protocols
With the proliferation of contactless applications, obtaining reliable information about distance is becoming an important security goal, and specific protocols have been designed for that purpose. These protocols typically measure the round trip time of messages and use this information to infer a distance.
Formal methods have proved their usefulness when analysing standard security protocols such as confidentiality or authentication protocols. However, existing results and tools do not apply to distance bounding protocols. This is due in particular to the fact that the communication model is too abstract and do not reflect constraints from the physical world (e.g. messages can not travel faster than the speed of the light).
In this paper, we propose a symbolic model suitable to analyse distance bounding protocols. We propose a new procedure for analysing (a bounded number of sessions of) protocols in this model. The procedure has been integrated in the Akiss tool and tested on various distance bounding protocols among which MasterCard and NXP.
Thu 11 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 16:00 | |||
14:00 30mTalk | Wys*: A DSL for Verified Secure Multi-party Computations POST Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Michael Hicks University of Maryland, College Park Link to publication | ||
14:30 30mTalk | Generalised Differential Privacy for Text Document Processing POST Link to publication | ||
15:00 30mTalk | Symbolic verification of distance bounding protocols POST Link to publication | ||
15:30 30mTalk | On the formalisation of Σ-Protocols and Commitment Schemes POST Link to publication |