5G网络认证与密钥协商协议的形式化验证与分析  

Formal Verification and Analysis of Authentication and Key Agreement for 5G Networks

作　　者：杨成龙 杨晋吉[1] 苏桂钿 管金平 YANG Cheng-Long;YANG Jin-Ji;SU Gui-Tian;GUAN Jin-Ping(School of Computer Science,South China Normal University,Guangzhou 510631,China)

机构地区：[1]华南师范大学计算机学院,广州510631

出　　处：《计算机系统应用》2022年第12期398-404,共7页Computer Systems & Applications

基　　金：广东省自然科学基金(2020A1515010445)

摘　　要：网络攻击的手段层出不穷,如中间人攻击,重放攻击,DoS攻击等,以此获取不当利益.密钥协商协议的设立是为合法用户提供正确认证入口,并拒绝攻击者的非法接入和攻击.密钥协商协议是保护移动通信提高服务质量的第一道安全防线,5G网络密钥协商协议在实际环境中仍然存在安全隐患,其协议本身的安全特性能否满足要求仍未可知,本文提出使用基于概率模型检测的方法,通过对5G网络密钥协商协议的各协议方实体进行建模,建立离散时间马尔科夫链模型,在建模过程中考虑外界的攻击影响,引入攻击率来描述外界的影响程度,通过攻击率对5G网络密钥协商协议的研究进行定量分析,使用概率计算树逻辑对待验属性规约进行编码描述,利用概率模型检测工具PRISM进行实验.实验结果表明:在引入攻击率的5G网络密钥协商协议模型中,5G网络密钥协商协议各协议方实体所受攻击的影响对该协议的时延性,有效性,保密性等属性规约的性能有不同程度的影响,因此,研究外界网络攻击对协议的安全性能的影响,对加强协议安全性能及其改进具有一定借鉴意义,并对5G网络密钥协商协议的安全特性的提升和保护用户的经济与信息安全具有很大的意义.There are numerous methods of network attacks,such as man-in-the-middle attacks,replay attacks,and DoS attacks,which are ways to gain improper benefits.The authentication and key agreement(AKA)is set up to provide a correct authentication portal for legitimate users and deny illegal access and attacks from attackers.AKA is the first line of security to protect mobile communications for higher quality of service.The AKA for 5G networks still has security problems in the actual environment,and it is still unknown whether the security features of AKA can meet the requirements.Therefore,this study proposes to use the method based on probabilistic model checking to build a discretetime Markov chain model by modeling each protocol party entity of AKA for 5G networks.In the modeling process,the influence of external attacks is considered,and the attack rate is introduced to describe the degree of external influence.The studies of AKA for 5G networks are quantitatively analyzed through the attack rate,and the probabilistic computation tree logic is employed to describe the codes of the specifications for the a priori attributes.Experiments are conducted by the probabilistic model checking tool PRISM.The experimental results indicate that in the AKA model with the introduction of the attack rate,the attacks on each protocol party entity of AKA for 5G networks have different influences on the performance of the attribute specifications such as delay,validity,and confidentiality of the protocol.Therefore,the study of the impact of external network attacks on the security performance of the protocol has certain implications for strengthening the security performance of the protocol and its improvement,and it is of great significance to enhance the security features of AKA for 5G networks and protect the economic and information security of users.

关 键 词：概率模型检测 5G网络 认证与密钥协商协议 形式化验证 PRISM 

分 类 号：TN929.5[电子电信—通信与信息系统] TN918.4[电子电信—信息与通信工程]