More Like this

1. Formal Methods Analysis of the Secure Remote Password Protocol

   Sherman, Alan T. ; Lanus, Erin ; Liskov, Moses ; Zieglar, Edward ; Chang, Richard ; Golaszewski, Enis ; Wnuk-Fink, Ryan ; Bonyadi, Cyrus J. ; Yaksetig, Mario ; Blumenfel, Ian ( October 2020 , Festschrift in Honour of Professor Andre Scedrov, Vivek Nigam, Editor, LNCS, Springer)

   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
2. Cryptographic Binding Should Not Be Optional: A Formal-Methods Analysis of FIDO UAF Authentication

   Golaszewski, Enis ; Sherman, Alan T. ; Zieglar, Edward ( July 2023 , ACM CCS (submitted))

   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
3. Two-factor Password-authenticated Key Exchange with End-to-end Security

   https://doi.org/10.1145/3446807  

   Jarecki, Stanislaw ; Jubur, Mohammed ; Krawczyk, Hugo ; Saxena, Nitesh ; Shirvanian, Maliheh ( August 2021 , ACM Transactions on Privacy and Security)

   null (Ed.)

   We present a secure two-factor authentication (TFA) scheme based on the user’s possession of a password and a crypto-capable device. Security is “end-to-end” in the sense that the attacker can attack all parts of the system, including all communication links and any subset of parties (servers, devices, client terminals), can learn users’ passwords, and perform active and passive attacks, online and offline. In all cases the scheme provides the highest attainable security bounds given the set of compromised components. Our solution builds a TFA scheme using any Device-enhanced Password-authenticated Key Exchange (PAKE), defined by Jarecki et al., and any Short Authenticated String (SAS) Message Authentication, defined by Vaudenay. We show an efficient instantiation of this modular construction, which utilizes any password-based client-server authentication method, with or without reliance on public-key infrastructure. The security of the proposed scheme is proven in a formal model that we formulate as an extension of the traditional PAKE model. We also report on a prototype implementation of our schemes, including TLS-based and PKI-free variants, as well as several instantiations of the SAS mechanism, all demonstrating the practicality of our approach. Finally, we present a usability study evaluating the viability of our protocol contrasted with the traditional PIN-based TFA approach in terms of efficiency, potential for errors, user experience, and security perception of the underlying manual process. 1 

   more » « less
4. Limitations of Wrapping Protocols and TLS Channel Bindings: Formal-Methods Analysis of the Session Binding Proxy Protocol (submitted to CIC)

   Golaszewski, Enis ; Zieglar, Edward ; Sherman, Alan T. ; Elsaad, Kirellos Abou ; Fuchs, Jonathan ( January 2024 , Communications in Cryptology)

   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
5. Asymmetric PAKE with Low Computation and communication

   Dos Santos, Bruno Freitas ; Gu, Yanqi. ; Jarecki, Stanislaw. ; Krawczyk, Hugo ( May 2022 , Lecture Notes in Computer Science (LNCS))

   Dunkelman, O. ; Dziembowski, S (Ed.)

   In Crypto’21 Gu, Jarecki, and Krawczyk [25] showed an asymmetric password authenticated key exchange protocol (aPAKE) whose computational cost matches (symmetric) password authenticated key exchange (PAKE) and plain (i.e. unauthenticated) key exchange (KE). However, this minimal-cost aPAKE did not match prior aPAKE’s in round complexity, using 4 rounds assuming the client initiates compared to 2 rounds in an aPAKE of Bradley et al. [13]. In this paper we show two aPAKE protocols (but not strong aPAKEs like [13, 30]), which achieve optimal computational cost and optimal round complexity. Our protocols can be seen as variants of the Encrypted Key Exchange (EKE) compiler of Bellovin and Merritt [7], which creates password-authenticated key exchange by password-encrypting messages in a key exchange protocol. Whereas Bellovin and Merritt used this method to construct a PAKE by applying password-encryption to KE messages, we construct an aPAKE by password-encrypting messages of a unilaterally authenticated Key Exchange (ua-KE). We present two versions of this compiler. The first uses salted password hash and takes 2 rounds if the server initiates. The second uses unsalted password hash and takes a single simultaneous flow, thus simultaneously matching the minimal computational cost and the minimal round complexity of PAKE and KE. We analyze our aPAKE protocols assuming an Ideal Cipher (IC) on a group, and we analyze them as modular constructions from ua-KE realized via a universally composable Authenticated Key Exchange where the server uses one-time keys (otk-AKE). We also show that one-pass variants of 3DH and HMQV securely realize otk-AKE in the ROM. Interestingly, the two resulting concrete aPAKE’s use the exact same protocol messages as variants of EKE, and the only difference between the symmetric PAKE (EKE) and asymmetric PAKE (our protocols) is in the key derivation equation. 

   more » « less