Skip to content 

include quic_types
include quic_transport_error_code
include quic_frame
include quic_packet
include quic_transport_parameters
include ip
The packet protocol

The packet protocol has several funcitons including establishing connections and loss detection. Packets carry frames whihc implement many other funcition of QUIC.

QUIC Packets¤

This section defines the QUIC packet datatype. Packets are the basic unit of communication between endpoints. A packet may be encoded in either the long or the short format. There are packet types: initial, handshake, zero_rtt and one_rtt. The zero_rtt type is encoded in the short format, while others are encoded in the long format. Packets have associated source cid (long format only) and destination cid, protocol version (long format only), and a packet sequence number. An initial packet also has a retry token, which is a (possibly empty) sequence of bytes. The payload of the packet consists of a sequence of frames (see frame.ivy).

Todo

retry and one_rtt packet types

instance index : unbounded_sequence
instance versions : array(index,stream_data)
interpret version -> bv[32]
instance versions_bv : array(index,version)

Packet¤

The type quic_packet_vn represents packet.

The fields are:

  • ptype: the packet type [2]
  • pversion: the protocol version, if long format, else 0 [3]
  • dst_cid: the destination cid [4]
  • src_cid: the source cid, if long format, else 0 [5]
  • token: the retry token (see section 4.4.1) [6]
  • seq_num: the packet sequence number [7]
  • payload: the payload, a sequence of frames [8]

object quic_packet_vn = {
    type this = struct {
        ptype : quic_packet_type, # [2]
        pversion : version, # [3]
        dst_cid : cid, # [4]
        src_cid : cid, # [5]
        supported_version : versions_bv # [3]
    }

    instance idx : unbounded_sequence
    instance arr : array(idx,this)
}
Note: Short header are considered to have scid of 0 so it is quite important to use this value

Packet protocol events¤

The packet event¤

This event corresponds to transmission of a QUIC packet.

Parameters¤

  • src: the source endpoint
  • dst: the destination endpoint
  • pkt : the packet contents

action packet_event_vn(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet_vn) = {}
Packet protocol state

This section defines the history variables that track the state of the packet protocol. Some of these variables are shared between protocol layers, so that the allowed interleavings of events at different layers can be specified.

Packet protocol state¤

Packet event specification¤

A packet event represents the transmision of a QUIC packet pkt from source endpoint src to a QUIC destination endpoint dst containing a sequence of queued frames.

Requirements¤

  • The packet payload may not be empty [7].

An endpoint MUST NOT send a Version Negotiation packet in response to receiving a Version Negotiation packet. [1c]

A client that supports only this version of QUIC MUST abandon the current connection attempt if it receives a Version Negotiation packet, with the following two exceptions.

A client MUST discard any Version Negotiation packet if it has received and successfully processed any other packet, including an earlier Version Negotiation packet.

A client MUST discard a Version Negotiation packet that lists the QUIC version selected by the client.

around packet_event_vn(src:ip.endpoint,dst:ip.endpoint,pkt:quic_packet_vn) {
Extract the source and destination cid's and packet number from the packet.

    var dcid := pkt.dst_cid;
    var scid := pkt.src_cid;
    if cid_mapped(dcid) {
        dcid := cid_to_aid(dcid);
    };

    if src = client_alt | dst = client_alt {
        migration_done := true;
call net.close(endpoint_id.client,sock); # destroy connection ? 
    };


    require pkt.ptype = quic_packet_type.version_negociation;

    require ~negocation_of_version_initiated(src);  #[1c]

    ...

    var dcid := pkt.dst_cid;
    var scid := pkt.src_cid;

    if cid_mapped(dcid) {
        dcid := cid_to_aid(dcid);
    };

    if  ~_generating  {
        conn_requested(src,dst,scid) := false;
        conn_requested(src,dst,dcid) := false;
        connected(dcid) :=  false;
        connected(scid) :=  false;
        conn_seen(dcid) := false;
        conn_seen(scid) := false;

        var old_cid := the_cid;
        the_cid := inc_cid(old_cid,2); # 0x0;
        server_cid := 0x0;
        connected(the_cid)    := false;
        connected(server_cid) := false;
        conn_seen(the_cid)    := false;
        conn_seen(server_cid) := false;

        var extns := tls_extensions.empty;
        extns := extns.append(make_transport_parameters);
        call tls_api.upper.create(0,false,extns);  # false means this instance of tls is not a server put that in shim
        conn_requested(dst,src,the_cid) := true;
    };
Record the packet number as latest see 
    negocation_of_version_initiated(src) := true;
}

action inc_cid(c:cid, inc:stream_pos) returns(res:cid) = {
    <<<
    res.val = c.val + inc;
    >>>
}

import action show_initial_request_vn