Formal Methods Analysis of the Secure Remote Password Protocol

Simple item page
dc.contributor.authorSherman, Alan T.
dc.contributor.authorLanus, Erin
dc.contributor.authorLiskov, Moses
dc.contributor.authorZieglar, Edward
dc.contributor.authorChang, Richard
dc.contributor.authorGolaszewski, Enis
dc.contributor.authorWnuk-Fink, Ryan
dc.contributor.authorBonyadi, Cyrus J.
dc.contributor.authorYaksetig, Mario
dc.contributor.authorBlumenfeld, Ian
dc.date.accessioned2020-04-09T19:57:56Z
dc.date.available2020-04-09T19:57:56Z
dc.date.issued2020-03-16
dc.description.abstractWe 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.sponsorshipThanks 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.urihttps://www.springerprofessional.de/en/formal-methods-analysis-of-the-secure-remote-password-protocol/18531710en_US
dc.format.extent23 pagesen_US
dc.genrechapters
dc.genrepreprints
dc.identifierdoi:10.13016/m2qmyh-lfry
dc.identifier.citationSherman, 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.urihttp://hdl.handle.net/11603/17914
dc.language.isoen_USen_US
dc.publisherSpringer International Publishing
dc.relation.isAvailableAtThe University of Maryland, Baltimore County (UMBC)
dc.relation.ispartofUMBC Computer Science and Electrical Engineering Department Collection
dc.relation.ispartofUMBC Center for Information Security and Assurance (CISA)
dc.relation.ispartofUMBC Faculty Collection
dc.relation.ispartofUMBC Student Collection
dc.rightsThis 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.rightsPublic Domain Mark 1.0
dc.rights.urihttp://creativecommons.org/publicdomain/mark/1.0/*
dc.subjectUMBC Cyber Defense Lab
dc.titleFormal Methods Analysis of the Secure Remote Password Protocolen_US
dc.typeTexten_US
dcterms.creatorhttps://orcid.org/0000-0003-1130-4678
dcterms.creatorhttps://orcid.org/0000-0001-5278-7958
dcterms.creatorhttps://orcid.org/0000-0002-0814-9956
dcterms.creatorhttps://orcid.org/0000-0002-4964-1381
dcterms.creatorhttps://orcid.org/0000-0002-3686-7242
dcterms.creatorhttps://orcid.org/0000-0003-2175-1957

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
2003.07421.pdf
Size:
379.85 KB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
2.56 KB
Format:
Item-specific license agreed upon to submission
Description:
Download

Collections

UMBC Computer Science and Electrical Engineering Department
UMBC Center for Information Security and Assurance (CISA)
UMBC Faculty Collection
UMBC Student Collection