Partially Specified Channels: The TLS 1.3 Record Layer without Elision

Christopher Patton; Thomas Shrimpton

Paper 2018/634

Partially Specified Channels: The TLS 1.3 Record Layer without Elision

Christopher Patton and Thomas Shrimpton

Abstract

We advance the study of secure stream-based channels (Fischlin et al., CRYPTO ’15) by considering the multiplexing of many data streams over a single channel, an essential feature of real world protocols such as TLS. Our treatment adopts the definitional perspective of Rogaway and Stegers (CSF ’09), which offers an elegant way to reason about what standardizing documents actually provide: a partial specification of a protocol that admits a collection of compliant, fully realized implementations. We formalize partially specified channels as the component algorithms of two parties communicating over a channel. Each algorithm has an oracle that provides specification details; the algorithms abstract the things that must be explicitly specified, while the oracle abstracts the things that need not be. Our security notions, which capture a variety of privacy and integrity goals, allow the adversary to respond to these oracle queries; security relative to these notions implies that the channel withstands attacks in the presence of worst-case (i.e., adversarial) realizations of the specification details. We apply this framework to a formal treatment of the TLS 1.3 record and, in doing so, show that its security hinges crucially upon details left unspecified by the standard.

Note: The latest version fixes a minor bug in Theorem 4.

Metadata

Available format(s): PDF
Category: Applications
Publication info: Published elsewhere. Minor revision. 10.1145/3243734.3243789
Keywords: provable security cryptographic standards TLS 1.3 stream-based channels partially specified protocols
Contact author(s): cjpatton @ ufl edu
History: 2020-04-03: last of 3 revisions; 2018-06-28: received; See all versions
Short URL: https://ia.cr/2018/634
License: CC BY

BibTeX

@misc{cryptoeprint:2018/634,
      author = {Christopher Patton and Thomas Shrimpton},
      title = {Partially Specified Channels: The {TLS} 1.3 Record Layer without Elision},
      howpublished = {Cryptology {ePrint} Archive, Paper 2018/634},
      year = {2018},
      url = {https://eprint.iacr.org/2018/634}
}