5.1. Record Layer

RFC 8446

enum {
    invalid(0),
    change_cipher_spec(20),
    alert(21),
    handshake(22),
    application_data(23),
    (255)
} ContentType;

struct {
    ContentType type;
    ProtocolVersion legacy_record_version;
    uint16 length;
    opaque fragment[TLSPlaintext.length];
} TLSPlaintext;

src/model/macros.splib

DataRecord(data) = <data, '23'>

Sending and receiving data is modelled by sending and receiving some fresh term ~data. The keys used for encryption are stored in the SendStream and RecvStream facts which are introduced here.

src/model/record.splib

rule send:
    [
        SendStream(~tid, $actor, $peer, auth_status, app_key_out),
        Fr(~data)
    ]
    --[
        Send(~tid),
        SendData(~tid, $actor, $peer, auth_status, ~data)
    ]->
    [
        SendStream(~tid, $actor, $peer, auth_status, app_key_out),
        MessageOut(senc{DataRecord(~data)}app_key_out)
    ]

src/model/record.splib

rule recv:
    [
        RecvStream(~tid, $actor, $peer, auth_status, app_key_in),
        F_MessageIn(senc{DataRecord(data)}app_key_in)
    ]
    --[
        Recv(~tid),
        RecvData(~tid, $actor, $peer, auth_status, data)
    ]->
    [
      RecvStream(~tid, $actor, $peer, auth_status, app_key_in)
    ]