As a case study in cryptographic binding, we present a formal-methods analysis of the cryptographic channel binding mechanisms in the Fast IDentity Online (FIDO) Universal Authentication Framework (UAF) authentication protocol, which seeks to reduce the use of traditional passwords in favor of authentication devices. First, we show that UAF's channel bindings fail to mitigate protocol interaction by a Dolev-Yao adversary, enabling the adversary to transfer the server's authentication challenge to alternate sessions of the protocol. As a result, in some contexts, the adversary can masquerade as a client and establish an authenticated session with a server (e.g., possibly a bank server). Second, we implement a proof-of-concept man-in-the-middle attack against eBay's open source FIDO UAF implementation. Third, we propose and formally verify improvements to UAF. The weakness we analyze is similar to the vulnerability discovered in the Needham-Schroeder protocol over 25 years ago. That this vulnerability appears in the FIDO UAF standard highlights the strong need for protocol designers to bind messages properly and to analyze their designs with formal-methods tools. To our knowledge, we are first to carry out a formal-methods analysis of channel binding in UAF and first to exhibit details of an attack on UAF that exploits the weaknesses of UAF's channel binding. Our case study illustrates the importance of cryptographically binding context to protocol messages to prevent an adversary from misusing messages out of context.

翻译：作为密码学绑定的案例研究，我们对快速身份在线（FIDO）通用认证框架（UAF）认证协议中的密码学信道绑定机制进行了形式化方法分析，该协议旨在减少传统密码的使用，转而采用认证设备。首先，我们证明UAF的信道绑定无法缓解Dolev-Yao攻击者引发的协议交互问题，使得攻击者能够将服务器的认证质询转移到协议的其他会话中。因此，在某些场景下，攻击者可以伪装成客户端并与服务器（例如可能是银行服务器）建立认证会话。其次，我们针对eBay的开源FIDO UAF实现实施了概念验证的中间人攻击。第三，我们提出并形式化验证了对UAF的改进方案。我们分析的这一弱点与25年前在Needham-Schroeder协议中发现的漏洞相似。该漏洞出现在FIDO UAF标准中，突显了协议设计者必须正确绑定消息并使用形式化方法工具分析其设计的迫切需求。据我们所知，我们是首个对UAF信道绑定进行形式化方法分析的研究，也是首个详细展示利用UAF信道绑定弱点实施攻击的研究。我们的案例研究说明了将上下文密码学绑定至协议消息的重要性，以防止攻击者在上下文之外滥用消息。