Marienplatz (city centre)

Englischer Garten
The English Garden

Chinesischer Turm
Chinese Tower (famous beer garden)

Computer science building
The Computer Science building of the TUM

Main hall of the computer science building
The main hall in the CS-building

The river Isar
The Isar river

The conference poster

SPEAKER: David Basin

TITLE: Let's get physical: models and methods for real-world security protocols

(Joint work with Patrick Schaller, Benedikt Schmidt, and Srdjan Capkun)

Traditional security protocols are mainly concerned with key establishment and principal authentication, and rely on predistributed keys and properties of cryptographic operators. In contrast, new application areas are emerging that establish and rely on properties of the physical world. Examples include secure localization, distance bounding, and device pairing protocols.

We present a formal model extending standard, inductive, trace-based, symbolic approaches in two directions. In terms of communication, we refine the standard Dolev-Yao model to account for network topology, transmission delays, and node positions. This results in a distributed intruder with restricted, but more realistic, communication capabilities. On the level of messages, we use an abstract message theory to establish facts independent of the concrete protocol and message theory. To analyse the security of a given protocol, we instantiate the abstract message theory so that properties of the cryptographic operators under consideration are accurately modeled. We describe the formalization of this model in Isabelle/HOL and present its application to a distance bounding protocol, where the concrete message theory includes exclusive-or and its associated equational theory.

Last modified: Wed Apr 29 19:18:31 CEST 2009 [Validate this page.]