5G网络认证与密钥协商协议的形式化验证与分析
作者:
基金项目:

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


Formal Verification and Analysis of Authentication and Key Agreement for 5G Networks
Author:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [18]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    网络攻击的手段层出不穷, 如中间人攻击, 重放攻击, DoS攻击等, 以此获取不当利益. 密钥协商协议的设立是为合法用户提供正确认证入口, 并拒绝攻击者的非法接入和攻击. 密钥协商协议是保护移动通信提高服务质量的第一道安全防线, 5G网络密钥协商协议在实际环境中仍然存在安全隐患, 其协议本身的安全特性能否满足要求仍未可知, 本文提出使用基于概率模型检测的方法, 通过对5G网络密钥协商协议的各协议方实体进行建模, 建立离散时间马尔科夫链模型, 在建模过程中考虑外界的攻击影响, 引入攻击率来描述外界的影响程度, 通过攻击率对5G网络密钥协商协议的研究进行定量分析, 使用概率计算树逻辑对待验属性规约进行编码描述, 利用概率模型检测工具PRISM进行实验. 实验结果表明: 在引入攻击率的5G网络密钥协商协议模型中, 5G网络密钥协商协议各协议方实体所受攻击的影响对该协议的时延性, 有效性, 保密性等属性规约的性能有不同程度的影响, 因此, 研究外界网络攻击对协议的安全性能的影响, 对加强协议安全性能及其改进具有一定借鉴意义, 并对5G网络密钥协商协议的安全特性的提升和保护用户的经济与信息安全具有很大的意义.

    Abstract:

    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 discrete-time 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.

    参考文献
    [1] 邱勤, 张滨, 吕欣. 5G安全需求与标准体系研究. 信息安全研究, 2020, 6(8): 673–679. [doi: 10.3969/j.issn.2096-1057.2020.08.002
    [2] 胡鑫鑫, 刘彩霞, 彭亚斌, 等. 5G鉴权认证协议的安全性研究. 无线电通信技术, 2020, 46(4): 405–411. [doi: 10.3969/j.issn.1003-3114.2020.04.006
    [3] 齐旻鹏, 彭晋. 5G网络的认证体系. 中兴通讯技术, 2019, 25(4): 14–18. [doi: 10.12142/ZTETJ.201904003
    [4] 陆峰, 郑康锋, 钮心忻, 等. 3GPP认证与密钥协商协议安全性分析. 软件学报, 2010, 21(7): 1768–1782
    [5] 纪韬. 5G网络中身份认证协议研究[硕士学位论文]. 西安: 西安电子科技大学, 2018.
    [6] Arapinis M, Mancini L, Ritter E, et al. New privacy issues in mobile telephony: Fix and verification. Proceedings of the 2012 ACM Conference on Computer and Communications Security. North Carolina: ACM, 2012. 205–216.
    [7] Borgaonkar R, Hirschi L, Park S, et al. New privacy threat on 3G, 4G, and upcoming 5GAKA protocols. Proceedings on Privacy Enhancing Technologies, 2019, 2019(3): 108–127. [doi: 10.2478/popets-2019-0039
    [8] Hahn C, Kwon H, Kim D, et al. A privacy threat in 4th generation mobile telephony and its countermeasure. Proceedings of the 9th International Conference on Wireless Algorithms, Systems, and Applications. Harbin: Springer, 2014. 624–635.
    [9] Hussain SR, Chowdhury O, Mehnaz S, et al. LTEInspector: A systematic approach for adversarial testing of 4G LTE. Proceedings of the 25th Annual Network and Distributed System Security Symposium. San Diego: The Internet Society, 2018.
    [10] Basin D, Dreier J, Hirschi L, et al. A formal analysis of 5G authentication. Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. Toronto: ACM, 2018. 1383–1396.
    [11] Koutsos A. The 5GAKA authentication protocol privacy. Proceedings of the 2019 IEEE European Symposium on Security and Privacy (EuroS&P). Stockholm: IEEE, 2019. 464–479.
    [12] 李晓逸. 5G认证协议设计及形式化验证[硕士学位论文]. 北京: 北京交通大学, 2021.
    [13] Ferrag MA, Maglaras L, Argyriou A, et al. Security for 4G and 5G cellular networks: A survey of existing authentication and privacy-preserving schemes. Journal of Network and Computer Applications, 2018, 101: 55–82. [doi: 10.1016/j.jnca.2017.10.017
    [14] 夏奴奴, 杨晋吉, 赵淦森, 等. 基于概率模型的云辅助的轻量级无证书认证协议的形式化验证. 计算机科学, 2019, 46(8): 206–211. [doi: 10.11896/j.issn.1002-137X.2019.08.034
    [15] Kwiatkowska M, Norman G, Parker D. Advances and challenges of probabilistic model checking. Proceedings of the 2010 48th Annual Allerton Conference on Communication, Control, and Computing. Monticello: IEEE, 2010. 1691–1698.
    [16] Sharir M, Pnueli A, Hart S. Verification of probabilistic programs. SIAM Journal on Computing, 1984, 13(2): 292–314. [doi: 10.1137/0213021
    [17] Liu LY, Hasan O, Tahar S. Formal reasoning about finite-state discrete-time Markov chains in HOL. Journal of Com-puter Science and Technology, 2013, 28(2): 217–231. [doi: 10.1007/s11390-013-1324-6
    [18] Kwiatkowska M, Norman G, Parker D. PRISM 4.0: Verification of probabilistic real-time systems. Proceedings of the 23rd International Conference on Computer Aided Verification. Snowbird: Springer, 2011. 585–591.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

杨成龙,杨晋吉,苏桂钿,管金平.5G网络认证与密钥协商协议的形式化验证与分析.计算机系统应用,2022,31(12):398-404

复制
分享
文章指标
  • 点击次数:791
  • 下载次数: 2020
  • HTML阅读次数: 1511
  • 引用次数: 0
历史
  • 收稿日期:2022-06-03
  • 最后修改日期:2022-08-19
  • 在线发布日期: 2022-10-28
文章二维码
您是第11207290位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京海淀区中关村南四街4号 中科院软件园区 7号楼305房间,邮政编码:100190
电话:010-62661041 传真: Email:csa (a) iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号