s a case study in cryptographic binding, we present a formal-methods analysis of the Fast IDentity Online (FIDO) Universal Authentication Framework (UAF) authentication protocol's cryptographic channel binding mechanisms.
First, we show that UAF's channel bindings fail to mitigate protocol interaction by a Dolev-Yao (DY) 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, which
might be 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 verify an improvement of UAF channel binding that better resists protocol interaction, in which the client and the server, rather than the client alone, bind the server's challenge to the session.
The weakness we analyze is similar to the vulnerability discovered in the Needham-Schroeder protocol over 25 years ago. That this vulnerability appears in FIDO UAF highlights the strong need for protocol designers to bind messages properly and to analyze their designs with formal-methods tools.
UAF's channel bindings fail for four reasons: channel binding is optional;
the client cannot authenticate the server's challenge,
even when channel binding is used;
the standard permits the server to accept incorrect channel bindings; and
the protocol binds only to the communication endpoints and not to the protocol session.
We carry out our analysis of the standard and our suggested improvement using the Cryptographic Protocol Shapes Analyzer (CPSA).
To our knowledge, we are first to carry out a formal-methods analysis of channel binding in FIDO UAF, first to identify the structural weakness resulting from improper binding, and first to exhibit details of an attack resulting from this weakness.
In FIDO UAF, the client can cryptographically bind protocol data (including a server-generated authentication challenge) to the underlying authenticated communication channel.
To facilitate the protocol's adoption, the FIDO Alliance makes the channel binding optional and allows a server to accept incorrect channel bindings, such as when the client communicates through a network perimeter proxy.
Practitioners should be aware that, when omitting channel binding or accepting incorrect channel bindings, FIDO UAF is vulnerable to a protocol-interaction attack in which the adversary tricks the client and authenticator to act as confused deputies to sign an authentication challenge for the adversary.
In addition to enabling the server to verify the client's binding of the challenge to the channel, our improved mandatory dual channel-binding mechanism provides the following two advantages:
(1) By binding the challenge to the channel, the server provides an opportunity for the client to verify this binding. By contrast, in the current standard, the client cannot authenticate the server's challenge.
(2) It performs binding at the server where the authentication challenge is created, hindering an adversary from transplanting the challenge into another protocol execution.
Our case study illustrates the importance of cryptographically binding context to protocol messages to prevent an adversary from misusing messages out of context.
more »
« less
This content will become publicly available on January 8, 2025
Limitations of Wrapping Protocols and TLS Channel Bindings: Formal-Methods Analysis of the Session Binding Proxy Protocol (submitted to CIC)
We present the first formal-methods analysis of the Session Binding Proxy (SBP) protocol,
which protects a vulnerable system by wrapping it and introducing
a reverse proxy between the system and its clients.
SBP mitigates thefts of authentication cookies by
cryptographically binding the authentication cookie---issued by the server to the client---to an underlying Transport Layer Security (TLS) channel using the channel's master secret
and a secret key known only by the proxy.
An adversary who steals a bound cookie cannot reuse this cookie to create malicious requests on a separate connection because the cookie's channel binding will not match the adversary's channel.
SBP seeks to achieve this goal without modifications to the client or the server software,
rendering the client and server
``oblivious protocol participants'' that are not aware of the SBP session.
Our analysis verifies that the original SBP design mitigates cookie stealing
under the client's cryptographic assumptions
but fails to authenticate the client to the proxy.
Resulting from two issues, the proxy has no assurance that it shares a session context with a legitimate client:
SBP assumes an older flawed version of TLS (1.2), and SBP relies on legacy server usernames and passwords to authenticate clients.
Due to these issues, there is no guarantee of cookie-stealing resistance from the proxy's cryptographic perspective.
Using the Cryptographic Protocol Shapes Analyzer (CPSA), we model and analyze
the original SBP and three variations
in the Dolev-Yao network intruder model.
Our models differ in the version of TLS they use:
1.2 (original SBP), 1.2 with mutual authentication, 1.3, and {\it 1.3 with mutual authentication (mTLS-1.3)}.
For comparison, we also analyze a model of the baseline scenario without SBP.
We separately analyze each of our SBP models from two perspectives: client and proxy.
In each SBP model, the client has assurance that the cookie is valid only for the client's legitimate session.
Only in mTLS-1.3 does the proxy have assurance that it communicates with a legitimate client and that the client's cookie is valid.
We formalize these results by stating and proving, or disproving, security goals for each model.
SBP is useful because it provides a practical solution to the important challenge of protecting flawed legacy systems that cannot be patched.
Our analysis of this obscure protocol sheds insight into the properties necessary for wrapper protocols to resist a Dolev-Yao adversary.
When engineering wrapper protocols, designers must carefully consider authentication, freshness, and requirements of cryptographic bindings such as channel bindings.
Our work exposes strengths and limitations of wrapper protocols and TLS channel bindings.
more »
« less
- Award ID(s):
- 1753681
- NSF-PAR ID:
- 10490240
- Publisher / Repository:
- Communications in Cryptology
- Date Published:
- Journal Name:
- Communications in Cryptology
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
We analyze the Secure Remote Password (SRP) protocol for structural weaknesses using the Cryptographic Protocol Shapes Analyzer (CPSA) in the first formal analysis of SRP (specifically, Version 3). SRP is a widely deployed Password Authenticated Key Exchange (PAKE) protocol used in 1Password, iCloud Keychain, and other products. As with many PAKE protocols, two participants use knowledge of a preshared password to authenticate each other and establish a session key. SRP aims to resist dictionary attacks, not store plaintext-equivalent passwords on the server, avoid patent infringement, and avoid export controls by not using encryption. Formal analysis of SRP is challenging in part because existing tools provide no simple way to reason about its use of the mathematical expression “v + g b mod q”. Modeling v + g b as encryption, we complete an exhaustive study of all possible execution sequences of SRP. Ignoring possible algebraic attacks, this analysis detects no major structural weakness, and in particular no leakage of any secrets. We do uncover one notable weakness of SRP, which follows from its design constraints. It is possible for a malicious server to fake an authentication session with a client, without the client’s participation. This action might facilitate an escalation of privilege attack, if the client has higher privileges than does the server. We conceived of this attack before we used CPSA and confirmed it by generating corresponding execution shapes using CPSA.more » « less
-
We analyze the Secure Remote Password (SRP) protocol for structural weaknesses using the Cryptographic Protocol Shapes Analyzer (CPSA) in the first formal analysis of SRP (specifically, Version 3). SRP is a widely deployed Password Authenticated Key Exchange (PAKE) protocol used in 1Password, iCloud Keychain, and other products. As with many PAKE protocols, two participants use knowledge of a pre-shared password to authenticate each other and establish a session key. SRP aims to resist dictionary attacks, not store plaintext-equivalent passwords on the server, avoid patent infringement, and avoid export controls by not using encryption. Formal analysis of SRP is challenging in part because existing tools provide no simple way to reason about its use of the mathematical expression “v + g b mod q”. Modeling v + g b as encryption, we complete an exhaustive study of all possible execution sequences of SRP. Ignoring possible algebraic attacks, this analysis detects no major structural weakness, and in particular no leakage of any secrets. We do uncover one notable weakness of SRP, which follows from its design constraints. It is possible for a malicious server to fake an authentication session with a client, without the client’s participation. This action might facilitate an escalation of privilege attack, if the client has higher privileges than does the server. We conceived of this attack before we used CPSA and confirmed it by generating corresponding execution shapes using CPSA.more » « less
-
Hazay, Carmit ; Stam, Martin (Ed.)OPAQUE is an Asymmetric Password-Authenticated Key Exchange (aPAKE) protocol being standardized by the IETF (Internet Engineering Task Force) as a more secure alternative to the traditional “password-over-TLS” mechanism prevalent in current practice. OPAQUE defends against a variety of vulnerabilities of password-over-TLS by dispensing with reliance on PKI and TLS security, and ensuring that the password is never visible to servers or anyone other than the client machine where the password is entered. In order to facilitate the use of OPAQUE in practice, integration of OPAQUE with TLS is needed. The main proposal for standardizing such integration uses the Exported Authenticators (TLS-EA) mechanism of TLS 1.3 that supports post-handshake authentication and allows for a smooth composition with OPAQUE. We refer to this composition as TLS-OPAQUE and present a detailed security analysis for it in the Universal Composability (UC) framework. Our treatment is general and includes the formalization of components that are needed in the analysis of TLS-OPAQUE but are of wider applicability as they are used in many protocols in practice. Specifically, we provide formalizations in the UC model of the notions of post-handshake authentication and channel binding. The latter, in particular, has been hard to implement securely in practice, resulting in multiple protocol failures, including major attacks against prior versions of TLS. Ours is the first treatment of these notions in a computational model with composability guarantees. We complement the theoretical work with a detailed discussion of practical considerations for the use and deployment of TLS-OPAQUE in real-world settings and applications.more » « less
-
null (Ed.)Methods for continuous user authentication have become important with the proliferation of mobile devices in m-Health and human-centered systems. These methods must guarantee user identity with high assurance, authenticate without explicit intervention, and be power-aware. We present an evaluation of the power consumption of collaborative authentication (coauthentication) as a continuous authentication method. Coauthentication is a single-factor method in which multiple registered devices work together to authenticate a user, minimizing obtrusiveness while providing high user authentication assurance. To evaluate coauthentication's power consumption, we conducted experiments using two Bluetooth-enabled mobile devices and a stand-alone server in a local area network and running coauthentication continuously for eight hours. We found that the protocol uses approximately between 1.19% and 4.0% of the total power used by the devices. These results give evidence of the feasibility of using coauthentication as a continuous authentication method in mobile devices from the power consumption perspective.more » « less
