引用本文:刘逸冰,周刚.一个切换认证的5G鉴权协议及其形式化分析.软件学报,2023,34(8):3708-3725
【打印本页】   【下载PDF全文】   查看/发表评论  【EndNote】   【RefMan】   【BibTex】
←前一篇|后一篇→ 过刊浏览    高级检索
本文已被:浏览 1990次   下载 4766 本文二维码信息
码上扫一扫!
分享到: 微信 更多
一个切换认证的5G鉴权协议及其形式化分析
刘逸冰, 周刚
中国人民解放军信息工程大学 数据与目标工程学院, 河南 郑州 450002
摘要:
随着移动通信的发展, 迎来了第5代移动通信技术(5G). 5G认证与密钥协商 (5G authentication and key agreement, 5G-AKA)协议的提出主要是为了实现用户和服务网络的双向鉴权. 然而, 最近的研究认为其可能会遭受信息破译和消息重放攻击. 同时, 发现当前5G-AKA的一些变种不能满足协议的无连接性. 针对上述缺陷, 提出一个改进方案: SM-AKA. SM-AKA由两个并行子协议组成, 通过巧妙的模式切换使更加轻量的子协议(GUTI子模块)被频繁采用, 而另一个子协议(SUPI子模块)则主要用于异常发生时的鉴权. 依据这种机制, 它不仅实现用户和归属网之间的高效认证, 还能提升鉴权的稳定性. 此外, 变量的新鲜性也得到有效维持, 可以防止消息的重放, 而严格的加解密方式进一步提升协议的安全性. 最后, 对SM-AKA展开完整的评估, 通过形式建模、攻击假定和Tamarin推导, 证明该方案可以达到鉴权和隐私目标, 而理论分析部分也论证了协议性能上的优势.
关键词:  5G鉴权  认证协议  形式化分析  移动网络
DOI:10.13328/j.cnki.jos.006617
分类号:TP311
基金项目:
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
Abstract:
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.
Key words:  5G authentication  authentication protocol  formal analysis  mobile network

引用本文:
【打印本页】   【下载PDF全文】   查看/发表评论  【EndNote】   【RefMan】   【BibTex】
←前一篇|后一篇→ 过刊浏览    高级检索
本文已被:浏览次   下载  
分享到: 微信 更多
摘要:
关键词:  
DOI:
分类号:
基金项目:
Abstract:
Key words: