ProtoVeriPhy

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

• Theory files: external page ProtoVerPhy-20090616.tar.gz

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

• Theory files: external page ProtoVerPhy-overshadow.tar.gz

Authors

Benedikt Schmidt, Patrick Schaller