Marienplatz (city centre)

The English Garden

Chinese Tower (famous beer garden)

The Computer Science building of the TUM

The main hall in the CS-building

The Isar river

The conference poster

SPEAKER: David Basin

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

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.