TLS Local Encryption

[nikswamy]

Within TLS, there are several uses of internally determined encryption constructions.

For instance, to represent PSK identifiers, we choose an encrypted blob { PSK keyid info }K-seal to represent a key identifier. We have similar ad hoc encryptions for cookies, tickets and seals.

The existing code uses the high-level interface to EverCrypt AEAD using AEADProvider, a bytes-oriented interface. It is also not idealized. And it doesn't handle all four uses of local encryption.

We want to migrate to using a low-level interface to EverCrypt.AEAD, that has security idealization, that supports multiplexing of all four usages.

Current status

We have two modules from @tahina-pro,

• Crypto.AEAD
• Crypto.AE
  which provide a low-level idealized interface to EverCrypt.AEAD. Crypto.AE differs from Crypto.AEAD in that it also generates IVs when encrypting. Note, the first module does not actually support "additional data" ... so perhaps it should be renamed.

Meanwhile experiments/TLS.Store.fsti is an interface sketch that aims to:

• provide the application the ability to set a key in TLS global state associated with each usage

• and then encrypts or decrypts for a given usage using the appropriate key

One task is to implement this interface over Crypto.AE/AEAD.
Then, we need to revise Ticket.fst (ticket_encrypt and decyrypt) to use the TLS.Store interface instead. This will also require updating Cookie.fst, which will first use EverParse to serialize a cookie to bytes before encrypting.

Open issue: Enhancing the Crypto.AEAD to support key indexing and update

Crypto.AEAD indexes keys using an authentication predicate phi. The choice of this predicate has to be made at the level of the Handshake, e.g., instantiating it in a form suitable for the state machine properties in stateless hello retry (see @s-zanella experiments towards that).

We would like to move the set_key functionality of TLS.Store into Crypto.AEAD, maintaining a global table there of indexed keys, per usage.

We should integrate with Santiago's connection table experiments to check that we can instantiate the key indexes properly and gain a top-level security property.

Restoring concrete functionality

After revising Ticket and Cookie, we should be able to run the code and interop again. Since this is TLS local encryption, a change in the details of the encryption scheme being used shouldn't matter.