Formal Reasoning about Physical Properties of Security Protocols
Formal Reasoning about Physical Properties of Security Protocols
复制标题
关于安全协议物理属性的形式推理
DOI：
10.1145/2019599.2019601
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Benedikt Schmidt
中科院分区：
文献类型：
--
作者：
D. Basin;Srdjan Capkun;P. Schaller;Benedikt Schmidt
传统的安全协议主要涉及认证和密钥建立，并依赖于预先分配的密钥和密码运算符的性质。相反，新的应用领域正在出现，建立和依赖于物理世界的属性。示例包括用于安全定位、距离界定和安全时间同步的协议。
我们提出了一个形式化的模型建模和推理这样的物理安全协议。我们的模型扩展了标准的，归纳的，基于痕迹的，象征性的方法与环境的物理属性，即通信，位置和时间的形式化。特别地，通信受到物理约束，例如，消息传输所花费的时间由所使用的通信介质和节点之间的距离确定。所有的代理，包括入侵者，都受到这些限制，这导致在一个分布式入侵者的限制，但更现实的，通信能力比那些标准的Dolev姚入侵者。我们已经正式我们的模型在伊莎贝尔/HOL，并已使用它来验证协议的认证测距，距离绑定，广播认证的基础上延迟密钥披露，和时间同步。
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.
让我们来看看实际情况：现实世界安全协议的模型和方法
DOI：
10.1007/978-3-642-03359-9_1
发表时间：
2009
期刊：
影响因子：
--
作者：
Stefan Berghofer;Lukas Bulwahn;Florian Haftmann
通讯作者：
Florian Haftmann