对 5G 认证的正式分析
密码学与安全
2020-01-13 v4
摘要
移动通信网络连接了世界上大部分人口。用户通话、短信和移动数据的安全性取决于所采用的认证密钥交换协议提供的保证。对于下一代网络（5G），3GPP 小组为此标准化了 5G AKA 协议。我们提供了 AKA 家族中协议的首个全面形式化模型：5G AKA。我们还从定义 5G 的 3GPP 标准中提取了精确需求，并识别出缺失的安全目标。利用安全协议验证工具 Tamarin，我们针对 5G 安全目标对模型进行了完整、系统的安全评估。我们的自动化分析识别了每个安全目标所需的最小安全假设，并发现某些关键安全目标无法达成，除非在标准之外附加额外假设。最后，我们针对所发现的攻击与弱点提出了具有可证明安全修复的明确建议。
引用
@article{arxiv.1806.10360,
title = {A Formal Analysis of 5G Authentication},
author = {David Basin and Jannik Dreier and Lucca Hirschi and Saša Radomirović and Ralf Sasse and Vincent Stettler},
journal= {arXiv preprint arXiv:1806.10360},
year = {2020}
}
备注
Categories (ACM class 2012): Security and privacy - Formal methods and theory of security -- Security requirements -- Formal security models -- Logic and verification; Network protocols - Protocol correctness -- Formal specifications; Security and privacy - Network security -- Mobile and wireless security - Security services -- Privacy-preserving protocols