CDL talk 9/10 Prajna Bhandary, Selfie Attack on TLS

Abstract.

Using the Cryptographic Protocol Shapes Analyzer (CPSA), we found the “selfie” attack on TLS 1.3, and we propose and formally verify two mitigations. Previously, in 2019, researchers had discovered this reflection attack against the pre-shared key (PSK) mode of authentication, but not using formal-methods tools. They discovered a gap in one of the proofs that ignores the case of external PSKs. They demonstrated that, in this case, a PSK belongs to at most two parties, but the protocol cannot distinguish which party sent the message. We also identify a previously discovered impersonation attack that uses post-handshake authentication, which invalidates this approach as a possible mitigation to the selfie attack.

Our work illustrates the strengths and weaknesses of formal-methods tools. Although TLS 1.3 has been formally analyzed using the Tamarin, Maude NPA and ProVerif tools, initially researchers missed the selfie attack, perhaps because they did not look for such an attack. Previous researchers focused on critical known attacks, such as Logjam, Triple Handshake, or SMACK. These analyses did not consider any case where the client uses TLS 1.3 with external PSK to talk to itself for an entire session. By contrast, CPSA enumerates all equivalence classes of protocol executions for a given set of assumptions, but requires the user to interpret the graphical output.


About the Speaker.

Prajna Bhandary is a PhD student in computer science at UMBC, studying under Dr. Nicholas. Her research areas include protocol analysis, and malware analysis using machine learning and data science.