基于Tamarin的5G AKA协议形式化分析及其改进方法

• 作者: 刘镝 王梓屹 李大伟 关振宇 孙钰 刘建伟
• 来源期刊: 密码学报
• 学科: 工学
• 关键词: 鉴权协议 5G AKA协议 Lowe分类法 形式化分析 Tamarin
• 年，卷（期）: 2022,（2）
• 页码范围: 237-247
• 页数: 11页
• 分类号: TP309.7
• 语种: 中文
• DOI: 10.13868/j.cnki.jcr.000515

摘要

对于5G移动通信网络,3GPP组织标准化了5G AKA等协议,用于身份认证和密钥协商.本文使用安全协议验证工具Tamarin对5G AKA协议进行了形式化分析.首先基于3GPP TS 33.501 v17.0.0版本,完成了对5G AKA协议及期望其满足的安全性质的形式化建模.安全性质考虑了保密性质和Lowe鉴权性质,保密性质包括安全锚点密钥KSEAF和长期共享密钥K的保密性,鉴权性质包括协议参与实体之间在参数SUPI、SNID、KSEAF上的非单射一致性,以及在KSEAF上的单射一致性.然后本文在Tamarin中验证了5G AKA协议是否满足相关安全性质,发现保密性质全部得到满足,鉴权性质一共验证了36种情况,其中有23种情况没有得到满足.最后针对协议不满足的鉴权性质,本文采用了三种修改方法来对协议模型进行改进,并对改进前后的验证结果进行了分析总结.