基于 Tamarin 的 5G AKA 协议形式化分析及其改进方法
本文主要介绍了基于 Tamarin 的 5G AKA 协议形式化分析及其改进方法。在 5G 移动通信网络中，3GPP 组织标准化了 5G AKA 协议，用以身份认证和密钥协商。文章使用安全协议验证工具 Tamarin 对 5G AKA 协议进行了形式化分析，并对协议进行了改进。
1. 5G AKA 协议的形式化建模
本文首先基于 3GPP TS 33.501v17.0.0 版本，完成了对 5G AKA 协议及期望其满足的安全性质的形式化建模。安全性质包括保密性质和 Lowe 鉴权性质。保密性质包括安全锚点密钥 KSEAF 和长期共享密钥 K 的保密性，鉴权性质包括协议参与实体之间在参数 SUPI、SNID、KSEAF 上的非单射一致性，以及在 KSEAF 上的单射一致性。
2. 5G AKA 协议的形式化分析
在 Tamarin 中验证了 5G AKA 协议是否满足相关安全性质，发现保密性质全部得到满足，但鉴权性质中只有 13 种情况满足，23 种情况没有得到满足。
3. 鉴权协议的改进方法
针对协议不满足的鉴权性质，本文采用了三种修改方法来对协议模型进行改进，然后对改进前后的验证结果进行了分析总结。
4. Lowe 分类法在 5G AKA 协议中的应用
Lowe 分类法是一种常用的鉴权协议分析方法，本文使用 Lowe 分类法对 5G AKA 协议进行了分析，并对协议的安全性质进行了评估。
5. Tamarin 工具在 5G AKA 协议形式化分析中的应用
Tamarin 是一种常用的安全协议验证工具，本文使用 Tamarin 工具对 5G AKA 协议进行了形式化分析，并对协议的安全性质进行了评估。
6. 5G AKA 协议的安全性质分析
本文对 5G AKA 协议的安全性质进行了分析，包括保密性质和鉴权性质，并对协议的安全性质进行了评估。
本文对 5G AKA 协议进行了形式化分析，并对协议进行了改进。研究结果表明，基于 Tamarin 的形式化分析可以有效地评估 5G AKA 协议的安全性质，并对协议进行改进，以提高协议的安全性。
