Paper Info
Title
Formal Reasoning about Physical Properties of Security Protocols
Abstract
Traditional security protocols are mainly concerned with authentication and key establishment 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 secure time synchronization. We present a formal model for modeling and reasoning about such physical security protocols. Our model extends standard, inductive, trace-based, symbolic approaches with a formalization of physical properties of the environment, namely communication, location, and time. In particular, communication is subject to physical constraints, for example, message transmission takes time determined by the communication medium used and the distance between nodes. All agents, including intruders, are subject to these constraints and this results in a distributed intruder with restricted, but more realistic, communication capabilities than those of the standard Dolev-Yao intruder. We have formalized our model in Isabelle/HOL and have used it to verify protocols for authenticated ranging, distance bounding, broadcast authentication based on delayed key disclosure, and time synchronization.
Year
DOI
Venue
2011
10.1145/2019599.2019601
ACM Trans. Inf. Syst. Secur.
Keywords
DocType
Volume
Formal Reasoning,physical property,formal model,broadcast authentication,communication capability,communication medium,physical constraint,Physical Properties,Security Protocols,physical security protocol,time synchronization,physical world,secure time synchronization
Journal
14
Issue
ISSN
Citations 
2
1094-9224
9
PageRank 
References 
Authors
0.49
34
4
Name
Order
Citations
PageRank
David A. Basin14930281.93
Srdjan Capkun24970390.04
Patrick Schaller3513.24
Benedikt Schmidt446829.24