@Article{	  basin.ea:formal:2011,
  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.},
  author	= {David Basin and Srdjan Capkun and Patrick Schaller and
		  Benedikt Schmidt},
  journal	= {ACM Transactions on Information and System Security},
  language	= {USenglish},
  month		= 09,
  number	= 2,
  pages		= {16:1--16:29},
  pdf		= {papers/2011/1_journal.pdf},
  title		= {Formal Reasoning about Physical Properties of Security
		  Protocols},
  url		= {http://dx.doi.org/10.1145/2019599.2019601},
  volume	= 14,
  year		= 2011,
  user		= {benschmi}
}