论文标题
对受限物联网设备的EDHOC关键建立的正式分析
Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices
论文作者
论文摘要
受限制的物联网设备在社会中变得无处不在，并且需要安全的通信协议，以尊重这些设备运行的约束。 EDHOC是针对受约束IoT设备的经过身份验证的关键建立协议，目前由Internet工程工作组（IETF）标准化。 EDHOC的基本版本仅在2018年正式分析了两种关键建立方法。从那时起，该协议已经显着发展，并添加了几种新的关键建立方法。在本文中，我们在增强的符号Dolev-yao模型中使用tamarin工具介绍了对所有EDHOC方法的正式分析。我们表明，并非所有方法都满足了认识的身份验证概念，但它们都满足了隐性身份验证的概念，以及对会话关键材料的完美远期保密（PFS）。我们确定提出改进的其他弱点。例如，一方可能打算与某个同行建立会话密钥，但最终与另一个值得信赖但受到妥协的同伴建立了会话密钥。我们向IETF传达了我们的发现和建议，该发现将其中一些纳入了标准的较新版本。
Constrained IoT devices are becoming ubiquitous in society and there is a need for secure communication protocols that respect the constraints under which these devices operate. EDHOC is an authenticated key establishment protocol for constrained IoT devices, currently being standardized by the Internet Engineering Task Force (IETF). A rudimentary version of EDHOC with only two key establishment methods was formally analyzed in 2018. Since then, the protocol has evolved significantly and several new key establishment methods have been added. In this paper, we present a formal analysis of all EDHOC methods in an enhanced symbolic Dolev-Yao model using the Tamarin tool. We show that not all methods satisfy the authentication notion injective of agreement, but that they all do satisfy a notion of implicit authentication, as well as Perfect Forward Secrecy (PFS) of the session key material. We identify other weaknesses to which we propose improvements. For example, a party may intend to establish a session key with a certain peer, but end up establishing it with another, trusted but compromised, peer. We communicated our findings and proposals to the IETF, which has incorporated some of these in newer versions of the standard.
