DBVerify

Information

This repository contains the source files for Tamarin analysis of distance-bounding security protocols. For further details, see our paper Distance-Bounding Protocols: Verification without Time and Location.

DBVerify-Feb2018.zip (contains amendments thanks to observations by A. Debant and S. Delaune from IRISA, Rennes).
A later version available on Github.

tamarinprotocols contains the .spthy files used by Tamarin for the analysis. If the Tamarin tool is installed on your device, they can be executed by the command tamarin-prover --prove <filename>
mscs contains pdf diagrams showing the intended execution trace of each protocol. These diagrams are slightly abstracted from the original definition of the protocol - in most cases, this is the conversion of the fast phase of a communication protocol from a series of short messages to one long message. At times, the equational theory has been changed to a strictly stronger version than that provided in the original paper. The existence of an attack on the abstracted protocol indicates the existence of an attack on the original version.