典型文献
基于Tamarin的5G AKA协议形式化分析及其改进方法
文献摘要：
对于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种情况没有得到满足.最后针对协议不满足的鉴权性质,本文采用了三种修改方法来对协议模型进行改进,并对改进前后的验证结果进行了分析总结.
文献关键词：
鉴权协议;5G AKA协议;Lowe分类法;形式化分析;Tamarin
中图分类号：
作者姓名：
刘镝;王梓屹;李大伟;关振宇;孙钰;刘建伟
作者机构：
北京航空航天大学 网络空间安全学院, 北京 100191
文献出处：
引用格式：
[1]刘镝;王梓屹;李大伟;关振宇;孙钰;刘建伟-.基于Tamarin的5G AKA协议形式化分析及其改进方法)[J].密码学报,2022(02):237-247
A类：
Tamarin,v17,KSEAF,SUPI,SNID,鉴权协议
B类：
AKA,形式化分析,改进方法,移动通信网络,3GPP,身份认证,密钥协商,使用安全,安全协议,验证工具,TS,形式化建模,保密性,Lowe,锚点,共享密钥,单射,一共,修改方法,进前,分类法
AB值：
0.261948
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
