 |
|
||||||||||
ProtoVeriPhy
Zurich Information Security Center
We are affiliated with the Zurich Information Security Center (ZISC)
The ZISC workshop on Securing Future Communication Networks against Emerging Threats will take place on 16-17 October 2013 at ETH Zurich and is announced here.
Events & News
- Our book Applied Information Security - A Hands-on Approach is an editor's pick and the current highlight of ACM's Computing Reviews.
- David Basin, Torsten Lodderstedt, and Juergen Doser, received the "Ten Year Most Influential Paper Award" at the MODELS 2012 conference for the paper SecureUML: A UML-Based Modeling Language for Model-Driven Security.
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:
- Proof Outline: outline.pdf
- Proof Document: document.pdf
- Theory files: 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:
- Proof Outline: outline.pdf
- Proof Document: document.pdf
- Theory files: ProtoVeriPhy-20120305.tar.gz
Authors:
Benedikt Schmidt, Patrick Schaller
Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne
graphische Elemente dargestellt. Die Funktionalität der
Website ist aber trotzdem gewährleistet. Wenn Sie diese
Website regelmässig benutzen, empfehlen wir Ihnen, auf
Ihrem Computer einen aktuellen Browser zu installieren. Weitere
Informationen finden Sie auf
folgender
Seite.
Important Note:
The content in this site is accessible to any browser or
Internet device, however, some graphics will display correctly
only in the newer versions of Netscape. To get the most out of
our site we suggest you upgrade to a newer browser.
More
information
