|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
2009 22nd IEEE Computer Security Foundations Symposium
Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks
Port Jefferson, New York
July 08-July 10
ISBN: 978-0-7695-3712-2
| ASCII Text | x | ||
| Patrick Schaller, Benedikt Schmidt, David Basin, Srdjan Capkun, "Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks," 2012 IEEE 25th Computer Security Foundations Symposium, pp. 109-123, 2009 22nd IEEE Computer Security Foundations Symposium, 2009. | |||
| BibTex | x | ||
| @article{ 10.1109/CSF.2009.6, author = {Patrick Schaller and Benedikt Schmidt and David Basin and Srdjan Capkun}, title = {Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks}, journal ={2012 IEEE 25th Computer Security Foundations Symposium}, volume = {0}, year = {2009}, issn = {1063-6900}, pages = {109-123}, doi = {http://doi.ieeecomputersociety.org/10.1109/CSF.2009.6}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - 2012 IEEE 25th Computer Security Foundations Symposium TI - Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks SN - 1063-6900 SP109 EP123 A1 - Patrick Schaller, A1 - Benedikt Schmidt, A1 - David Basin, A1 - Srdjan Capkun, PY - 2009 KW - Security Protocols KW - Formal Security Model KW - Wireless Network Protocols KW - Isabelle/HOL VL - 0 JA - 2012 IEEE 25th Computer Security Foundations Symposium ER - | |||
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSF.2009.6
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.
Index Terms:
Security Protocols, Formal Security Model, Wireless Network Protocols, Isabelle/HOL
Citation:
Patrick Schaller, Benedikt Schmidt, David Basin, Srdjan Capkun, "Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks," csf, pp.109-123, 2009 22nd IEEE Computer Security Foundations Symposium, 2009
Usage of this product signifies your acceptance of the Terms of Use.