tls_handshake.rflx

package TLS_Handshake is

   -- RFC 8446

   type Handshake_Type is
      (HT_CLIENT_HELLO           =>   1,
       HT_SERVER_HELLO           =>   2,
       HT_NEW_SESSION_TICKET     =>   4,
       HT_END_OF_EARLY_DATA      =>   5,
       HT_ENCRYPTED_EXTENSIONS   =>   8,
       HT_CERTIFICATE            =>  11,
       HT_CERTIFICATE_REQUEST    =>  13,
       HT_CERTIFICATE_VERIFY     =>  15,
       HT_FINISHED               =>  20,
       HT_KEY_UPDATE             =>  24,
       HT_COMPRESSED_CERTIFICATE =>  25,  -- draft-ietf-tls-certificate-compression
       HT_MESSAGE_HASH           => 254)
   with Size => 8;

   type Length is mod 2 ** 24;

   type Handshake is
      message
         Tag : Handshake_Type;
         Length : Length;
         Payload : Opaque
            with Size => Length * 8;
      end message;

   -- Extensions

   type Extension_Type is
      (ET_SERVER_NAME                            =>  0,
       ET_MAX_FRAGMENT_LENGTH                    =>  1,
       ET_STATUS_REQUEST                         =>  5,  -- unsupported
       ET_SUPPORTED_GROUPS                       => 10,
       ET_SIGNATURE_ALGORITHMS                   => 13,
       ET_USE_SRTP                               => 14,  -- unsupported
       ET_HEARTBEAT                              => 15,
       ET_APPLICATION_LAYER_PROTOCOL_NEGOTIATION => 16,
       ET_SIGNED_CERTIFICATE_TIMESTAMP           => 18,  -- unsupported
       ET_CLIENT_CERTIFICATE_TYPE                => 19,  -- unsupported
       ET_SERVER_CERTIFICATE_TYPE                => 20,  -- unsupported
       ET_PADDING                                => 21,  -- unsupported
       ET_PRE_SHARED_KEY                         => 41,
       ET_EARLY_DATA                             => 42,
       ET_SUPPORTED_VERSIONS                     => 43,
       ET_COOKIE                                 => 44,
       ET_PSK_KEY_EXCHANGE_MODES                 => 45,
       ET_CERTIFICATE_AUTHORITIES                => 47,
       ET_OID_FILTERS                            => 48,
       ET_POST_HANDSHAKE_AUTH                    => 49,
       ET_SIGNATURE_ALGORITHMS_CERT              => 50,
       ET_KEY_SHARE                              => 51)
   with Size => 16, Always_Valid;

   type Data_Length is range 0 .. 2 ** 16 - 1 with Size => 16;

   type Extension is
      message
         Tag : Extension_Type;
         Data_Length : Data_Length;
         Data : Opaque
            with Size => 8 * Data_Length;
      end message;

   type Extensions is sequence of Extension;

   type CH_Extension is new Extension;
   type CH_Extensions is sequence of CH_Extension;

   type SH_Extension is new Extension;
   type SH_Extensions is sequence of SH_Extension;

   type HRR_Extension is new Extension;
   type HRR_Extensions is sequence of HRR_Extension;

   type EE_Extension is new Extension;
   type EE_Extensions is sequence of EE_Extension;

   type CT_Extension is new Extension;
   type CT_Extensions is sequence of CT_Extension;

   type CR_Extension is new Extension;
   type CR_Extensions is sequence of CR_Extension;

   type NST_Extension is new Extension;
   type NST_Extensions is sequence of NST_Extension;

   -- Key Exchange Messages

   type Protocol_Version is
      (TLS_1_0 => 16#0301#,
       TLS_1_1 => 16#0302#,
       TLS_1_2 => 16#0303#,
       TLS_1_3 => 16#0304#)
   with Size => 16, Always_Valid;

   type Legacy_Session_ID_Length is range 0 .. 32 with Size => 8;

   type Cipher_Suites_Length is range 2 .. 2 ** 16 - 2 with Size => 16;

   type Cipher_Suite is
      (TLS_AES_128_GCM_SHA256       => 16#1301#,
       TLS_AES_256_GCM_SHA384       => 16#1302#,
       TLS_CHACHA20_POLY1305_SHA256 => 16#1303#,
       TLS_AES_128_CCM_SHA256       => 16#1304#,
       TLS_AES_128_CCM_8_SHA256     => 16#1305#)
   with Size => 16, Always_Valid;

   type Cipher_Suites is sequence of Cipher_Suite;

   type Legacy_Compression_Methods_Length is range 1 .. 1 with Size => 8;

   type Client_Hello_Extensions_Length is range 8 .. 2 ** 16 - 1 with Size => 16;

   type Client_Hello is
      message
         Legacy_Version : Protocol_Version
            if Legacy_Version = TLS_1_2;
         Random : Opaque
            with Size => 32 * 8;
         Legacy_Session_ID_Length : Legacy_Session_ID_Length;
         Legacy_Session_ID : Opaque
            with Size => Legacy_Session_ID_Length * 8;
         Cipher_Suites_Length : Cipher_Suites_Length;
         Cipher_Suites : Cipher_Suites
            with Size => Cipher_Suites_Length * 8;
         Legacy_Compression_Methods_Length : Legacy_Compression_Methods_Length;
         Legacy_Compression_Methods : Opaque
            with Size => Legacy_Compression_Methods_Length * 8
            then null
               if Message'Last / 8 = Legacy_Compression_Methods'Last / 8
            then Extensions_Length
               if Message'Last / 8 /= Legacy_Compression_Methods'Last / 8;
         Extensions_Length : Client_Hello_Extensions_Length;
         Extensions : CH_Extensions
            with Size => Extensions_Length * 8;
      end message;

   for Handshake use (Payload => Client_Hello)
      if Tag = HT_CLIENT_HELLO;

   type Legacy_Compression_Method is range 0 .. 0 with Size => 8;
   type Server_Hello_Extensions_Length is range 6 .. 2 ** 16 - 1 with Size => 16;

   type Server_Hello is
      message
         Legacy_Version : Protocol_Version
            if Legacy_Version = TLS_1_2;
         Random : Opaque
            with Size => 32 * 8;
         Legacy_Session_ID_Length : Legacy_Session_ID_Length;
         Legacy_Session_ID : Opaque
            with Size => Legacy_Session_ID_Length * 8;
         Cipher_Suite : Cipher_Suite;
         Legacy_Compression_Method : Legacy_Compression_Method;
         Extensions_Length : Server_Hello_Extensions_Length
            then Extensions
               with Size => Extensions_Length * 8
               if Random /= [16#CF#, 16#21#, 16#AD#, 16#74#, 16#E5#, 16#9A#, 16#61#, 16#11#, 16#BE#,
                             16#1D#, 16#8C#, 16#02#, 16#1E#, 16#65#, 16#B8#, 16#91#, 16#C2#, 16#A2#,
                             16#11#, 16#16#, 16#7A#, 16#BB#, 16#8C#, 16#5E#, 16#07#, 16#9E#, 16#09#,
                             16#E2#, 16#C8#, 16#A8#, 16#33#, 16#9C#]
            then HRR_Extensions
               with Size => Extensions_Length * 8
               if Random = [16#CF#, 16#21#, 16#AD#, 16#74#, 16#E5#, 16#9A#, 16#61#, 16#11#, 16#BE#,
                            16#1D#, 16#8C#, 16#02#, 16#1E#, 16#65#, 16#B8#, 16#91#, 16#C2#, 16#A2#,
                            16#11#, 16#16#, 16#7A#, 16#BB#, 16#8C#, 16#5E#, 16#07#, 16#9E#, 16#09#,
                            16#E2#, 16#C8#, 16#A8#, 16#33#, 16#9C#];
         Extensions : SH_Extensions
            then null;
         HRR_Extensions : HRR_Extensions;
      end message;

   for Handshake use (Payload => Server_Hello)
      if Tag = HT_SERVER_HELLO;

   -- Server Parameters

   type Encrypted_Extensions_Length is range 0 .. 2 ** 16 - 1 with Size => 16;

   type Encrypted_Extensions is
      message
         Length : Encrypted_Extensions_Length;
         Extensions : EE_Extensions
            with Size => Length * 8;
      end message;

   for Handshake use (Payload => Encrypted_Extensions)
      if Tag = HT_ENCRYPTED_EXTENSIONS;

   type Certificate_Request_Context_Length is range 0 .. 2 ** 8 - 1 with Size => 8;
   type Certificate_Request_Extensions_Length is range 2 .. 2 ** 16 - 1 with Size => 16;

   type Certificate_Request is
      message
         Certificate_Request_Context_Length : Certificate_Request_Context_Length;
         Certificate_Request_Context : Opaque
            with Size => Certificate_Request_Context_Length * 8;
         Extensions_Length : Certificate_Request_Extensions_Length;
         Extensions : CR_Extensions
            with Size => Extensions_Length * 8;
      end message;

   for Handshake use (Payload => Certificate_Request)
      if Tag = HT_CERTIFICATE_REQUEST;

   -- Authentication Messages

   type Certificate_Type is (X509 => 0, RAW_PUBLIC_KEY => 2) with Size => 8;
   type ASN1_Subject_Public_Key_Info_Length is range 1 .. 2 ** 24 - 1 with Size => 24;
   type Cert_Data_Length is range 1 .. 2 ** 24 - 1 with Size => 24;
   type Certificate_Extensions_Length is range 0 .. 2 ** 16 - 1 with Size => 16;

   type Certificate_Entry is
      message
         Cert_Data_Length : Cert_Data_Length;
         Cert_Data : Opaque
            with Size => Cert_Data_Length * 8;
         Extensions_Length : Certificate_Extensions_Length;
         Extensions : CT_Extensions
            with Size => Extensions_Length * 8;
      end message;

   type Certificate_List_Length is range 0 .. 2 ** 24 - 1 with Size => 24;
   type Certificate_Entries is sequence of Certificate_Entry;

   type Certificate is
      message
         Certificate_Request_Context_Length : Certificate_Request_Context_Length;
         Certificate_Request_Context : Opaque
            with Size => Certificate_Request_Context_Length * 8;
         Certificate_List_Length : Certificate_List_Length;
         Certificate_List : Certificate_Entries
            with Size => Certificate_List_Length * 8;
      end message;

   for Handshake use (Payload => Certificate)
      if Tag = HT_CERTIFICATE;

   type Signature_Scheme is
      (-- RSASSA-PKCS1-v1_5 algorithms
       RSA_PKCS1_SHA256       => 16#0401#,
       RSA_PKCS1_SHA384       => 16#0501#,
       RSA_PKCS1_SHA512       => 16#0601#,
       -- ECDSA algorithms
       ECDSA_SECP256R1_SHA256 => 16#0403#,
       ECDSA_SECP384R1_SHA384 => 16#0503#,
       ECDSA_SECP521R1_SHA512 => 16#0603#,
       -- RSASSA-PSS algorithms with public key OID rsaEncryption
       RSA_PSS_RSAE_SHA256    => 16#0804#,
       RSA_PSS_RSAE_SHA384    => 16#0805#,
       RSA_PSS_RSAE_SHA512    => 16#0806#,
       -- EdDSA algorithms
       ED25519                => 16#0807#,
       ED448                  => 16#0808#,
       -- RSASSA-PSS algorithms with public key OID RSASSA-PSS
       RSA_PSS_PSS_SHA256     => 16#0809#,
       RSA_PSS_PSS_SHA384     => 16#080A#,
       RSA_PSS_PSS_SHA512     => 16#080B#,
       -- Legacy algorithms
       RSA_PKCS1_SHA1         => 16#0201#,
       ECDSA_SHA1             => 16#0203#)
   with Size => 16, Always_Valid;

   type Signature_Length is range 0 .. 2 ** 16 - 1 with Size => 16;

   type Certificate_Verify is
      message
         Algorithm : Signature_Scheme;
         Signature_Length : Signature_Length;
         Signature : Opaque
            with Size => Signature_Length * 8;
      end message;

   for Handshake use (Payload => Certificate_Verify)
      if Tag = HT_CERTIFICATE_VERIFY;

   type Finished is
      message
         Verify_Data : Opaque
            with Size => Message'Size;
      end message;

   for Handshake use (Payload => Finished)
      if Tag = HT_FINISHED;

   -- End of Early Data

   type End_Of_Early_Data is null message;

   for Handshake use (Payload => End_Of_Early_Data)
      if Tag = HT_END_OF_EARLY_DATA;

   -- Post-Handshake Messages

   type Ticket_Lifetime is mod 2 ** 32;
   type Ticket_Age_Add is mod 2 ** 32;
   type Ticket_Nonce_Length is range 0 .. 255 with Size => 8;
   type Ticket_Length is range 1 .. 2 ** 16 - 1 with Size => 16;
   type New_Session_Ticket_Extensions_Length is range 0 .. 2 ** 16 - 2 with Size => 16;

   type New_Session_Ticket is
      message
         Ticket_Lifetime : Ticket_Lifetime;
         Ticket_Age_Add : Ticket_Age_Add;
         Ticket_Nonce_Length : Ticket_Nonce_Length;
         Ticket_Nonce : Opaque
            with Size => Ticket_Nonce_Length * 8;
         Ticket_Length : Ticket_Length;
         Ticket : Opaque
            with Size => Ticket_Length * 8;
         Extensions_Length : New_Session_Ticket_Extensions_Length;
         Extensions : NST_Extensions
            with Size => Extensions_Length * 8;
      end message;

   for Handshake use (Payload => New_Session_Ticket)
      if Tag = HT_NEW_SESSION_TICKET;

   type Key_Update_Request is (UPDATE_NOT_REQUESTED => 0, UPDATE_REQUESTED => 1) with Size => 8;

   type Key_Update is
      message
         Request_Update : Key_Update_Request;
      end message;

   for Handshake use (Payload => Key_Update)
      if Tag = HT_KEY_UPDATE;

   -- Server Name Indication Extension

   type Name_Type is (HOST_NAME => 0) with Size => 8;
   type Name_Length is range 1 .. 2 ** 16 - 1 with Size => 16;

   type Server_Name is
      message
         Name_Type : Name_Type;
         Length : Name_Length;
         Name : Opaque
            with Size => 8 * Length;
      end message;

   type Server_Name_List_Length is range 1 .. 2 ** 16 - 1 with Size => 16;
   type Server_Names is sequence of Server_Name;

   type Server_Name_List is
      message
         Length : Server_Name_List_Length;
         Server_Name_List : Server_Names
            with Size => 8 * Length;
      end message;

   for CH_Extension use (Data => Server_Name_List)
      if Tag = ET_SERVER_NAME;
   for EE_Extension use (Data => Server_Name_List)
      if Tag = ET_SERVER_NAME;

   -- Max Fragment Length

   type Max_Fragment_Length_Value is
      (MAX_FRAGMENT_LENGTH_9  => 1,
       MAX_FRAGMENT_LENGTH_10 => 2,
       MAX_FRAGMENT_LENGTH_11 => 3,
       MAX_FRAGMENT_LENGTH_12 => 4)
   with Size => 8;

   type Max_Fragment_Length is
      message
         Max_Fragment_Length : Max_Fragment_Length_Value;
      end message;

   for CH_Extension use (Data => Max_Fragment_Length)
      if Tag = ET_MAX_FRAGMENT_LENGTH;
   for EE_Extension use (Data => Max_Fragment_Length)
      if Tag = ET_MAX_FRAGMENT_LENGTH;

   -- Supported Versions Extension

   type Supported_Versions_Length is range 2 .. 254 with Size => 8;
   type Protocol_Versions is sequence of Protocol_Version;

   type Supported_Versions is
      message
         Length : Supported_Versions_Length;
         Versions : Protocol_Versions
            with Size => 8 * Length;
      end message;

   type Supported_Version is
      message
         Version : Protocol_Version;
      end message;

   for CH_Extension use (Data => Supported_Versions)
      if Tag = ET_SUPPORTED_VERSIONS;
   for SH_Extension use (Data => Supported_Version)
      if Tag = ET_SUPPORTED_VERSIONS;
   for HRR_Extension use (Data => Supported_Version)
      if Tag = ET_SUPPORTED_VERSIONS;

   -- Cookie Extension

   type Cookie_Length is range 1 .. 2 ** 16 - 1 with Size => 16;

   type Cookie is
      message
         Length : Cookie_Length;
         Cookie : Opaque
            with Size => 8 * Length;
      end message;

   for CH_Extension use (Data => Cookie)
      if Tag = ET_COOKIE;
   for HRR_Extension use (Data => Cookie)
      if Tag = ET_COOKIE;

   -- Signature Algorithms Extension

   type Signature_Algorithms_Length is range 2 .. 2 ** 16 - 2 with Size => 16;
   type Signature_Schemes is sequence of Signature_Scheme;

   type Signature_Algorithms is
      message
         Length : Signature_Algorithms_Length;
         Algorithms : Signature_Schemes
            with Size => 8 * Length;
      end message;

   for CH_Extension use (Data => Signature_Algorithms)
      if Tag = ET_SIGNATURE_ALGORITHMS;
   for CR_Extension use (Data => Signature_Algorithms)
      if Tag = ET_SIGNATURE_ALGORITHMS;

   type Signature_Algorithms_Cert is
      message
         Length : Signature_Algorithms_Length;
         Algorithms : Signature_Schemes
            with Size => 8 * Length;
      end message;

   for CH_Extension use (Data => Signature_Algorithms_Cert)
      if Tag = ET_SIGNATURE_ALGORITHMS_CERT;
   for CR_Extension use (Data => Signature_Algorithms_Cert)
      if Tag = ET_SIGNATURE_ALGORITHMS_CERT;

   -- Heartbeat Extension

   type Heartbeat_Mode is (PEER_ALLOWED_TO_SEND => 1, PEER_NOT_ALLOWED_TO_SEND => 2) with Size => 8;

   type Heartbeat is
      message
         Mode : Heartbeat_Mode;
      end message;

   -- Certificate Authorities Extension

   type Certificate_Authorities_Length is range 3 .. 2 ** 16 - 1 with Size => 16;
   type Distinguished_Name_Length is range 1 .. 2 ** 16 - 1 with Size => 16;

   type Distinguished_Name is
      message
         Length : Distinguished_Name_Length;
         Name : Opaque
            with Size => 8 * Length;
      end message;

   type Distinguished_Names is sequence of Distinguished_Name;

   type Certificate_Authorities is
      message
         Length : Certificate_Authorities_Length;
         Authorities : Distinguished_Names
            with Size => 8 * Length;
      end message;

   for CH_Extension use (Data => Certificate_Authorities)
      if Tag = ET_CERTIFICATE_AUTHORITIES;
   for CR_Extension use (Data => Certificate_Authorities)
      if Tag = ET_CERTIFICATE_AUTHORITIES;

   -- OID Filters Extension

   type Filters_Length is range 0 .. 2 ** 16 - 1 with Size => 16;
   type OID_Length is range 1 .. 2 ** 8 - 1 with Size => 8;
   type Values_Length is range 0 .. 2 ** 16 - 1 with Size => 16;

   type Filter is
      message
         OID_Length : OID_Length;
         OID : Opaque
            with Size => 8 * OID_Length;
         Values_Length : Values_Length;
         Values : Opaque
            with Size => 8 * Values_Length;
      end message;

   type Filters is sequence of Filter;

   type OID_Filters is
      message
         Length : Filters_Length;
         Filters : Filters
            with Size => 8 * Length;
      end message;

   for CR_Extension use (Data => OID_Filters)
      if Tag = ET_OID_FILTERS;

   -- Post-Handshake Client Authentication Extension

   type Post_Handshake_Auth is null message;

   for CH_Extension use (Data => Post_Handshake_Auth)
      if Tag = ET_POST_HANDSHAKE_AUTH;

   -- Supported Groups Extension

   type Supported_Groups_Length is range 2 .. 2 ** 16 - 1 with Size => 16;

   type Named_Group is
      (-- Elliptic Curve Groups (ECDHE)
       SECP256R1 => 16#0017#,
       SECP384R1 => 16#0018#,
       SECP521R1 => 16#0019#,
       X25519    => 16#001D#,
       X448      => 16#001E#,
       -- Finite Field Groups (DHE)
       FFDHE2048 => 16#0100#,
       FFDHE3072 => 16#0101#,
       FFDHE4096 => 16#0102#,
       FFDHE6144 => 16#0103#,
       FFDHE8192 => 16#0104#)
   with Size => 16, Always_Valid;

   type Named_Groups is sequence of Named_Group;

   type Supported_Groups is
      message
         Length : Supported_Groups_Length;
         Groups : Named_Groups
            with Size => 8 * Length;
      end message;

   for CH_Extension use (Data => Supported_Groups)
      if Tag = ET_SUPPORTED_GROUPS;
   for EE_Extension use (Data => Supported_Groups)
      if Tag = ET_SUPPORTED_GROUPS;

   -- Key Share Extension

   type Key_Exchange_Length is range 1 .. 2 ** 16 - 1 with Size => 16;

   type Key_Share_Entry is
      message
         Group : Named_Group;
         Length : Key_Exchange_Length;
         Key_Exchange : Opaque
            with Size => 8 * Length;
      end message;

   type Key_Share_Entries is sequence of Key_Share_Entry;

   type Key_Shares_Length is range 0 .. 2 ** 16 - 1 with Size => 16;

   type Key_Share_CH is
      message
         Length : Key_Shares_Length;
         Shares : Key_Share_Entries
            with Size => 8 * Length;
      end message;

   type Key_Share_SH is new Key_Share_Entry;

   type Key_Share_HRR is
      message
         Selected_Group : Named_Group;
      end message;

   for CH_Extension use (Data => Key_Share_CH)
      if Tag = ET_KEY_SHARE;
   for SH_Extension use (Data => Key_Share_SH)
      if Tag = ET_KEY_SHARE;
   for HRR_Extension use (Data => Key_Share_HRR)
      if Tag = ET_KEY_SHARE;

   -- Pre-Shared Key Exchange Modes Extension

   type PSK_Key_Exchange_Modes_Length is range 1 .. 255 with Size => 8;

   type Key_Exchange_Mode is
      (PSK_KE     => 0,
       PSK_DHE_KE => 1)
   with Size => 8, Always_Valid;

   type Key_Exchange_Modes is sequence of Key_Exchange_Mode;

   type PSK_Key_Exchange_Modes is
      message
         Length : PSK_Key_Exchange_Modes_Length;
         Modes : Key_Exchange_Modes
            with Size => 8 * Length;
      end message;

   for CH_Extension use (Data => PSK_Key_Exchange_Modes)
      if Tag = ET_PSK_KEY_EXCHANGE_MODES;

   -- Early Data Indication Extension

   type Max_Early_Data_Size is mod 2 ** 32;

   type Early_Data_Indication is
      message
         Max_Early_Data_Size : Max_Early_Data_Size;
      end message;

   type Early_Data is null message;

   for CH_Extension use (Data => Early_Data)
      if Tag = ET_EARLY_DATA;
   for EE_Extension use (Data => Early_Data)
      if Tag = ET_EARLY_DATA;
   for NST_Extension use (Data => Early_Data_Indication)
      if Tag = ET_EARLY_DATA;

   -- Pre-Shared Key Extension

   type Identity_Length is range 1 .. 2 ** 16 - 1 with Size => 16;
   type Obfuscated_Ticket_Age is mod 2 ** 32;

   type PSK_Identity is
      message
         Length : Identity_Length;
         Identity : Opaque
            with Size => 8 * Length;
         Obfuscated_Ticket_Age : Obfuscated_Ticket_Age;
      end message;

   type PSK_Identities is sequence of PSK_Identity;

   type PSK_Binder_Entry_Length is range 32 .. 255 with Size => 8;

   type PSK_Binder_Entry is
      message
         Length : PSK_Binder_Entry_Length;
         PSK_Binder_Entry : Opaque
            with Size => 8 * Length;
      end message;

   type PSK_Binder_Entries is sequence of PSK_Binder_Entry;

   type Identities_Length is range 7 .. 2 ** 16 - 1 with Size => 16;
   type Binders_Length is range 33 .. 2 ** 16 - 1 with Size => 16;

   type Pre_Shared_Key_CH is
      message
         Identities_Length : Identities_Length;
         Identities : PSK_Identities
            with Size => 8 * Identities_Length;
         Binders_Length : Binders_Length;
         Binders : PSK_Binder_Entries
            with Size => 8 * Binders_Length;
      end message;

   type Identity_Index is mod 2 ** 16;

   type Pre_Shared_Key_SH is
      message
         Selected_Identity : Identity_Index;
      end message;

   for CH_Extension use (Data => Pre_Shared_Key_CH)
      if Tag = ET_PRE_SHARED_KEY;
   for SH_Extension use (Data => Pre_Shared_Key_SH)
      if Tag = ET_PRE_SHARED_KEY;

   -- Application-Layer Protocol Negotiation Extension

   type Protocol_Name_Length is range 1 .. 2 ** 8 - 1 with Size => 8;

   type Protocol_Name is
      message
         Length : Protocol_Name_Length;
         Name : Opaque
            with Size => 8 * Length;
      end message;

   type Protocol_Names is sequence of Protocol_Name;
   type Protocol_Name_List_Length is range 2 .. 2 ** 16 - 1 with Size => 16;

   type Protocol_Name_List is
      message
         Length : Protocol_Name_List_Length;
         Protocol_Name_List : Protocol_Names
            with Size => 8 * Length;
      end message;

   for CH_Extension use (Data => Protocol_Name_List)
      if Tag = ET_APPLICATION_LAYER_PROTOCOL_NEGOTIATION;
   for EE_Extension use (Data => Protocol_Name_List)
      if Tag = ET_APPLICATION_LAYER_PROTOCOL_NEGOTIATION;

end TLS_Handshake;