Alexandre Debant and Stéphanie Delaune. Symbolic Verification of Distance Bounding Protocols. In Proceedings of the 8th International Conference on Principles of Security and Trust (POST'19), Lecture Notes in Computer Science, Springer, Prague, Czech Republic, 2019.
With the proliferation of contactless applications, obtaining reliable information about distance is becoming an importantsecurity goal, and specific protocols have been designed for that purpose.These protocols typically measure the round trip time of messagesand use this information to infera distance.Formal methods have proved their usefulness when analysing standardsecurity protocols such as confidentiality or authenticationprotocols. However, due to their abstract communication model, existing results and tools do not apply to distance bounding protocols.In this paper, we consider a symbolic model suitable to analysedistance bounding protocols, and we propose a new procedure foranalysing (a bounded number of sessions of) protocols in this model.The procedure has been integrated in the Akisstool and tested on various distance bounding and payment protocols (e.g.MasterCard, NXP).
@inproceedings{DD-post19,
abstract = {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, due to their abstract communication model,
existing results and tools do not apply to distance bounding protocols.
In this paper, we consider a symbolic model suitable to analyse
distance bounding protocols, and 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 and payment protocols (e.g.
MasterCard, NXP).
},
address = {Prague, Czech Republic},
author = {Alexandre Debant and
St{\'{e}}phanie Delaune},
title = {Symbolic Verification of Distance Bounding Protocols},
booktitle = {Proceedings of the 8th International Conference on Principles of Security and Trust (POST'19)},
year = {2019},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
acronym = {{POST}'19}
}