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

Formal Analysis and Improvement Methods of 5G AKA Protocol Based on Tamarin

作　　者：刘镝 王梓屹 李大伟 关振宇 孙钰 刘建伟 LIU Di;WANG Zi-Yi;LI Da-Wei;GUAN Zhen-Yu;SUN Yu;LIU Jian-Wei(School of Cyber Science and Technology,Beihang University,Beijing 100191,China)

机构地区：[1]北京航空航天大学网络空间安全学院,北京100191

出　　处：《密码学报》2022年第2期237-247,共11页Journal of Cryptologic Research

基　　金：国家重点研发计划(2021YFB2700200);国家自然科学基金(62002006,62172025,U21B2021,61932011,61932014,61972018,61972019,61772538,32071775,91646203);国防基础科研计划(JCKY2021211B017)。

摘　　要：对于5G移动通信网络,3GPP组织标准化了5G AKA等协议,用于身份认证和密钥协商.本文使用安全协议验证工具Tamarin对5G AKA协议进行了形式化分析.首先基于3GPP TS33.501 v17.0.0版本,完成了对5G AKA协议及期望其满足的安全性质的形式化建模.安全性质考虑了保密性质和Lowe鉴权性质,保密性质包括安全锚点密钥KSEAF和长期共享密钥K的保密性,鉴权性质包括协议参与实体之间在参数SUPI、SNID、KSEAF上的非单射一致性,以及在KSEAF上的单射一致性.然后本文在Tamarin中验证了5G AKA协议是否满足相关安全性质,发现保密性质全部得到满足,鉴权性质一共验证了36种情况,其中有23种情况没有得到满足.最后针对协议不满足的鉴权性质,本文采用了三种修改方法来对协议模型进行改进,并对改进前后的验证结果进行了分析总结.For 5G mobile communication networks,the 3GPP group has standardized protocols such as 5G AKA for identity authentication and key agreement.This paper applies Tamarin,a security protocol verification tool,to carry out a formal analysis of the 5G AKA protocol.Firstly,the formal modeling of the 5G AKA protocol and its expected security properties are accomplished based on 3GPP TS 33.501 v17.0.0 version.Security properties take secrecy properties and Lowe authentication properties into consideration.The secrecy properties include the secrecy of the security anchor key KSEAF and the long-term shared key K.The authentication properties include the non-injective agreement on the parameters SUPI,SNID,and KSEAF,and the injective agreement on the KSEAF between the parties of the protocol.This paper then verifies and confirms that the 5G AKA protocol satisfies the relevant security properties in the Tamarin,while the authentication properties are verified for a total of 36 cases,in which 23 cases are not satisfied.Finally,for the authentication properties that the protocol does not satisfy,this paper uses three modification methods to improve the protocol model,and analyzes and summarizes the verification results before and after the improvement.

关 键 词：鉴权协议 5GAKA协议 Lowe分类法 形式化分析 TAMARIN 

分 类 号：TP309.7[自动化与计算机技术—计算机系统结构]