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 protocols for secure localization, distance bounding, and device pairing. We present a formal model that extends inductive, trace-based approaches in two directions. First, 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, comon capabilities. Second, we develop an abstract message theory that formalizes protocol-independent facts about messages, which hold instances. When verifying protocols, we instantiate the abstract message theory, modeling the properties of the cryptographic operators under consideration. We have formalized this model in Isabel...

• Type: Conference
• Year: 2009
• Where: TPHOL
• Authors: David A. Basin, Srdjan Capkun, Patrick Schaller, Benedikt Schmidt
• Keywords: Abstract Message Theory, Artificial Intelligence, Cryptographic Operators, TPHOL 2009, Traditional Security Protocols