Add RecordFlux specification for a subset of DTLS 1.3 and refine TLS 1.3

Ref. eng/recordflux/RecordFlux#1221

examples/specs/tls_alert.rflx

@@ -1,45 +1,20 @@
-package TLS_Alert is
+with Tls_Parameters;
 
-   -- RFC 8446
+package TLS_Alert is
 
-   type Alert_Level is (WARNING => 1, FATAL => 2) with Size => 8;
+   -- TLS 1.3 (RFC 8446) and DTLS 1.3 (RFC 9147)
 
-   type Alert_Description is
-      (CLOSE_NOTIFY                    =>   0,
-       UNEXPECTED_MESSAGE              =>  10,
-       BAD_RECORD_MAC                  =>  20,
-       RECORD_OVERFLOW                 =>  22,
-       HANDSHAKE_FAILURE               =>  40,
-       BAD_CERTIFICATE                 =>  42,
-       UNSUPPORTED_CERTIFICATE         =>  43,
-       CERTIFICATE_REVOKED             =>  44,
-       CERTIFICATE_EXPIRED             =>  45,
-       CERTIFICATE_UNKNOWN             =>  46,
-       ILLEGAL_PARAMETER               =>  47,
-       UNKNOWN_CA                      =>  48,
-       ACCESS_DENIED                   =>  49,
-       DECODE_ERROR                    =>  50,
-       DECRYPT_ERROR                   =>  51,
-       PROTOCOL_VERSION                =>  70,
-       INSUFFICIENT_SECURITY           =>  71,
-       INTERNAL_ERROR                  =>  80,
-       INAPPROPRIATE_FALLBACK          =>  86,
-       USER_CANCELED                   =>  90,
-       MISSING_EXTENSION               => 109,
-       UNSUPPORTED_EXTENSION           => 110,
-       UNRECOGNIZED_NAME               => 112,
-       BAD_CERTIFICATE_STATUS_RESPONSE => 113,
-       UNKNOWN_PSK_IDENTITY            => 115,
-       CERTIFICATE_REQUIRED            => 116,
-       NO_APPLICATION_PROTOCOL         => 120)
-   with Size => 8;
+   type Alert_Level is (Warning => 1, Fatal => 2) with Size => 8;
 
    type Alert is
       message
          Level : Alert_Level;
-         Description : Alert_Description
-            if (Level = WARNING and (Description = CLOSE_NOTIFY or Description = USER_CANCELED))
-               or (Level = FATAL and Description /= CLOSE_NOTIFY and Description /= USER_CANCELED);
+         Description : Tls_Parameters::TLS_Alerts
+            if (Level = Warning and
+                  (Description = Tls_Parameters::Close_Notify
+                     or Description = Tls_Parameters::User_Canceled))
+               or (Level = Fatal and Description /= Tls_Parameters::Close_Notify
+                     and Description /= Tls_Parameters::User_Canceled);
       end message;
 
 end TLS_Alert;

examples/specs/tls_common.rflx

@@ -0,0 +1,28 @@
+package TLS_Common is
+
+   -- Common definitions for TLS 1.3 (RFC 8446) and DTLS 1.3 (RFC 9147)
+
+   -- TLS and DTLS versions.
+   --
+   -- Notes:
+   -- 1. TLS 1.3 and DTLS 1.3 are to some extent backwards compatible. Hence, they indicate lower
+   --    versions in certain (legacy) fields. Hence, it is necessary to keep those values here even
+   --    for strict 1.3 compatibility.
+   -- 2. The values in the type below are also used to distinguish between DTLS and TLS in some
+   --    context. Hence, when this type is modified the referencing specifications need to be
+   --    analyzed and potentially modified accordingly.
+   --    * For instance, there exist intermediate non-standard versions, such as 16#7F1C# for TLS
+   --      1.3 draft 28 etc. Some tools (e.g. Wireshark) support these versions. However, they have
+   --      been excluded from here currently.
+   type Protocol_Version is
+      (TLS_1_0 => 16#0301#,
+       TLS_1_1 => 16#0302#,
+       TLS_1_2 => 16#0303#,
+       TLS_1_3 => 16#0304#,
+       DTLS_1_0 => 16#FEFF#,
+       -- DTLS 1.1 does not exist
+       DTLS_1_2 => 16#FEFD#,
+       DTLS_1_3 => 16#FEFC#)
+   with Size => 16;
+
+end TLS_Common;