Searching for Selfie in TLS 1.3 with the Cryptographic Protocol Shapes Analyzer

Thumbnail Image

Files

Searching for Selfies.pdf (5.8 MB)

Links to Files

https://link.springer.com/chapter/10.1007/978-3-030-91631-2_3

Permanent Link

https://doi.org/10.1007/978-3-030-91631-2_3
 http://hdl.handle.net/11603/23860

Collections

UMBC Computer Science and Electrical Engineering Department
UMBC Faculty Collection
UMBC Staff Collection

Author/Creator

Author/Creator ORCID

https://orcid.org/0000-0001-9494-7139

Date

2021-11-19

Type of Work

book chapters
Text

Department

Program

Citation of Original Publication

Bhandary P., Zieglar E., Nicholas C. (2021) Searching for Selfie in TLS 1.3 with the Cryptographic Protocol Shapes Analyzer. In: Dougherty D., Meseguer J., Mödersheim S.A., Rowe P. (eds) Protocols, Strands, and Logic. Lecture Notes in Computer Science, vol 13066. Springer, Cham. https://doi.org/10.1007/978-3-030-91631-2_3

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.
Public Domain Mark 1.0

Subjects

Abstract

TLS 1.3 was developed in conjunction with several formal analyses and proofs of its security properties. However, in 2019, researchers Drucker and Gueron discovered a reflection attack, they named Selfie, against the pre-shared key (PSK) mode of authentication used by TLS 1.3 by identifying a gap in the proofs. They realized that the proofs ignored the case of external PSKs. They demonstrated that if the PSK was not associated with a particular client and server pairing, such as a single PSK between a pair of hosts which could use the key as either a client or server, implicit authentication implied by the use of the PSK would fail in a reflection attack. The proofs and tools used did not account for this, so we set out to determine if it was possible to identify this attack with the Cryptographic Protocol Shapes Analyzer (CPSA). Using CPSA, which attempts to enumerate all equivalence classes of a protocol’s executions, we were able to uncover the attack and verify two proposed mitigations. We were also able to identify a previously discovered impersonation attack against the use of post handshake authentication in scenarios where a PSK is used as a network key