研究机构：北京邮电大学
论文出处：NDSS，网络与信息安全A会
2.论文总结
FIDO协议套件旨在实现用户通过本地可信认证器登录远程服务。采用FIDO的依赖服务无需存储用户自主选择的密钥或其哈希值，从而显著降低了电子商务领域中的潜在攻击面。鉴于该协议的其日益普及，系统性地验证FIDO的安全性承诺变得尤为重要。
本文通过形式化定义其安全假设与目标，并在不同场景下采用ProVerif对FIDO UAF协议进行全面的系统验证，提出了详细的分析。研究结果明确了确保FIDO UAF各安全目标成立所需的最小安全假设，还通过自动化验证了先前发现的漏洞，并揭示了若干新型攻击模式。在形式验证的指导下，作者还发现了两款主流Android FIDO应用中的两类实际攻击，并向供应商披露了这些漏洞。此外，本文还提出了若干具体建议，以修复协议中存在的问题与弱点，增强其安全性。
3.UAF协议概述
UAF协议主要包括认证器注册与认证两个核心操作，在这一部分，主要介绍了UAF协议的工作流程。
4.威胁模型和安全目标
为了进行更全面的分析，作者基于涵盖更为现实场景的安全假设下进行了研究分析。
5.Proveif建模UAF协议
在本节中，简要介绍了形式验证工具ProVerif，并阐述了在ProVerif中对安全属性的建模方法。
6.安全分析
本节展示了UAF协议的形式化验证结果，实现了各安全目标所需的最小安全假设。
7.评价总结
本文对UAF协议进行了形式化分析。明确了该协议的安全假设与目标，构建了协议的形式化模型，并利用ProVerif在不同场景下对协议进行分析。研究明确了UAF协议各安全目标所需的最小安全假设，通过总结和分析ProVerif提供的结果，呈现了协议的缺陷并演示了若干攻击方式。此外，研究不仅以自动化方式验证了已知漏洞，并披露了若干新型攻击。基于分析结果，作者进一步提出了具体的协议改进建议，以修复协议中存在的安全问题和设计缺陷。