Séminaire des équipes de recherche
Composition Theorems for CryptoVerif and Application to TLS 1.3
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.
For more informations
- Time : 11h00
- Place : Inria de Paris - 2 rue Simone Iff - Salle Lions 2, bâtiment C