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

TL;DR

The paper applies formal-methods analysis (CPSA) to FIDO UAF 1.2 channel binding, showing that several binding variants fail to prevent protocol interactions that enable MITM attacks. It demonstrates a practical attack against eBay's open-source UAF server and formalizes security goals as session-context injective agreements, revealing which bindings preserve these goals under a DY adversary. The authors propose and formally verify improvements, including TLS1.3 exporter binding and a dual-binding approach, to robustly tie challenges to TLS sessions. They argue for mandatory, properly verified cryptographic bindings and highlight the value of formal methods in protocol design to avert historical vulnerabilities like those seen in NS. The work emphasizes adopting stronger bindings and proactive verification to improve the security of broad, password-replacing authentication standards.

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.

Figures (10)

• Figure 1: Architecture of UAF authentication using a pre-registered, embedded authenticator. The server issues a challenge to the client, who incorporates that challenge into a final challenge and transmits it to the authenticator (Auth). Using the authentication secret key, the authenticator signs an assertion, which the client transmits to the server to complete authentication. The server verifies the assertion using the authentication public key that it obtains when the client registers the authenticator. The attestation process in UAF registration reflects a similar structure. In our analysis, we assume that the adversary cannot manipulate local device communication between the client and their authenticator.
• Figure 2: Challenge-reissuing attack during UAF authentication: CPSA shape for UAF authentication under the server's cryptographic assumptions. When the client omits channel binding, or includes one of the standard UAF bindings in tlsData, the client acts as a confused deputy and produces an attestation for the adversary. This shape reveals the following structural weakness: in two scenarios, the adversary can masquerade as the client to the server, or transplant messages from one session to another between the same endpoints. In particular, the adversary can masquerade as the client when the client omits channel binding in the tlsData, or when the server fails to verify this binding. The adversary can transplant messages between such sessions because the client binds only to the endpoints of the channel and not to the session.
• Figure 3: Idealized message sequence diagram of UAF registration over a network. Vertical lines correspond to protocol roles; horizontal arrows indicate message flows from one role to another; and arrow labels indicate message contents. Information in boxes specify local processing for each role. The client and server communicate over a pre-negotiated TLS channel. The client communicates with the authenticator via the Authenticator-Specific Module (ASM) API. The authenticator signs $s$ using the attestation key corresponding to the attestation certificate that the manufacturer loads on the device.
• Figure 4: Idealized message sequence diagram of UAF authentication over a network. As in registration, the client and server communicate over a pre-negotiated TLS channel, and the client communicates with the authenticator using a local API. The authenticator signs $s$ using $K_{priv}$, which it recalls from a successful run of the registration protocol.
• Figure 5: CPSA specification of a client-reg role in UAF registration without channel binding, using TLS 1.2. A role consists of variable definitions and a trace expressing terms that a strand sends and receives from the network. Variable definitions comprise s-expressions that list labels followed by a sort (type). The macro TLS generates client terms to establish a TLS session with the server. The macro UAF_Reg_Unbound_TLS12 generates client terms that carry out UAF registration using a specific binding method and TLS version. To model alternative versions, we substitute the TLS macro to generate terms for TLS 1.2 or TLS 1.3, and substitute the UAF macro for the desired binding and TLS version. To model the auth-reg role, we reverse the sign of each term by altering the order of the send and recv inputs to the macros.

Theorems & Definitions (14)

• definition thmcounterdefinition: Successful Completion
• definition thmcounterdefinition: Unique Completion
• theorem thmcountertheorem
• proof : Proof (By enumeration).
• theorem thmcountertheorem
• proof : Proof (By counterexample).
• theorem thmcountertheorem
• proof : Proof (By enumeration).
• theorem thmcountertheorem
• proof : Proof (By enumeration).