基于Tamarin Prover的5G EAP-TLS协议的形式化分析

为了保证5G专用网络中移动设备的通信安全，第三代合作伙伴计划（3rd generation partnership project, 3GPP）提出了5G可扩展认证协议-传输层安全（extensible authentication protocol-transport layer security, EAP-TLS）。然而，现有的针对于5G EAP-TLS协议的研究工作较少且缺乏系统性。因此，对5G EAP-TLS协议进行详细的描述，并对该协议进行全面的形式化建模。对5G规范中涉及的所有协议实体以及证书分发机制进行建模，同时从5G规约中提取并建模了与5G EAPTLS协议相关的安全目标。提出证据搜索策略引导符号分析工具Tamarin Prover进行自动化证据搜索，解决了Tamarin Prover在验证复杂模型时验证过程无法终止的问题，实现了5G EAP-TLS安全目标的自动化验证。通过分析验证结果，发现了5G EAP-TLS协议能够满足机密性目标，但难以满足一些认证性目标，同时，揭示了协议存在拒绝服务（denial of service,DoS）攻击和用户通信数据泄露的隐患。针对...