随着移动通信技术的发展,5G的部署和实施正在逐步进行,5G相关的安全性问题成为研究人员和广大用户的关注焦点。但是由于5G仿真网络并未实现,目前通信系统的安全性研究仍旧以LTE网络的仿真测试为主,针对5G网络进行安全性分析的研究较少。而作为系统安全基础的认证和密钥协商协议,其安全性是5G安全的核心问题,并且存在工具可以对其进行安全性分析。本文借助TAMARIN证明程序对EAP-AKA’协议进行建模分析,从保密属性和身份认证属性两个角度出发,考虑不同安全假设下的属性满足程度,对于违反的安全属性,进一步分析可能的攻击路径以及攻击存在的原因,并提出可行的安全加固方法。本文主要工作包含以下四点:（1）分析认证和密钥协商协议相关规范,总结至少应满足的安全属性。将安全属性归纳为保密属性和身份认证属性两种。身份认证属性根据Lowe分类法进行不同级别的认证判断,保密属性分为保密性和前向保密性两种级别。（2）提出六种不同的安全假设,根据TAMARIN使用手册建立模型对不同安全假设下的安全属性进行验证。（3）观察并分析TAMARIN返回的安全属性验证结果。对于违反的安全属性,考虑属性违反的原因以及可能导致的攻击类型。（4）针对攻击类型提出可行的安全加固方法,并进行理论分析或实验验证。