@InProceedings{	  schaller.ea:modeling:2009,
  abstract	= {We present a formal model for modeling and reasoning about
		  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 traveled. 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 used it to verify
		  protocols for authenticated ranging, distance bounding, and
		  broadcast authentication based on delayed key disclosure.},
  author	= {Patrick Schaller and Benedikt Schmidt and David Basin and
		  Srdjan Capkun},
  booktitle	= {22nd IEEE Computer Security Foundations Symposium},
  language	= {USenglish},
  organization	= {IEEE Computer Society Washington, DC, USA},
  pages		= {109--123},
  pdf		= {papers/2009/CSF2009.pdf},
  title		= {Modeling and Verifying Physical Properties of Security
		  Protocols for Wireless Networks},
  year		= 2009,
  user		= {benschmi}
}