Main content

ProtoVeriPhy is an Isabelle/HOL framework for analyzing physical protocols such as distance bounding protocols, secure time-synchronization protocols, and authenticated ranging protocols.

There are two versions of the framework. The original version and an extended version that accounts for overshadowing attacks.

The original version is described in the articles "Formal Reasoning about Physical Properties of Security Protocols" (TISSEC'11) and "Let's get physical: Models and Methods for Real-World Security Protocols" (TPHOLS'09). It includes support for reasoning about XOR and authenticated ranging, distance bounding, broadcast authentication, and secure time synchronization protocols as case studies:

Isabelle theories and proofs

An extended version that accounts for overshadowing attacks is described in "Distance Hijacking Attacks on Distance Bounding Protocols" (Security&Privacy'12). This version includes proofs that the Brands-Chaum protocol and a wrongly fixed version are vulnerable to Distance-Hijacking attacks. Additionally, it contains proofs that our proposed fixes indeed prevent these attacks.

Isabelle theories and proofs


Benedikt Schmidt, Patrick Schaller

Page URL:
Wed Jul 26 00:27:31 CEST 2017
© 2017 Eidgenössische Technische Hochschule Zürich