本文对FIDO2、CTAP 2.1和WebAuthn 2这一现代无密码认证协议族进行了形式化安全分析，并提出了后量子安全的实例化方案。研究者首先构建了这些协议的符号模型，涵盖了注册、认证、凭证管理等多阶段交互，并利用Tamarin Prover工具进行了自动化安全验证。分析揭示了在标准安全假设下协议能够满足预期的安全属性（如抗钓鱼、密钥泄露保护、绑定认证等），但发现了在特定场景下存在的设计缺陷，例如CTAP 2.1中某些消息序列可能导致不安全的凭证共享。基于这些发现，论文提出了两方面的贡献：一是给出了一个增强的、可证明安全的协议规范修正；二是引入了后量子密码原语（如基于格的签名方案），对协议进行了后量子安全实例化，并证明了其在量子计算机威胁下的安全性。实验评估表明，后量子实例化在性能开销上可接受，兼容现有硬件。该工作为大规模部署无密码认证提供了坚实的理论基础和工程指导。