密码学绑定不应是可选的：对FIDO UAF信道绑定的形式方法分析
密码学与安全
2025-11-11 v1
摘要
作为密码学绑定的一个案例研究，我们对Fast IDentity Online（FIDO）Universal Authentication Framework (UAF)身份验证协议中的密码学信道绑定机制进行了形式方法分析，该框架旨在减少对传统密码的使用，转而依赖身份验证设备。首先，我们展示了UAF的信道绑定未能缓解来自Dolev-Yao攻击者的协议交互，攻击者可以将服务器的身份验证挑战转移到协议的其他会话中。结果，在某些情况下，攻击者可以冒充客户端与服务器（例如，银行服务器）建立已认证会话。其次，我们在eBay开源FIDO UAF实现上实现了一个概念证中间人攻击。第三，我们提出并形式化地验证了对UAF的改进。我们分析的弱点与25年前在Needham-Schroeder协议中发现的漏洞类似。这一发现暴露了协议设计者正确绑定消息并使用形式方法工具分析其设计的强烈需求。到我们知识中，本文是首次对UAF信道绑定进行形式方法分析，也是首次展示了利用UAF信道绑定弱点的攻击细节。本案例研究说明了将上下文密码学地绑定到协议消息中以防止攻击者在上下文之外滥用消息的重要性。
引用
@article{arxiv.2511.06028,
title = {Cryptographic Binding Should Not Be Optional: A Formal-Methods Analysis of FIDO UAF Channel Binding},
author = {Enis Golaszewski and Alan T. Sherman and Edward Zieglar and Jonathan D. Fuchs and Sophia Hamer},
journal= {arXiv preprint arXiv:2511.06028},
year = {2025}
}
备注
A shorter version of this paper will appear in the Proceedings of Security Standardisation Research (SSR) 2025, published by Springer in the LNCS series