Tls msg

include tls_picotls

This module defines the interface to TLS at the message level. This interface eliminates the TLS record layer, instead delegating encryption to the client, as needed by the QUIC protocol. The interface provides suiatable encryption and decryption methods that can be used for this purpose.

module tls_lower_intf(cid,bytes) = {

Encryption level, ranges from 0-3.

    type level

Transfers message data from connection to underlying transport

    action send(c:cid,data:bytes,lev:level)

Transfers message data from the underlying transport to connection

    action recv(c:cid,data:bytes,lev:level)

}

This module defines the interface of a TLS endpoint (either a client or a server. The parameters are:

cid:the type of connection identifiers bytes:the type of byte arrays lower:the interface to the underlying transport extens:the type of lists of extensions exten_ser:serializer for extensions

module tls_intf(cid,index,bytes,lower,extens,hextens,exten_ser,seq_num) = {

The upper interface is between TLS and the application

Encryption level, ranges from 0-3.

    type level

Transfers connection data to application

    action recv(c:cid,data:bytes)

Transfers application data to conection

    action send(c:cid,data:bytes)

Alert from connection to application

    action alert(c:cid,data:bytes)

Indicates to application that a session is established, meaning the connection is ready to send on.

    action session_established(c:cid)

Indicates to application that the keys for a given encryption level are established.

    action keys_established(c:cid,lev:level)

Generates key material based on master secret, per RFC 5705.

    action key_material_export(c:cid,label:bytes,context:bytes,length:index) returns (key:bytes)

Create a new connection with a fresh cid, and list of extensions

    action eavesdrop_client(c:cid)

    action eavesdrop_server(c:cid)

    action create(c:cid, is_server:bool, e:extens)

    action create_0rtt_client(c:cid, is_server:bool, e:extens)

    action create_0rtt(c:cid, is_server:bool, e:extens, he:hextens)

    action get_old_retry_token returns (b:stream_data)

    action save_token(token:stream_data)

    action save_initial_max_stream_data_uni(i:stream_pos)

    action save_initial_max_stream_data_bidi_remote(i:stream_pos)

    action save_initial_max_data(i:stream_pos)

    action save_initial_max_stream_data_bidi_local(i:stream_pos)

    action save_initial_max_stream_id_bidi(i:stream_id)

    action save_active_connection_id_limit(i:stream_pos)

    action get_initial_max_stream_data_uni returns(i:stream_pos)

    action get_initial_max_stream_data_bidi_remote returns(i:stream_pos)

    action get_initial_max_data returns(i:stream_pos)

    action get_initial_max_stream_data_bidi_local returns(i:stream_pos)

    action get_initial_max_stream_id_bidi returns(i:stream_id)

    action get_active_connection_id_limit returns(i:stream_pos)

action create_no_hs(c:cid, is_server:bool, e:extens)

    action get_old_new_token returns (b:stream_data)

Destroy an existing connection

    action destroy(c:cid)

Set the initial keys for a session. There are determined by the salt and the initial key material ikm. In QUIC, the salt is fixed by the protocol version, whereas ikm is the client's initial destination connection id.

    action set_initial_keys(c:cid,salt:bytes,ikm:bytes)

Get the size of the cipher initial value for a given level.

    action iv_size(c:cid,l:level) returns (sz:index)

Encrypt data with sending symmertic cipher cipher for given level and initial value. If recv is true, encrypt with receiving cipher. This option is needed for QUIC header protection.

    action encrypt_cipher(c:cid,l:level,clear:bytes,iv:bytes,recv:bool) returns (cipher:bytes)

Decrypt data with receiving symmetric cipher for given level and initial value.

    action decrypt_cipher(c:cid,l:level,cipher:bytes,iv:bytes) returns (clear:bytes)


    action compute_retry_integrity_tag(odcil: stream_pos, odcid: cid,
                                       pversion: version,
                                       dcil: stream_pos, dcid: cid,
                                       scil: stream_pos, scid: cid,
                                       token:stream_data,
                                       seq:seq_num,h:stream_pos,is_recv:bool) returns (cipher:bytes)

Encrypt data with AEAD for given level, additional data ad and sequence number seq.

    action encrypt_aead(c:cid,l:level,clear:bytes,seq:seq_num,ad:bytes) returns (cipher:bytes)

    type decrypt_result = struct {
        ok:bool,
        data:bytes,
        payload:bytes
    }

Decrypt data with cipher for given level, additional data ad and sequence number seq. Return parameter ok indicates decryption was successful.

    action decrypt_aead(c:cid,l:level,cipher:bytes,seq:seq_num,ad:bytes)
    returns (res:decrypt_result)

    specification {

        relation open(C:cid)
        relation established(C:cid)

        after init {
            open(C) := false;
            established(C) := false;
        }

        around create {
            require ~open(c);
            ...
            open(c) := true;
        }

        around destroy {
            require open(c);
            ...
            open(c) := false;
            established(c) := false;
        }

        before recv {
            require open(c);
        }

        before send {
            require open(c) & established(c);
        }

        before session_established {
            require open(c) & ~established(c);
            established(c) := true
        }

        before key_material_export {
            require open(c) & established(c);
        }

        invariant established(C) -> open(C)
    }

    instance foo:tls_gnutls(cid,index,bytes,extens,hextens,exten_ser,lower,this)

}