Thread 中 Mesh 网络配置协议的符号化安全验证（扩展版）
密码学与安全
2023-12-21 v1 符号计算
摘要
Thread 协议是物联网中一种流行的网络协议。它允许一组应用和协议的无缝集成，从而降低了不同应用或用户协议之间不兼容的风险。Thread 已被大多数物联网制造商部署在许多流行的智能家居产品中，例如 Apple TV、Apple HomePod mini、eero 6、Nest Hub 和 Nest Wifi。尽管对 Thread 的安全性已有一些经验分析，但对这一蓬勃发展的物联网生态系统的基础设施仍缺乏形式化分析。在本研究中，我们对 Thread 的安全属性进行了形式化的符号化分析。我们的主要关注点是 MeshCoP（Mesh Commissioning Protocol），它是 Thread 中用于在现有 Thread 网络内对新加入的、不受信任的设备进行安全认证和配置的主要子协议。本案例研究展示了在建模 MeshCoP 时面临的挑战及提出的解决方案。我们使用 ProVerif（一种 -演算模型的符号化验证工具）来验证 MeshCoP 的安全属性。
引用
@article{arxiv.2312.12958,
title = {Symbolic Security Verification of Mesh Commissioning Protocol in Thread (extended version)},
author = {Pankaj Upadhyay and Subodh Sharma and Guangdong Bai},
journal= {arXiv preprint arXiv:2312.12958},
year = {2023}
}
备注
18 pages