Sites Inria

Version française

Séminaire des équipes de recherche

Composition Theorems for CryptoVerif and Application to TLS 1.3

© INRIA Sophie Auvin - P comme Protocole

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.

  • Date : 26/06/2018
  • Place : Inria de Paris, 2 rue Simone Iff, Salle Jacques-Louis Lions 1, bâtiment C
  • Guest(s) : Bruno Blanchet (Prosecco)

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.

Keywords: Séminaire Prosecco Inria de Paris Theorems CryptoVerif TLS 1.3 Application