Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks
Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks
复制标题
无线网络安全协议的物理属性建模和验证
DOI：
10.1109/csf.2009.6
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Srdjan Capkun
中科院分区：
文献类型：
--
作者：
P. Schaller;Benedikt Schmidt;D. Basin;Srdjan Capkun
我们提出了一个形式化模型的建模和推理的安全协议。我们的模型扩展了标准的，归纳的，基于痕迹的，象征性的方法与环境的物理属性，即通信，位置和时间的形式化。特别是，通信受到物理约束，例如，消息传输所需的时间由所使用的通信介质和行进的距离决定。所有的代理，包括入侵者，都受到这些限制，这导致在一个分布式入侵者的限制，但更现实的，通信能力比那些标准的Dolev姚入侵者。我们已经正式我们的模型在Isabelle/HOL和使用它来验证协议的认证测距，距离绑定，和广播认证的基础上延迟密钥披露。
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.