Bgp open message

After a TCP connection is established, the first message sent by each side is an OPEN message. If the OPEN message is acceptable, a KEEPALIVE message confirming the OPEN is sent back.

In addition to the fixed-size BGP header, the OPEN message contains the following fields:

0 1 2 3 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 +-+-+-+-+-+-+-+-+ | Version | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | My Autonomous System | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Hold Time | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | BGP Identifier | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | Opt Parm Len | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+ | | | Optional Parameters (variable) | | | +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+

  Version:

     This 1-octet unsigned integer indicates the protocol version
     number of the message.  The current BGP version number is 4.

  My Autonomous System:

     This 2-octet unsigned integer indicates the Autonomous System
     number of the sender.

  Hold Time:

     This 2-octet unsigned integer indicates the number of seconds
     the sender proposes for the value of the Hold Timer.  Upon
     receipt of an OPEN message, a BGP speaker MUST calculate the
     value of the Hold Timer by using the smaller of its configured
     Hold Time and the Hold Time received in the OPEN message.  The
     Hold Time MUST be either zero or at least three seconds.  An
     implementation MAY reject connections on the basis of the Hold
     Time.  The calculated value indicates the maximum number of
     seconds that may elapse between the receipt of successive
     KEEPALIVE and/or UPDATE messages from the sender.

  BGP Identifier:

     This 4-octet unsigned integer indicates the BGP Identifier of
     the sender.  A given BGP speaker sets the value of its BGP
     Identifier to an IP address that is assigned to that BGP
     speaker.  The value of the BGP Identifier is determined upon
     startup and is the same for every local interface and BGP peer.

  Optional Parameters Length:

     This 1-octet unsigned integer indicates the total length of the
     Optional Parameters field in octets.  If the value of this
     field is zero, no Optional Parameters are present.

  Optional Parameters:

     This field contains a list of optional parameters, in which
     each parameter is encoded as a <Parameter Type, Parameter
     Length, Parameter Value> triplet.

     0                   1
     0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5
     +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-...
     |  Parm. Type   | Parm. Length  |  Parameter Value (variable)
     +-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-...

     Parameter Type is a one octet field that unambiguously
     identifies individual parameters.  Parameter Length is a one
     octet field that contains the length of the Parameter Value
     field in octets.  Parameter Value is a variable length field
     that is interpreted according to the value of the Parameter
     Type field.

     \[RFC3392\] defines the Capabilities Optional Parameter.

The minimum length of the OPEN message is 29 octets (including the message header).

include bgp_optional_params

function queued_opt_param : optional_parameter.arr
function queued_opt_param_len : stream_pos

relation open_message_recv(I:bgp_id)


object bgp_open_message = {
    type this = struct {
        pversion: version,
        my_as_number: as_number,
        hold_time: seconds,
        bgp_identifier: bgp_id,
        opt_parm_len: stream_pos,
        opt_params: optional_parameter.arr
    }
    instance idx : unbounded_sequence
    instance arr : array(idx,this)
}

action bgp_open_message_event(src:bgp_id,dst:bgp_id,bgp_message:bgp_open_message) = {}

around bgp_open_message_event(src:bgp_id,dst:bgp_id,bgp_message:bgp_open_message) {
    require isup(bgpid_to_endpoint(src));
    require ~open_message_recv(src);
    ...
    require isup(bgpid_to_endpoint(src));
    open_message_recv(src) := true;
}