[Resource Topic] 2025/2067: Cryptographic Binding Should Not Be Optional: A Formal-Methods Analysis of FIDO UAF Channel Binding

Welcome to the resource topic for 2025/2067

Title:
Cryptographic Binding Should Not Be Optional: A Formal-Methods Analysis of FIDO UAF Channel Binding

Authors: Enis Golaszewski, Alan T. Sherman, Edward Zieglar, Jonathan D. Fuchs, Sophia Hamer

Abstract:

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.

ePrint: https://eprint.iacr.org/2025/2067

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .