Copenhagen Programming Language Seminar
(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.
Scientific host:Carsten Schürmann Administrative host:Renée Korver Michan.
All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org