Composition Theorems for CryptoVerif and Application to TLS 1.3

Abstract : We present composition theorems for security protocols, to compose a key exchange protocol and a symmetric-key protocol that uses the exchanged key. Our results rely on the computational model of cryptography and are stated in the framework of the tool CryptoVerif. They support key exchange protocols that guarantee injective or non-injective authentication. They also allow random oracles shared between the composed protocols. To our knowledge, they are the first composition theorems for key exchange stated for a computational protocol verification tool, and also the first to allow such flexibility. As a case study, we apply our composition theorems to a proof of TLS 1.3 Draft-18. This work fills a gap in a previous paper that informally claims a compositional proof of TLS 1.3, without formally justifying it.
Document type :
Reports
Complete list of metadatas

Cited literature [37 references]  Display  Hide  Download

https://hal.inria.fr/hal-01764527
Contributor : Bruno Blanchet <>
Submitted on : Thursday, April 12, 2018 - 10:46:45 AM
Last modification on : Monday, September 10, 2018 - 3:15:39 PM

File

RR-9171.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01764527, version 1

Collections

Citation

Bruno Blanchet. Composition Theorems for CryptoVerif and Application to TLS 1.3. [Research Report] RR-9171, Inria Paris. 2018, pp.67. ⟨hal-01764527⟩

Share

Metrics

Record views

319

Files downloads

363