基于Tamarin的5GAKA协议形式化分析及其改进方法*
2022-10-31 18:15:12   来源：    点击：

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