Let's Get Physical: Models and Methods for Real-World Security Protocols
Let's Get Physical: Models and Methods for Real-World Security Protocols
复制标题
让我们来看看实际情况：现实世界安全协议的模型和方法
DOI：
10.1007/978-3-642-03359-9_1
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Florian Haftmann
中科院分区：
文献类型：
--
作者：
Stefan Berghofer;Lukas Bulwahn;Florian Haftmann
传统的安全协议主要涉及密钥建立和主体认证，依赖于预先分配的密钥和密码算子的性质。相反，新的应用领域正在出现，建立和依赖于物理世界的属性。例子包括协议的安全定位，距离界定，和设备pairing.We提出了一个正式的模型，扩展归纳，跟踪为基础的方法在两个方向。首先，我们改进了标准的Dolev-Yao模型，以考虑网络拓扑结构，传输延迟和节点位置。这导致分布式入侵者具有有限的，但更现实的通信能力。第二，我们开发了一个抽象的消息理论，形式化的协议无关的事实消息，这适用于所有的情况。在验证协议时，我们实例化抽象消息理论，对所考虑的密码运算符的属性进行建模。我们已经正式这个模型在Isabelle/HOL和使用它来验证距离边界协议的具体消息理论包括异或。
Traditional security protocols are mainly concerned with key establishment and principal authentication 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 device pairing.We present a formal model that extends inductive, trace-based approaches in two directions. First, we refine the standard Dolev-Yao model to account for network topology, transmission delays, and node positions. This results in a distributed intruder with restricted, but more realistic, communication capabilities. Second, we develop an abstract message theory that formalizes protocol-independent facts about messages, which hold for all instances. When verifying protocols, we instantiate the abstract message theory, modeling the properties of the cryptographic operators under consideration. We have formalized this model in Isabelle/HOL and used it to verify distance bounding protocols where the concrete message theory includes exclusive-or.
登录
查看更多内容
DOI：
10.1007/978-1-4020-6324-4
发表时间：
2008
期刊：
Proceedings IEEE 24th Annual Joint Conference of the IEEE Computer and Communications Societies.
影响因子：
--
作者：
T. Nipkow
通讯作者：
T. Nipkow
无线网络安全协议的物理属性建模和验证
DOI：
10.1109/csf.2009.6
发表时间：
2009
期刊：
2009 22nd IEEE Computer Security Foundations Symposium
影响因子：
--
作者：
P. Schaller;Benedikt Schmidt;D. Basin;Srdjan Capkun
通讯作者：
Srdjan Capkun
逻辑框架
DOI：
10.1016/b978-044450813-3/50019-9
发表时间：
2001
期刊：
First International Conference on Security and Privacy for Emerging Areas in Communications Networks (SECURECOMM'05)
影响因子：
--
作者：
F. Pfenning
通讯作者：
F. Pfenning
DOI：
--
发表时间：
2008-03
期刊：
--
影响因子：
--
作者：
O. Grumberg;T. Nipkow;C. Pfaller
通讯作者：
O. Grumberg;T. Nipkow;C. Pfaller
DOI：
10.1006/inco.2000.2858
发表时间：
1996
期刊：
First International Conference on Security and Privacy for Emerging Areas in Communications Networks (SECURECOMM'05)
影响因子：
--
作者：
D. Basin;S. Matthews
通讯作者：
S. Matthews