Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks
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.
People
BibTex
@INPROCEEDINGS{schaller2009modeling,
isbn = {978-0-7695-3712-2},
doi = {10.1109/CSF.2009.6},
year = {2009},
booktitle = {2009 22nd IEEE Computer Security Foundations Symposium},
type = {Conference Paper},
author = {Schaller, Patrick and Schmidt, Benedikt and Basin, David and Capkun, Srdjan},
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.},
keywords = {Formal Security Model; Isabelle/HOL; Security Protocols; Wireless Network Protocols},
language = {en},
address = {Piscataway, NJ},
publisher = {IEEE},
title = {Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks},
PAGES = {109 - 123},
Note = {22nd IEEE Computer Security Foundations Symposium (CSF 2009); Conference Location: Port Jefferson, NY, USA; Conference Date: July 8-10, 2009}
}Research Collection: 20.500.11850/638495