摘要
5G网络发展迅速,作为系统安全基础的认证和密钥协商协议,其安全性是5G安全的核心问题。该文借助TAMARIN证明程序对5G网络中的EAP-AKA'协议进行建模分析。通过分析协议规范将安全性需求归纳为保密属性和认证属性两种安全属性,利用TAMARIN建立模型来验证不同安全属性的满足程度。根据TAMARIN证明程序返回的验证结果,该文发现了SEAF与AUSF间关于SNID的单射一致性违反以及锚定密钥K_(SEAF)前向保密性的违反,从而发现了重放攻击、身份验证同步失败攻击以及锚定密钥K_(SEAF)泄露攻击,并针对这些攻击提出了相应的安全加固方法,最后对方法进行理论分析和实验验证。
5G networks are developing rapidly.The security of the authentication and key agreement protocols is the core issue of 5G security.The TAMARIN prover is used here to analyze the EAP-AKA'protocol for 5G networks.The protocol specifications are analyzed to identify the security requirements as a confidential attribute and an authentication attribute.A model is then established according to the TAMARIN standard to verify that these security attributes are satisfied.The verification results show a single shot consistency violation between SEAF and AUSF regarding SNID and a violation of the forward secrecy of the anchor key K_(SEAF),which may lead to the network experiencing replay attacks,authentication synchronization failure attacks,and Anchor key K_(SEAF) leak attacks.Security hardening methods are then presented for these attacks with theoretical and experimental verification.
作者
贾凡
严妍
袁开国
赵璐婧
JIA Fan;YAN Yan;YUAN Kaiguo;ZHAO Lujing(School of Electronic and Information Engineering,Beijing Jiaotong University,Beijing 100044,China;China Cybersecurity Review Technology and Certification Center,Beijing 100020,China;School of Cyberspace Security,Beijing University of Posts and Telecommunication,Beijing 100876,China)
出处
《清华大学学报(自然科学版)》
EI
CAS
CSCD
北大核心
2021年第11期1260-1266,共7页
Journal of Tsinghua University(Science and Technology)
基金
国家自然科学基金资助项目(61872033)。