【摘要】5G网络发展迅速,作为系统安全基础的认证和密钥协商协议,其安全性是5G安全的核心问题。该文借助TAMARIN证明程序对5G网络中的EAP-AKA′协议进行建模分析。通过分析协议规范将安全性需求归纳为保密属性和认证属性两种安全属性,利用TAMARIN建立模型来验证不同安全属性的满足程度。根据TAMARIN证明程序返回的验证结果,该文发现了SEAF与AUSF间关于SNID的单射一致性违反以及锚定密钥K_(SEAF)前向保密性的违反,从而发现了重放攻击、身份验证同步失败攻击以及锚定密钥K_(SEAF)泄露攻击,并针对这些攻击提出了相应的安全加固方法,最后对方法进行理论分析和实验验证。