一个切换认证的5G鉴权协议及其形式化分析  

5G Authentication Protocol Based on Sub-mode Switching Operation and Its Formal Analysis

作　　者：刘逸冰 周刚 LIU Yi-Bing;ZHOU Gang(School of Data and Target Engineering,PLA Information Engineering University,Zhengzhou 450002,China)

机构地区：[1]中国人民解放军信息工程大学数据与目标工程学院,河南郑州450002

出　　处：《软件学报》2023年第8期3708-3725,共18页Journal of Software

摘　　要：随着移动通信的发展,迎来了第5代移动通信技术(5G).5G认证与密钥协商(5G authentication and key agreement,5G-AKA)协议的提出主要是为了实现用户和服务网络的双向鉴权.然而,最近的研究认为其可能会遭受信息破译和消息重放攻击.同时,发现当前5G-AKA的一些变种不能满足协议的无连接性.针对上述缺陷,提出一个改进方案:SM-AKA.SM-AKA由两个并行子协议组成,通过巧妙的模式切换使更加轻量的子协议(GUTI子模块)被频繁采用,而另一个子协议(SUPI子模块)则主要用于异常发生时的鉴权.依据这种机制,它不仅实现用户和归属网之间的高效认证,还能提升鉴权的稳定性.此外,变量的新鲜性也得到有效维持,可以防止消息的重放,而严格的加解密方式进一步提升协议的安全性.最后,对SM-AKA展开完整的评估,通过形式建模、攻击假定和Tamarin推导,证明该方案可以达到鉴权和隐私目标,而理论分析部分也论证了协议性能上的优势.With the development of the Internet,the 5th generation(5G)of mobile communication technology emerges.The 5G authentication and key agreement(5G-AKA)protocol is proposed mainly to achieve two-way authentication between users and service networks.However,recent research suggests that the protocol may be subject to information deciphering and message replay attacks.At the same time,it is found that some variants of the current 5G-AKA cannot satisfy the protocol’s unlinkability.Therefore,in response to these shortcomings,this study proposes an improvement plan called SM-AKA.SM-AKA is composed of two parallel sub-protocols in a novel way.In addition,through the flexible mode switching,lightweight sub-protocols(GUTI submodule)are frequently adopted,and the other sub-protocol(SUPI submodule)is used to deal with abnormalities caused by authentication.Therefore,this mechanism not only realizes the efficient authentication between users and networks but also improves the stability of the protocol.Furthermore,the freshness of variables has been effectively maintained to prevent the replay of messages,and strict encryption and decryption methods have further strengthened the security of the protocol.Finally,the study carries out a complete evaluation of SM-AKA.Through formal modeling,attack assumptions,and Tamarin derivation,it is proved that the plan can achieve the authentication and privacy goals,and the theoretical analysis has demonstrated the performance advantage of the protocol.

关 键 词：5G鉴权 认证协议 形式化分析 移动网络 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]