Formal Methods Analysis of the Secure Remote Password Protocol
dc.contributor.author | Sherman, Alan T. | |
dc.contributor.author | Lanus, Erin | |
dc.contributor.author | Liskov, Moses | |
dc.contributor.author | Zieglar, Edward | |
dc.contributor.author | Chang, Richard | |
dc.contributor.author | Golaszewski, Enis | |
dc.contributor.author | Wnuk-Fink, Ryan | |
dc.contributor.author | Bonyadi, Cyrus J. | |
dc.contributor.author | Yaksetig, Mario | |
dc.contributor.author | Blumenfeld, Ian | |
dc.date.accessioned | 2020-04-09T19:57:56Z | |
dc.date.available | 2020-04-09T19:57:56Z | |
dc.date.issued | 2020-03-16 | |
dc.description.abstract | 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ᵇ modq. Modeling v+gᵇ 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. | en_US |
dc.description.sponsorship | Thanks to John Ramsdell (MITRE) and other participants at the Protocol eXchange for fruitful interactions. This research was supported in part by the U.S. Department of Defense under CySP Capacity grants H98230-17-1-0387 and H98230-18-1-0321. Sherman, Golaszewski, Wnuk-Fink, Bonyadi, and the UMBC Cyber Defense Lab were supported also in part by the National Science Foundation under SFS grant DGE-1753681. | en_US |
dc.description.uri | https://www.springerprofessional.de/en/formal-methods-analysis-of-the-secure-remote-password-protocol/18531710 | en_US |
dc.format.extent | 23 pages | en_US |
dc.genre | chapters | |
dc.genre | preprints | |
dc.identifier | doi:10.13016/m2qmyh-lfry | |
dc.identifier.citation | Sherman, Alan T., et al. "Formal Methods Analysis of the Secure Remote Password Protocol" Logic, Language, and Security (2020). https://www.springerprofessional.de/en/formal-methods-analysis-of-the-secure-remote-password-protocol/18531710. | en_US |
dc.identifier.uri | http://hdl.handle.net/11603/17914 | |
dc.language.iso | en_US | en_US |
dc.publisher | Springer International Publishing | |
dc.relation.isAvailableAt | The University of Maryland, Baltimore County (UMBC) | |
dc.relation.ispartof | UMBC Computer Science and Electrical Engineering Department Collection | |
dc.relation.ispartof | UMBC Center for Information Security and Assurance (CISA) | |
dc.relation.ispartof | UMBC Faculty Collection | |
dc.relation.ispartof | UMBC Student Collection | |
dc.rights | This work was written as part of one of the author's official duties as an Employee of the United States Government and is therefore a work of the United States Government. In accordance with 17 U.S.C. 105, no copyright protection is available for such works under U.S. Law. | * |
dc.rights | Public Domain Mark 1.0 | |
dc.rights.uri | http://creativecommons.org/publicdomain/mark/1.0/ | * |
dc.subject | UMBC Cyber Defense Lab | |
dc.title | Formal Methods Analysis of the Secure Remote Password Protocol | en_US |
dc.type | Text | en_US |
dcterms.creator | https://orcid.org/0000-0003-1130-4678 | |
dcterms.creator | https://orcid.org/0000-0001-5278-7958 | |
dcterms.creator | https://orcid.org/0000-0002-0814-9956 | |
dcterms.creator | https://orcid.org/0000-0002-4964-1381 | |
dcterms.creator | https://orcid.org/0000-0002-3686-7242 | |
dcterms.creator | https://orcid.org/0000-0003-2175-1957 |