5G核心网作为下一代移动通信网络的核心，其访问控制机制的安全性至关重要。然而，由于5G核心网的复杂性，传统的安全分析手段难以全面覆盖其访问控制策略的潜在缺陷。本文提出5GCVerif，一个基于模型测试的形式化分析框架，专门用于分析5G核心网的访问控制机制。5GCVerif采用模块化设计，通过多种抽象技术构建能够捕捉5G核心网访问控制机制复杂细节的抽象模型，从而解决了模型检查中的状态爆炸问题。此外，5GCVerif通过将模型检查器的探索范围限制在有效的网络配置内，避免了为所有可能的核心网配置生成模型的难题。利用5GCVerif，作者评估了55个安全属性，发现了5个新的访问控制漏洞。这些漏洞可能导致未授权访问敏感信息、非法访问服务以及拒绝服务等多种攻击。该研究表明，形式化方法在发现5G核心网安全漏洞方面具有显著效果，为5G网络的安全设计和验证提供了有力工具。

本文针对厚移动虚拟网络运营商（Thick MVNO）在5G环境下面临的安全与隐私挑战，提出了一种名为PGUS（Pretty Good User Security）的安全框架。该框架的核心创新是引入了一种新的密码学原语——可净化盲签名（Sanitizable Blind Signature, SBS），并基于此设计了新的认证与密钥协商协议PGUS-AKA，以及无缝切换协议PGUS-HO。PGUS旨在保护厚MVNO环境中的所有通信安全，包括用户身份隐私、通信完整性和机密性。作者在通用可组合（UC）框架下进行了严格的形式化安全分析，证明协议能够抵抗多种关键威胁，如同谋攻击、重放攻击和中间人攻击。此外，在5G测试床上进行的实验评估表明，PGUS在计算开销、通信延迟和切换性能方面具有可行性，适用于下一代移动网络的实际部署。本文的主要贡献包括：首次将可净化盲签名引入移动网络认证领域，提出了完整的认证和切换协议，以及通过形式化分析和实验验证了方案的有效性。适合对5G安全、移动隐私保护和密码学协议设计感兴趣的研究人员阅读。