%%% Handshake Protocol

       enum {
           hello_request_RESERVED(0),
           client_hello(1),
           server_hello(2),
           hello_verify_request_RESERVED(3),
           new_session_ticket(4),
           end_of_early_data(5),
           hello_retry_request(6),
           encrypted_extensions(8),
           certificate(11),
           server_key_exchange_RESERVED(12),
           certificate_request(13),
           server_hello_done_RESERVED(14),
           certificate_verify(15),
           client_key_exchange_RESERVED(16),
           finished(20),
           key_update(24),
           message_hash(254),
           (255)
       } HandshakeType;

       struct {
           HandshakeType msg_type;    /* handshake type */
           uint24 length;             /* bytes in message */
           select (Handshake.msg_type) {
               case client_hello:          ClientHello;
               case server_hello:          ServerHello;
               case end_of_early_data:     EndOfEarlyData;
               case hello_retry_request:   HelloRetryRequest;
               case encrypted_extensions:  EncryptedExtensions;
               case certificate_request:   CertificateRequest;
               case certificate:           Certificate;
               case certificate_verify:    CertificateVerify;
               case finished:              Finished;
               case new_session_ticket:    NewSessionTicket;
               case key_update:            KeyUpdate;
           } body;
       } Handshake;

---snip---

Handshake messages are constructed with the macro handshake_record('num', body...) which simply produces the tuple <'24', 'num', body...> where 'num' is the enum value from HandshakeType, and body is the contents of the message as defined later.

We omit a length parameter.

Cryptographic Negotiation

TLS cryptographic negotiation proceeds by the client offering the following four sets of options in its ClientHello:

• A list of cipher suites which indicates the AEAD algorithm/HKDF hash pairs which the client supports.
• A "supported_groups" () extension which indicates the (EC)DHE groups which the client supports and a "key_share" () extension which contains (EC)DHE shares for some or all of these groups.
• A "signature_algorithms" () extension which indicates the signature algorithms which the client can accept.
• A "pre_shared_key" () extension which contains a list of symmetric key identities known to the client and a "psk_key_exchange_modes" () extension which indicates the key exchange modes that may be used with PSKs. If the server does not select a PSK, then the first three of these options are entirely orthogonal: the server independently selects a cipher suite, an (EC)DHE group and key share for key establishment, and a signature algorithm/certificate pair to authenticate itself to the client. If there is overlap in the "supported_groups" extension but the client did not offer a compatible "key_share" extension, then the server will respond with a HelloRetryRequest () message. If there is no overlap in "supported_groups" then the server MUST abort the handshake.

If the server selects a PSK, then it MUST also select a key establishment mode from the set indicated by client's "psk_key_exchange_modes" extension (PSK alone or with (EC)DHE). Note that if the PSK can be used without (EC)DHE then non-overlap in the "supported_groups" parameters need not be fatal, as it is in the non-PSK case discussed in the previous paragraph.

The server indicates its selected parameters in the ServerHello as follows:

• If PSK is being used then the server will send a "pre_shared_key" extension indicating the selected key.
• If PSK is not being used, then (EC)DHE and certificate-based authentication are always used.
• When (EC)DHE is in use, the server will also provide a "key_share" extension.
• When authenticating via a certificate (i.e., when a PSK is not in use), the server will send the Certificate () and CertificateVerify () messages.

If the server is unable to negotiate a supported set of parameters (i.e., there is no overlap between the client and server parameters), it MUST abort the handshake with either a "handshake_failure" or "insufficient_security" fatal alert (see ).

We currently support a very limited amount of negotiation. However, this is quite a large improvement over previous symbolic models.

We support negotiation of handshake modes in the following way: The client in their initial message can include support for both PSK modes. The server can optionally choose either of these, or even fall back to a vanilla handshake.

Furthermore, we do include some support for group negotiation, which is detailed later.

When a client first connects to a server, it is REQUIRED to send the ClientHello as its first message. The client will also send a ClientHello when the server has responded to its ClientHello with a HelloRetryRequest. In that case, the client MUST send the same ClientHello (without modification) except:

• If a "key_share" extension was supplied in the HelloRetryRequest, replacing the list of shares with a list containing a single KeyShareEntry from the indicated group.

• Removing the "early_data" extension () if one was present. Early data is not permitted after HelloRetryRequest.

• Including a "cookie" extension if one was provided in the HelloRetryRequest.

• Updating the "pre_shared_key" extension if present by recomputing the "obfuscated_ticket_age" and binder values and (optionally) removing any PSKs which are incompatible with the server's indicated cipher suite.

---snip---

We represent a single instantation of a TLS client using the state fact: State(C1, tid, C, S, ClientState). There are actually multiple macros which are unfolded here. First, the macro State(X, ...) = State_X(...) which is a convenience. By writing rules which take in specifc state facts, we effectively constrain the state machine to only follow legal moves. That is, after client_hello, the fact State_C1(...) is constructed. This can only be consumed by hello_retry_request and recv_server_hello (ignoring PSK variants for now).

The other macro is ClientState which expands to a large tuple of variables, but can thought of as a struct containing all state variables.

For the HelloRetryRequest scenario, the client sends all the same variables as previously generated, but removes the "early_data_indication". We do not currently cover the "cookie" extension.

We cover the specifics of the "key_share" and "pre_shared_key" selection later.

Structure of this message:

%%% Key Exchange Messages

   uint16 ProtocolVersion;
   opaque Random[32];

   uint8 CipherSuite[2];    /* Cryptographic suite selector */

   struct {
       ProtocolVersion legacy_version = 0x0303;    /* TLS v1.2 */
       Random random;
       opaque legacy_session_id<0..32>;
       CipherSuite cipher_suites<2..2^16-2>;
       opaque legacy_compression_methods<1..2^8-1>;
       Extension extensions<8..2^16-1>;
   } ClientHello;

---snip---

legacy_version ---snip---

We define the ClientHello message as a macro defined in the following way:

define(<!ProtocolVersion!>, <!'0x0303'!>)
define(<!ClientRandom!>, <!nc!>)
define(<!ClientHello!>, <!handshake_record('1',
  ProtocolVersion,
  ClientRandom,
  '0', // legacy_session_id
  $cipher_suites,
  '0', // legacy_compression_methods
  ClientHelloExtensions 
)!>)

where ClientHelloExtensions is defined before a specific rule in order to contain the relevant extensions.

random

32 bytes generated by a secure random number generator. See for additional information.

The random value is generated in the client_hello{_psk} rules as a fresh value Fr(~nc) which is guaranteed to be unpredictable and never repeats (unless used maliciously by an adversary).

legacy_session_id ---snip---

cipher_suites ---snip---

legacy_compression_methods ---snip---

We do not attempt to model cipher suite negotiation, nor compatability with older version of TLS and simply set both legacy_session_id and legacy_compression_methods to '0'

extensions

Clients request extended functionality from servers by sending data in the extensions field. The actual "Extension" format is defined in .

---snip---

We cover the extensions in more details later. For the different client hello rules, the extensions used are:

client_hello:

define(<!ClientHelloExtensions!>, <!<SupportedVersions, NamedGroupList,
 SignatureSchemeList, KeyShareCH >!>)

client_hello_psk:

define(<!ClientHelloExtensions!>, <!<
  SupportedVersions,
  NamedGroupList,
  KeyShareCH,
  PskKeyExchangeModes,
  PreSharedKeyExtensionCH,
  EarlyDataIndication
>!>)

After sending the ClientHello message, the client waits for a ServerHello or HelloRetryRequest message. If early data is in use, the client may transmit early application data while waiting for the next handshake message.

The state State_C1 is consumed by recv_hello_retry_request, recv_client_hello, recv_client_hello_psk and recv_client_hello_psk_dhe representing this.

Structure of this message:

%%% Key Exchange Messages

   struct {
       ProtocolVersion version;
       Random random;
       CipherSuite cipher_suite;
       Extension extensions<0..2^16-1>;
   } ServerHello;

define(<!ProtocolVersion!>, <!'0x0303'!>)
define(<!ServerRandom!>, <!ns!>)
define(<!ServerHello!>, <!handshake_record('2',
  ProtocolVersion,
  ServerRandom,
  $cipher_suite,
  ServerHelloExtensions
)!>)

---snip---

extensions

A list of extensions. The ServerHello MUST only include extensions which are required to establish the cryptographic context. Currently the only such extensions are "key_share" and "pre_shared_key". All current TLS 1.3 ServerHello messages will contain one of these two extensions.

---snip---

The ServerHello message behaves similarly to the ClientHello message. As before, we cover the extensions in more detail later. The Extensions sent are:

server_hello:

define(<!ServerHelloExtensions!>, <!<SignatureSchemeList, KeyShareSH>!>)

server_hello_psk_dhe:

define(<!ServerHelloExtensions!>, <!<
  SignatureSchemeList,
  KeyShareSH,
  PreSharedKeyExtensionSH,
  EarlyDataIndication
>!>)

server_hello_psk:

define(<!ServerHelloExtensions!>, <!<
  SignatureSchemeList,
  PreSharedKeyExtensionSH,
  EarlyDataIndication
>!>)

The server will send this message in response to a ClientHello message if it is able to find an acceptable set of parameters but the ClientHello does not contain sufficient information to proceed with the handshake.

Structure of this message:

%%% Key Exchange Messages

   struct {
       ProtocolVersion server_version;
       CipherSuite cipher_suite;
       Extension extensions<2..2^16-1>;
   } HelloRetryRequest;

The version, cipher_suite, and extensions fields have the same meanings as their corresponding values in the ServerHello. The server SHOULD send only the extensions necessary for the client to generate a correct ClientHello pair. As with ServerHello, a HelloRetryRequest MUST NOT contain any extensions that were not first offered by the client in its ClientHello, with the exception of optionally the "cookie" (see ) extension.

Upon receipt of a HelloRetryRequest, the client MUST verify that the extensions block is not empty and otherwise MUST abort the handshake with a "decode_error" alert. Clients MUST abort the handshake with an "illegal_parameter" alert if the HelloRetryRequest would not result in any change in the ClientHello. If a client receives a second HelloRetryRequest in the same connection (i.e., where the ClientHello was itself in response to a HelloRetryRequest), it MUST abort the handshake with an "unexpected_message" alert.

Otherwise, the client MUST process all extensions in the HelloRetryRequest and send a second updated ClientHello. The HelloRetryRequest extensions defined in this specification are:

• cookie (see )

• key_share (see )

In addition, in its updated ClientHello, the client SHOULD NOT offer any pre-shared keys associated with a hash other than that of the selected cipher suite. This allows the client to avoid having to compute partial hash transcripts for multiple hashes in the second ClientHello. A client which receives a cipher suite that was not offered MUST abort the handshake. Servers MUST ensure that they negotiate the same cipher suite when receiving a conformant updated ClientHello (if the server selects the cipher suite as the first step in the negotiation, then this will happen automatically). Upon receiving the ServerHello, clients MUST check that the cipher suite supplied in the ServerHello is the same as that in the HelloRetryRequest and otherwise abort the handshake with an "illegal_parameter" alert.

Capturing this process is one of the trickier aspects of the model. Currently, it does not seem feasible to have a selection process wherein the server takes two lists and outputs a selected group, or reject. Instead we model the following limited version of group negotiation:

   Client                        Server
supports g1, g2               supports g

<g1, g2>, <g1, g1^x> ---->  if g != g1

                    <----- HRR <g>

checks g2 == g 
<g1, g2>, <g2, g2^x2> ---->  checks g == g2

That is, the client always sends two groups as supported, and the server checks whether the provided key share g1^x is in the supported group g.

If not, the server responds with g in a hello retry request. The client makes sure this is equal to the other group, g2, and sends a new client hello.

At the start of the model, g1, g2, and g are not restricted (they are modelled as public variables $g1). And the server does not necessarily know that the client sends the same groups in both handshakes. This is an overapproximation which guarantees the following:

• If the server reaches server_hello then the server has negotiated a supported group (so $g is either $g1 or $g2)
• The server only does HRR if `$g != $g1'
• The server only does HRR once.

The above three guarantee that the client must have offered $g as a supported group with a key share entry either in the first flight, or the retry.

The message is defined as:

define(<!HelloRetryRequest!>, <!handshake_record('6',
    ProtocolVersion,
    HelloRetryRequestExtensions
)!>)

where extensions are defined as:

hello_retry_request:

define(<!HelloRetryRequestExtensions!>, <!<KeyShareHRR>!>)

hello_retry_request_psk:

define(<!HelloRetryRequestExtensions!>, <!<KeyShareHRR>!>)

We do not currently support the Cookie extension, nor the server storing state using this extension.

A number of TLS messages contain tag-length-value encoded extensions structures.

%%% Key Exchange Messages

   struct {
       ExtensionType extension_type;
       opaque extension_data<0..2^16-1>;
   } Extension;

   enum {
       server_name(0),                             /* RFC 6066 */
       max_fragment_length(1),                     /* RFC 6066 */
       status_request(5),                          /* RFC 6066 */
       supported_groups(10),                       /* RFC 4492, 7919 */
       signature_algorithms(13),                   /* RFC 5246 */
       use_srtp(14),                               /* RFC 5764 */
       heartbeat(15),                              /* RFC 6520 */
       application_layer_protocol_negotiation(16), /* RFC 7301 */
       signed_certificate_timestamp(18),           /* RFC 6962 */
       client_certificate_type(19),                /* RFC 7250 */
       server_certificate_type(20),                /* RFC 7250 */
       padding(21),                                /* RFC 7685 */
       key_share(40),                              /* [[this document]] */
       pre_shared_key(41),                         /* [[this document]] */
       early_data(42),                             /* [[this document]] */
       supported_versions(43),                     /* [[this document]] */
       cookie(44),                                 /* [[this document]] */
       psk_key_exchange_modes(45),                 /* [[this document]] */
       certificate_authorities(47),                /* [[this document]] */
       oid_filters(48),                            /* [[this document]] */
       post_handshake_auth(49),                    /* [[this document]] */
       (65535)
   } ExtensionType;

Here:

• "extension_type" identifies the particular extension type.

• "extension_data" contains information specific to the particular extension type.

The list of extension types is maintained by IANA as described in .

Similarly, we define extensions using the macro Extension which simply expands to a list, Extension('10', client_sg) = <'10', client_sg> for the support groups for example.

Extensions are generally structured in a request/response fashion, though some extensions are just indications with no corresponding response. The client sends its extension requests in the ClientHello message and the server sends its extension responses in the ServerHello, EncryptedExtensions, HelloRetryRequest and Certificate messages. The server sends extension requests in the CertificateRequest message which a client MAY respond to with a Certificate message. The server MAY also send unsolicited extensions in the NewSessionTicket, though the client does not respond directly to these.

---snip---

We model this text directly; the client and server only send a specific set of extensions/messages. Note that actions such as "aborting the handshake" are effectively modelled by the obvservation that no subsequent client/server rules can be used. We do not explicitly model sending alert messages.

%%% Version Extension

   struct {
       ProtocolVersion versions<2..254>;
   } SupportedVersions;

---snip---

define(<!SupportedVersions!>, <!Extension('43', '0x0304')!>)

We do not attempt to model the interaction between different specifications, nor downgrade protection.

Cookie

%%% Cookie Extension

   struct {
       opaque cookie<1..2^16-1>;
   } Cookie;

Cookies serve two primary purposes:

• Allowing the server to force the client to demonstrate reachability at their apparent network address (thus providing a measure of DoS protection). This is primarily useful for non-connection-oriented transports (see for an example of this).

• Allowing the server to offload state to the client, thus allowing it to send a HelloRetryRequest without storing any state. The server can do this by storing the hash of the ClientHello in the HelloRetryRequest cookie (protected with some suitable integrity algorithm).

When sending a HelloRetryRequest, the server MAY provide a "cookie" extension to the client (this is an exception to the usual rule that the only extensions that may be sent are those that appear in the ClientHello). When sending the new ClientHello, the client MUST copy the contents of the extension received in the HelloRetryRequest into a "cookie" extension in the new ClientHello. Clients MUST NOT use cookies in subsequent connections.

Currently we do not make use of the Cookie extension for either of these purposes. It might be an interesting extension of this work to verify that offloading state through the cookie is safe.

The client uses the "signature_algorithms" extension to indicate to the server which signature algorithms may be used in digital signatures. Clients which desire the server to authenticate itself via a certificate MUST send this extension.

---snip---

The "extension_data" field of this extension in a ClientHello contains a SignatureSchemeList value:

%%% Signature Algorithm Extension

   enum {
   ---snip---
   } SignatureScheme;

   struct {
       SignatureScheme supported_signature_algorithms<2..2^16-2>;
   } SignatureSchemeList;

---snip---

Due to our assumption of "perfect crypto" much of this extension is irrelevant. We simply model the offered list as some public knowledge parameter: define(<!SignatureSchemeList!>, <!Extension('13', $sig_algs)!>) and validate the integrity of those algorithms in the transcript.

--snip---

We do not model the certificate authorities extension.

The "post_handshake_auth" extension is used to indicate that a client is willing to perform post-handshake authentication . Servers MUST not send a post-handshake CertificateRequest to clients which do not offer this extension. Servers MUST NOT send this extension.

The "extension_data" field of the "post_handshake_auth" extension is zero length.

We will add this in future work. As with many of our extensions, we will model this as always being supported by the client, so the impact of adding this will be negligible.

When sent by the client, the "supported_groups" extension indicates the named groups which the client supports for key exchange, ordered from most preferred to least preferred.

--snip---

The "extension_data" field of this extension contains a "NamedGroupList" value:

%%% Supported Groups Extension

   enum {
       ---snip---
   } NamedGroup;

   struct {
       NamedGroup named_group_list<2..2^16-1>;
   } NamedGroupList;

---snip---

We covered the logic behind the group selection in the HelloRetryRequest section. We define the extension as the list:

define(<!NamedGroupList!>, <!Extension('10', client_sg)!>)

where client_sg is defined locally by the client as client_sg = <$g1, $g2>.

That is, we only support the client sending two (distinct) groups. However, $g1 and $g2 are free to be any value, so any two client hello messages may have no overlapping groups.

As of TLS 1.3, servers are permitted to send the "supported_groups" extension to the client. If the server has a group it prefers to the ones in the "key_share" extension but is still willing to accept the ClientHello, it SHOULD send "supported_groups" to update the client's view of its preferences; this extension SHOULD contain all groups the server supports, regardless of whether they are currently supported by the client. Clients MUST NOT act upon any information found in "supported_groups" prior to successful completion of the handshake, but MAY use the information learned from a successfully completed handshake to change what groups they use in their "key_share" extension in subsequent connections.

We do not model this, nor do we model the client remembering which groups the server supports.

The "key_share" extension contains the endpoint's cryptographic parameters.

Clients MAY send an empty client_shares vector in order to request group selection from the server at the cost of an additional round trip. (see )

%%% Key Exchange Messages

   struct {
       NamedGroup group;
       opaque key_exchange<1..2^16-1>;
   } KeyShareEntry;

group

The named group for the key being exchanged. Finite Field Diffie-Hellman parameters are described in ; Elliptic Curve Diffie-Hellman parameters are described in .

key_exchange

Key exchange information. The contents of this field are determined by the specified group and its corresponding definition.

The "extension_data" field of this extension contains a "KeyShare" value:

%%% Key Exchange Messages

   struct {
       select (Handshake.msg_type) {
           case client_hello:
               KeyShareEntry client_shares<0..2^16-1>;

           case hello_retry_request:
               NamedGroup selected_group;

           case server_hello:
               KeyShareEntry server_share;
       };
   } KeyShare;

client_shares

A list of offered KeyShareEntry values in descending order of client preference. This vector MAY be empty if the client is requesting a HelloRetryRequest. Each KeyShareEntry value MUST correspond to a group offered in the "supported_groups" extension and MUST appear in the same order. However, the values MAY be a non-contiguous subset of the "supported_groups" extension and MAY omit the most preferred groups. Such a situation could arise if the most preferred groups are new and unlikely to be supported in enough places to make pregenerating key shares for them efficient.

selected_group

The mutually supported group the server intends to negotiate and is requesting a retried ClientHello/KeyShare for.

server_share

A single KeyShareEntry value that is in the same group as one of the client's shares.

Clients offer an arbitrary number of KeyShareEntry values, each representing a single set of key exchange parameters. For instance, a client might offer shares for several elliptic curves or multiple FFDHE groups. The key_exchange values for each KeyShareEntry MUST be generated independently. Clients MUST NOT offer multiple KeyShareEntry values for the same group. Clients MUST NOT offer any KeyShareEntry values for groups not listed in the client's "supported_groups" extension. Servers MAY check for violations of these rules and abort the handshake with an "illegal_parameter" alert if one is violated.

Upon receipt of this extension in a HelloRetryRequest, the client MUST verify that (1) the selected_group field corresponds to a group which was provided in the "supported_groups" extension in the original ClientHello; and (2) the selected_group field does not correspond to a group which was provided in the "key_share" extension in the original ClientHello. If either of these checks fails, then the client MUST abort the handshake with an "illegal_parameter" alert. Otherwise, when sending the new ClientHello, the client MUST replace the original "key_share" extension with one containing only a new KeyShareEntry for the group indicated in the selected_group field of the triggering HelloRetryRequest.

If using (EC)DHE key establishment, servers offer exactly one KeyShareEntry in the ServerHello. This value MUST be in the same group as the KeyShareEntry value offered by the client that the server has selected for the negotiated key exchange. Servers MUST NOT send a KeyShareEntry for any group not indicated in the "supported_groups" extension and MUST NOT send a KeyShareEntry when using the "psk_ke" PskKeyExchangeMode. If a HelloRetryRequest was received by the client, the client MUST verify that the selected NamedGroup in the ServerHello is the same as that in the HelloRetryRequest. If this check fails, the client MUST abort the handshake with an "illegal_parameter" alert.

---snip---

We reproduce the information in HelloRetryRequest to discuss the functionality of KeyShare:

       Client                        Server
    supports g1, g2               supports g

    <g1, g2>, <g1, g1^x> ---->  if g != g1

                        <----- HRR <g>

    checks g2 == g 
    <g1, g2>, <g2, g2^x2> ---->  checks g == g2

                        <------ <g, g^y>


                    Both parties compute
                          g^xy

We model DHE as taking place over some abstract group $g. The client initally supports a pair of groups <$g1, $g2>, and the server supports some group $g not necessarily equal to $g1 or $g2.

On the first flight, the client sends both supported groups, and the KeyShare extension:

define(<!KeyShareCH!>, <!Extension('40', g, gx)!>)

(locally we have g = $g1, $gx = $g1^~x).

If the server rejects this group and requests a retry, the client will simply set g = $g2 and generate a new value of ~x.

If the server requests a HRR, this contains the extension:

define(<!KeyShareHRR!>, <!Extension('40', new_g)!>)

where new_g is set locally to the server's group $g which is checked to be $g = $g2.

Finally, the server hello message contains the server's key share:

define(<!KeyShareSH!>, <!Extension('40', g, gy)!>)

where, again, g is set locally to $g and gy = $g^~y. If the server is sending a server hello message, we know the group must have been successfully negotiated with the client.

In order to use PSKs, clients MUST also send a "psk_key_exchange_modes" extension. The semantics of this extension are that the client only supports the use of PSKs with these modes, which restricts both the use of PSKs offered in this ClientHello and those which the server might supply via NewSessionTicket.

---snip---

%%% Key Exchange Messages

   enum { psk_ke(0), psk_dhe_ke(1), (255) } PskKeyExchangeMode;

   struct {
       PskKeyExchangeMode ke_modes<1..255>;
   } PskKeyExchangeModes;

---snip---

We model the client as always supporting both modes, allowing the server to choose between psk_ke and psk_dhe_ke. Therefore, this extension is simply

  define(<!PskKeyExchangeModes!>, <!Extension('45', psk_ke_mode)!>)

where ke_mode is set locally to <psk_ke, psk_dhe_ke> = <'0', '1'>.

When a PSK is used, the client can send application data in its first flight of messages. If the client opts to do so, it MUST supply an "early_data" extension as well as the "pre_shared_key" extension.

The "extension_data" field of this extension contains an "EarlyDataIndication" value:

%%% Key Exchange Messages

   struct {} Empty;

   struct {
       select (Handshake.msg_type) {
           case new_session_ticket:   uint32 max_early_data_size;
           case client_hello:         Empty;
           case encrypted_extensions: Empty;
       };
   } EarlyDataIndication;

See for the use of the max_early_data_size field.

The parameters for the 0-RTT data (symmetric cipher suite, ALPN protocol, etc.) are the same as those which were negotiated in the connection which established the PSK. The PSK used to encrypt the early data MUST be the first PSK listed in the client's "pre_shared_key" extension.

For PSKs provisioned via NewSessionTicket, a server MUST validate that the ticket age for the selected PSK identity (computed by subtracting ticket_age_add from PskIdentity.obfuscated_ticket_age modulo 2^32) is within a small tolerance of the time since the ticket was issued (see ). If it is not, the server SHOULD proceed with the handshake but reject 0-RTT, and SHOULD NOT take any other action that assumes that this ClientHello is fresh.

0-RTT messages sent in the first flight have the same (encrypted) content types as their corresponding messages sent in other flights (handshake and application_data) but are protected under different keys. After receiving the server's Finished message, if the server has accepted early data, an EndOfEarlyData message will be sent to indicate the key change. This message will be encrypted with the 0-RTT traffic keys.

In our model, when sending a ClientHello for a PSK handshake, we always allocate a space for the EarlyDataIndication extension. However, depending on whether we actually want to send the extension, we change the value locally:

  define(<!EarlyDataIndication!>, <!edi!>)
  define(<!early_data_indication!>, <!Extension('42', '0')!>)
  define(<!no_early_data_indication!>, <!'0'!>)

This allows us to pattern match on the server-side the client sending a hello with the extension present or not. For example, the client always sends this extension on the first PSK handshake attempt, but if the server sends a HRR in response to the initial message, the client never sends the extension on the second flight.

As noted in the PSK extension section, we use a pair of functions mask, unmask to capture the obfuscated ticket age mechanism, though it is not clear if this models anything interesting.

Currently, we do not model the EndOfEarlyData message.

A server which receives an "early_data" extension MUST behave in one of three ways:

• Ignore the extension and return a regular 1-RTT response. The server then ignores early data by attempting to decrypt received records in the handshake traffic keys until it is able to receive the client's second flight and complete an ordinary 1-RTT handshake, skipping records that fail to decrypt, up to the configured max_early_data_size.

• Request that the client send another ClientHello by responding with a HelloRetryRequest. A client MUST NOT include the "early_data" extension in its followup ClientHello. The server then ignores early data by skipping all records with external content type of "application_data" (indicating that they are encrypted).

• Return its own extension in EncryptedExtensions, indicating that it intends to process the early data. It is not possible for the server to accept only a subset of the early data messages. Even though the server sends a message accepting early data, the actual early data itself may already be in flight by the time the server generates this message.

---snip---

We model the three possibilities in the following way:

• The server can always ignore the extension if the recv_early_data rule is never actually used.

• We have the hello_retry_request_psk rule if the server wants to do a HRR. After this, the client will not send a early data indication, nor generate a EarlyDataSendStream.

• Accepting data happens by using the recv_early_data rule.

The "pre_shared_key" extension is used to indicate the identity of the pre-shared key to be used with a given handshake in association with PSK key establishment.

The "extension_data" field of this extension contains a "PreSharedKeyExtension" value:

%%% Key Exchange Messages

   struct {
       opaque identity<1..2^16-1>;
       uint32 obfuscated_ticket_age;
   } PskIdentity;

   opaque PskBinderEntry<32..255>;

   struct {
       select (Handshake.msg_type) {
           case client_hello:
               PskIdentity identities<7..2^16-1>;
               PskBinderEntry binders<33..2^16-1>;

           case server_hello:
               uint16 selected_identity;
       };

   } PreSharedKeyExtension; `---snip---`

Prior to accepting PSK key establishment, the server MUST validate the corresponding binder value (see below). If this value is not present or does not validate, the server MUST abort the handshake. Servers SHOULD NOT attempt to validate multiple binders; rather they SHOULD select a single PSK and validate solely the binder that corresponds to that PSK. In order to accept PSK key establishment, the server sends a "pre_shared_key" extension indicating the selected identity.

Clients MUST verify that the server's selected_identity is within the range supplied by the client, that the server selected a cipher suite indicating a Hash associated with the PSK and that a server "key_share" extension is present if required by the ClientHello "psk_key_exchange_modes". If these values are not consistent the client MUST abort the handshake with an "illegal_parameter" alert.

If the server supplies an "early_data" extension, the client MUST verify that the server's selected_identity is 0. If any other value is returned, the client MUST abort the handshake with an "illegal_parameter" alert.

This extension MUST be the last extension in the ClientHello (this facilitates implementation as described below). Servers MUST check that it is the last extension and otherwise fail the handshake with an "illegal_parameter" alert.

Ticket Age

The client's view of the age of a ticket is the time since the receipt of the NewSessionTicket message. Clients MUST NOT attempt to use tickets which have ages greater than the "ticket_lifetime" value which was provided with the ticket. The "obfuscated_ticket_age" field of each PskIdentity contains an obfuscated version of the ticket age formed by taking the age in milliseconds and adding the "ticket_age_add" value that was included with the ticket, see modulo 2^32. This addition prevents passive observers from correlating connections unless tickets are reused. Note that the "ticket_lifetime" field in the NewSessionTicket message is in seconds but the "obfuscated_ticket_age" is in milliseconds. Because ticket lifetimes are restricted to a week, 32 bits is enough to represent any plausible age, even in milliseconds.

We model a simplified version of the pre-shared key extension. Instead of offering a list of identities and binders, the client will only ever send a single one:

  define(<!PreSharedKeyExtensionCH!>, <!Extension('41', identities, <binder>)!>)
  define(<!PreSharedKeyExtensionSH!>, <!Extension('41', '0')!>)

The identities are supplied in the out_of_band_psk and new_session_ticket rules, and are simply fresh values ~psk_id generated at the time.

For obfuscated_ticket_age, we created a pair of functions mask such that unmask(mask(x, y), x) = y and similarly unmask(mask(x, y), y) = x. This effectively works like the XOR function and allows us to mask ticket ages.

Since an adversary can easily observe the time between two (hypothetically) connected session, we assume the ticket age is known: $ticket_age. Hence the obfuscated_ticket_age value is set to mask($ticket_age, ~ticket_age_add).

We do not currently attempt to model either correlation of sessions, or replay protection. Clearly if the client makes two resumed connections, the adversary can correlate sessions by observing mask($ticket_age.1, ~ticket_age_add) and mask($ticket_age.2, ~ticket_age_add). Moreover, we can assume that the server knows precisely the time elapsed, and therefore can verify that $ticket_age is correct, thereby preventing (to some measure) replay attacks.

However, to show that the adversary cannot correlate session otherwise might require using the indifferentiability framework in Tamarin which we do not currently use.

PSK Binder

The PSK binder value forms a binding between a PSK and the current handshake, as well as between the handshake in which the PSK was generated (if via a NewSessionTicket message) and the handshake where it was used. Each entry in the binders list is computed as an HMAC over a transcript hash (see ) containing a partial ClientHello up to and including the PreSharedKeyExtension.identities field. That is, it includes all of the ClientHello but not the binders list itself. The length fields for the message (including the overall length, the length of the extensions block, and the length of the "pre_shared_key" extension) are all set as if binders of the correct lengths were present.

The PskBinderEntry is computed in the same way as the Finished message () but with the BaseKey being the binder_key derived via the key schedule from the corresponding PSK which is being offered (see ).

If the handshake includes a HelloRetryRequest, the initial ClientHello and HelloRetryRequest are included in the transcript along with the new ClientHello. For instance, if the client sends ClientHello1, its binder will be computed over:

   Transcript-Hash(ClientHello1[truncated])

If the server responds with HelloRetryRequest, and the client then sends ClientHello2, its binder will be computed over:

   Transcript-Hash(ClientHello1,
                   HelloRetryRequest,
                   ClientHello2[truncated])

The full ClientHello1 is included in all other handshake hash computations. Note that in the first flight, ClientHello1[truncated] is hashed directly, but in the second flight, ClientHello1 is hashed and then reinjected as a "handshake_hash" message, as described in .

The binder values are computed over the entire ClientHello message using the following trick:

  binder = '0'
  // messages is expanded as the ClientHello message with binder set to '0'
  messages = ClientHello
  // The binder_key is computed over the messages, using the EarlySecret
  binder = binder_key()
  // messages is now recalculated using the most recent value for binder
  messages = ClientHello

(recall ClientHello is a macro which expands out to the message contents).

In the case of a HelloRetryRequest, a similar trick is used, but we need to store the previous messages in a temporary variable:

    messages = <messages, HelloRetryRequest>
    tmp_messages = messages
    binder = '0'
    messages = <messages, ClientHello>
    binder = binder_key()
    messages = <tmp_messages, ClientHello>

In all handshakes, the server MUST send the EncryptedExtensions message immediately after the ServerHello message. This is the first message that is encrypted under keys derived from the server_handshake_traffic_secret.

---snip---

Structure of this message:

%%% Server Parameters Messages

   struct {
       Extension extensions<0..2^16-1>;
   } EncryptedExtensions;

extensions

A list of extensions. For more information, see the table in .

We do not attempt to model any additional extensions, so the EncryptedExtensions message is simply:

define(<!EncryptedExtensions!>, <!handshake_record('8', $exts)!>)

As far as we are concerned, the extensions is just some blob of data which is protected under the handshake keys and included in the transcript.

A server which is authenticating with a certificate MAY optionally request a certificate from the client. This message, if sent, MUST follow EncryptedExtensions.

Structure of this message:

%%% Server Parameters Messages

   struct {
       opaque certificate_request_context<0..2^8-1>;
       Extension extensions<2..2^16-1>;
   } CertificateRequest;

certificate_request_context

An opaque string which identifies the certificate request and which will be echoed in the client's Certificate message. The certificate_request_context MUST be unique within the scope of this connection (thus preventing replay of client CertificateVerify messages). This field SHALL be zero length unless used for the post-handshake authentication exchanges described in . When requesting post-handshake authentication, the server SHOULD make the context unpredictable to the client (e.g., by randomly generating it) in order to prevent an attacker who has temporary access to the client's private key from pre-computing valid CertificateVerify messages.

extensions

A set of extensions describing the parameters of the certificate being requested. The "signature_algorithms" extension MUST be specified, and other extensions may optionally be included if defined for this message. Clients MUST ignore unrecognized extensions.

---snip---

The CertificateRequest message is optionally sent by the server, and only when not in PSK mode. This choice is covered by two rules: certificate_request and skip_certificate_request.

When certificate_request is used, the server sets the "bit" for auth_req to '1', which matches with the later rule recv_client_auth_cert reflecting that the server will expect a certificate. Similarly, skip_certificate_request leaves the bit as '0' and matches with the regular client_auth rule which just expects the client Finished message.

We define the CertificateRequest message as:

define(<!CertificateRequest!>, <! handshake_record('13',
  certificate_request_context,
  $certificate_extensions
)!>)

That is, the certificate_request_context is a free variable which is to be set locally. The extensions we simply leave as public variables and do not model any other certificate extension mechanism.

As stated in the specification, the certificate_request_context value is zero- length except for in post-handshake authentication. Therefore, we set this variable to '0' in both server and client rules (the latter reflecting that the client only continues if they receive a zero value).

As discussed in , TLS generally uses a common set of messages for authentication, key confirmation, and handshake integrity: Certificate, CertificateVerify, and Finished. (The PreSharedKey binders also perform key confirmation, in a similar fashion.) These three messages are always sent as the last messages in their handshake flight. The Certificate and CertificateVerify messages are only sent under certain circumstances, as defined below. The Finished message is always sent as part of the Authentication block. These messages are encrypted under keys derived from [sender]_handshake_traffic_secret.

The computations for the Authentication messages all uniformly take the following inputs:

• The certificate and signing key to be used.
• A Handshake Context consisting of the set of messages to be included in the transcript hash.
• A base key to be used to compute a MAC key. ---snip---

The rules in our model which use these messages are: server_auth, server_auth_psk, client_auth, client_auth_cert, client_auth_post (along with the corresponding recv_ rules).

We model certificates and the PKI with the Register_pk rule:

rule Register_pk:
  [ Fr(~ltkA) ]--[ GenLtk($A, ~ltkA), HonestUse(~ltkA)
  ]->
  [ !Ltk($A, ~ltkA), !Pk($A, pk(~ltkA)), Out(pk(~ltkA)) ]

This creates: a persistent (i.e. reusable) fact for the long term key (containing the signing key ~ltkA); a persistant fact for the long term key with the publick key pk(~ltkA) which can be used for verification; and finally outputs the public key to the adversary with an Out fact.

Note that the adversary is able to use the Reveal_Ltk rule to reveal the value of ~ltkA. This rule can be seen as either representing the adversary compromising the long-term key, or alternatively registering the fact that $A is a malicious server.

Signing is captured through the equations: verify{sign{message, ~ltkA}pk(~ltkA)} = True.

We assume that the authenticating party simply sends the public key pk(~ltkA) to their peer, and they are able to use the PKI to authenticate that this key belongs to $A by using the !Pk(...) fact.

For the Handshake Context, instead of a rolling hash we keep a transcript of all the messages, though we could easily compute the hash instead without any impact.

We compute the MAC key as specified later.

The server MUST send a Certificate message whenever the agreed-upon key exchange method uses certificates for authentication (this includes all key exchange methods defined in this document except PSK).

The client MUST send a Certificate message if and only if the server has requested client authentication via a CertificateRequest message (). If the server requests client authentication but no suitable certificate is available, the client MUST send a Certificate message containing no certificates (i.e., with the "certificate_list" field having length 0).

Structure of this message:

   struct {
       select(certificate_type){
           case RawPublicKey:
             // From RFC 7250 ASN.1_subjectPublicKeyInfo
             opaque ASN1_subjectPublicKeyInfo<1..2^24-1>;

           case X509:
             opaque cert_data<1..2^24-1>;
       };
       Extension extensions<0..2^16-1>;
   } CertificateEntry;

   struct {
       opaque certificate_request_context<0..2^8-1>;
       CertificateEntry certificate_list<0..2^24-1>;
   } Certificate;

certificate_request_context

If this message is in response to a CertificateRequest, the value of certificate_request_context in that message. Otherwise (in the case of server authentication), this field SHALL be zero length.

certificate_list ---snip---

extensions: ---snip---

OCSP Status and SCT Extensions

---snip---

Server Certificate Selection

---snip---

Client Certificate Selection

---snip---

As mentioned in the previous section, we simply model server/client certificates as a public key, which is authenticated by an abstract representation of the PKI.

Hence the Certificate message is defined as:

define(<!Certificate!>, <!handshake_record('11', certificate_request_context,
 certificate)!>)

Where certificate_request_context is set to '0' when it is not used (i.e. all cases other that post-handshake client auth), and certificate is set to pk(~ltkA). This is 'authenticated' using the fact !Pk($A, pk(~ltkA)) which models using the PKI to verify the public key belongs to $A.

In general, detailed certificate validation procedures are out of scope for TLS (see ). This section provides TLS-specific requirements.

If the server supplies an empty Certificate message, the client MUST abort the handshake with a "decode_error" alert.

If the client does not send any certificates, the server MAY at its discretion either continue the handshake without client authentication, or abort the handshake with a "certificate_required" alert. Also, if some aspect of the certificate chain was unacceptable (e.g., it was not signed by a known, trusted CA), the server MAY at its discretion either continue the handshake (considering the client unauthenticated) or abort the handshake.

---snip---

We do not currently model the scenario in which the client is unable to provide a certificate to authenticate.

This message is used to provide explicit proof that an endpoint possesses the private key corresponding to its certificate and also provides integrity for the handshake up to this point. Servers MUST send this message when authenticating via a certificate. Clients MUST send this message whenever authenticating via a certificate (i.e., when the Certificate message is non-empty). When sent, this message MUST appear immediately after the Certificate message and immediately prior to the Finished message.

Structure of this message:

%%% Authentication Messages

   struct {
       SignatureScheme algorithm;
       opaque signature<0..2^16-1>;
   } CertificateVerify;

The algorithm field specifies the signature algorithm used (see for the definition of this field). The signature is a digital signature using that algorithm. The content that is covered under the signature is the hash output as described in , namely:

   Transcript-Hash(Handshake Context, Certificate)

---snip---

We compute the (server) signature as:

messages = <messages, Certificate>
signature = compute_signature(~ltkS, server)

where compute_signature expands to:

sign{<'TLS13_server_CertificateVerify', h(messages)>}

Since messages contains the handshake transcript up until that point, this is valid for Handshake Context. We do not attempt to add the padding prefix specified in the specification since it would have no purpose given our assumption of perfect crypto.

The CertificateVerify message is simply defined as:

define(<!CertificateVerify!>, <!handshake_record('15', $sig_alg, signature)!>)

We do not currently model using different signing algorithms or their effects on security.

The peer validates the CertificateVerify message by recomputing the signature input, and enforcing the action Eq(verify(signature, sig_messages, pk(~ltkS)), true) which makes the trace invalid if the verification fails (implying the peer terminates the connection if receiving an invalid signature).

Note that an alternative way to model this in Tamarin would be to provide the peer with the long-term key ~ltkA and pattern match the signature as an expected message. While this can (probably) be shown to be equivalent and is potentially more efficient for Tamarin, we believe using explicit verification is clearer.

The Finished message is the final message in the authentication block. It is essential for providing authentication of the handshake and of the computed keys.

Recipients of Finished messages MUST verify that the contents are correct and if incorrect MUST terminate the connection with a "decrypt_error" alert.

Once a side has sent its Finished message and received and validated the Finished message from its peer, it may begin to send and receive application data over the connection. Early data may be sent prior to the receipt of the peer's Finished message, per .

The key used to compute the finished message is computed from the Base key defined in using HKDF (see ). Specifically:

finished_key =
    HKDF-Expand-Label(BaseKey, "finished", "", Hash.length)

Structure of this message:

%%% Authentication Messages

   struct {
       opaque verify_data[Hash.length];
   } Finished;

The verify_data value is computed as follows:

   verify_data =
       HMAC(finished_key,
            Transcript-Hash(Handshake Context,
                            Certificate*, CertificateVerify*))

   * Only included if present.

---snip---

The Finished message is modelled as:

define(<!Finished!>, <!handshake_record('20', verify_data)!>)

where verify_data is computed locally (for example in server_auth) by:

messages = <messages, Certificate>
...
messages = <messages, CertificateVerify>
fin_keys = keygen(handshake_traffic_secret(server), fin_key_label())
verify_data = compute_finished(fin_keys)

and messages is originally effectively Handshake Context.

Here we use the macros keygen, handshake_traffic_secret, fin_key_label and compute_finished to do the cryptographic processing.

These expand as:

fin_keys = HKDF_Expand_Label(BaseKey, finished, '0', '32')
compute_finished = hmac(fin_keys, h(messages))

where BaseKey is, in the example given the expansion of the server handshake traffic secret.

TLS also allows other messages to be sent after the main handshake. These messages use a handshake content type and are encrypted under the appropriate application traffic key.

At any time after the server has received the client Finished message, it MAY send a NewSessionTicket message. This message creates a pre-shared key (PSK) binding between the ticket value and the resumption master secret.

The client MAY use this PSK for future handshakes by including the ticket value in the "pre_shared_key" extension in its ClientHello (). Servers MAY send multiple tickets on a single connection, either immediately after each other or after specific events. For instance, the server might send a new ticket after post-handshake authentication in order to encapsulate the additional client authentication state. Clients SHOULD attempt to use each ticket no more than once, with more recent tickets being used first.

Any ticket MUST only be resumed with a cipher suite that has the same KDF hash algorithm as that used to establish the original connection, and only if the client provides the same SNI value as in the original connection, as described in Section 3 of .

Note: Although the resumption master secret depends on the client's second flight, servers which do not request client authentication MAY compute the remainder of the transcript independently and then send a NewSessionTicket immediately upon sending its Finished rather than waiting for the client Finished. This might be appropriate in cases where the client is expected to open multiple TLS connections in parallel and would benefit from the reduced overhead of a resumption handshake, for example.

%%% Ticket Establishment

   struct {
       uint32 ticket_lifetime;
       uint32 ticket_age_add;
       opaque ticket<1..2^16-1>;
       Extension extensions<0..2^16-2>;
   } NewSessionTicket;

ticket_lifetime

---snip---

ticket_age_add

A securely generated, random 32-bit value that is used to obscure the age of the ticket that the client includes in the "pre_shared_key" extension. The client-side ticket age is added to this value modulo 2^32 to obtain the value that is transmitted by the client. The server MUST generate a fresh value for each ticket it sends.

ticket

The value of the ticket to be used as the PSK identity. The ticket itself is an opaque label. It MAY either be a database lookup key or a self-encrypted and self-authenticated value. Section 4 of describes a recommended ticket construction mechanism.

extensions

A set of extension values for the ticket. The "Extension" format is defined in . Clients MUST ignore unrecognized extensions.

The sole extension currently defined for NewSessionTicket is "early_data", indicating that the ticket may be used to send 0-RTT data ()). It contains the following value:

max_early_data_size

The maximum amount of 0-RTT data that the client is allowed to send when using this ticket, in bytes. Only Application Data payload (i.e., plaintext but not padding or the inner content type byte) is counted. A server receiving more than max_early_data_size bytes of 0-RTT data SHOULD terminate the connection with an "unexpected_message" alert. Note that servers that reject early data due to lack of cryptographic material will be unable to differentiate padding from content, so clients SHOULD NOT depend on being able to send large quantities of padding in early data records.

Note that in principle it is possible to continue issuing new tickets which indefinitely extend the lifetime of the keying material originally derived from an initial non-PSK handshake (which was most likely tied to the peer's certificate). It is RECOMMENDED that implementations place limits on the total lifetime of such keying material; these limits should take into account the lifetime of the peer's certificate, the likelihood of intervening revocation, and the time since the peer's online CertificateVerify signature.

We have a new_session_ticket which models the server sending a NewSessionTicket message. The corresponding recv_ rule on the client side completes the exchange by receiving the message and generating the relevant values.

The NewSessionTicket message is defined as:

define(<!NewSessionTicket!>, <!handshake_record('4',
  $ticket_lifetime,
  ticket_age_add,
  ticket,
  TicketExtensions
)!>)

That is, we do not currently model the session ticket as having a particular lifetime, though we note that as usual if the server rejects a PSK then this is effectively covered by viewing a trace which terminates at recv_client_hello_psk or other.

ticket_age_add is a fresh value as used in PSK extension.

ticket is also a fresh value and is used by the client as the identity to resume a session. We do not currently model the server storing state by using ticket as an encrypted blob, however we would like to investigate this in future work, since it appears to be a common way of implementing PSKs.

For the extensions, we simply have:

define(<!TicketExtensions!>, <!<Extension('46', $max_early_data_size)>!>)

When the server/client sends/receives resp. the NewSessionTicket message, they also output a !Server/!ClientPSK fact which encapsulates the PSK state:

  !ServerPSK(S, C, res_psk, auth_status, NewSessionTicket, 'nst'),

This stores:

• server and client identities
• resumption master secret (res_psk)
• authentication status of the peer
• NewSessionTicket message blob, containing all other variables (ticket, ticket_age_add, etc.)
• type of session ticket ('nst' for NewSessionTicket, 'oob' for out of band PSK)

This fact is used in the client_hello_psk etc. rules to initialise the required variables.

We do not currently model anything to do with the cipher suites used, but this variable could also be used to ensure these are equal in the resumed session.

We believe there are some interesting scenarios which we can capture by modifying the above assumptions of what the server stores in the PSK state. For example:

• Server only stores limited information: e.g. just res_psk
• Server stores full set of information (usual case)
• Server encrypts state within ticket and avoid storing state

Furthermore, each of these scenarios have different implications for an adversary who is able to compromise the entire server state.

PSKs are currently modelled as persistanct facts; they live forever and can be reused as many time as desired.

When the client has sent the "post_handshake_auth" extension (see ), a server MAY request client authentication at any time after the handshake has completed by sending a CertificateRequest message. The client MUST respond with the appropriate Authentication messages (see ). If the client chooses to authenticate, it MUST send Certificate, CertificateVerify, and Finished. If it declines, it MUST send a Certificate message containing no certificates followed by Finished. All of the client's messages for a given response MUST appear consecutively on the wire with no intervening messages of other types.

A client that receives a CertificateRequest message without having sent the "post_handshake_auth" extension MUST send an "unexpected_message" fatal alert.

Note: Because client authentication could involve prompting the user, servers MUST be prepared for some delay, including receiving an arbitrary number of other messages between sending the CertificateRequest and receiving a response. In addition, clients which receive multiple CertificateRequests in close succession MAY respond to them in a different order than they were received (the certificate_request_context value allows the server to disambiguate the responses).

Here we have two main concerns to model:

1. Optional client auth
2. Multiple concurrent auth reqs/responses

We do not currently support the first. That is, the client will either never reply, or will send a certificate. We can look into supporting empty certificates in the future to model not authenticating.

We do, however, support the second option. Server certificate requests generate a new ServerCertReq fact which encapsulates the server storing additional state to track the certificate requests. This value is:

      ServerCertReq(tid, S, C, certificate_request_context),

which tracks the current session (tid), the identities of server and client, and the context value used to disambiguate the requests.

The client has equivalent facts for the same purpose.

%%% Updating Keys

   enum {
       update_not_requested(0), update_requested(1), (255)
   } KeyUpdateRequest;

   struct {
       KeyUpdateRequest request_update;
   } KeyUpdate;

request_update

Indicates whether the recipient of the KeyUpdate should respond with its own KeyUpdate. If an implementation receives any other value, it MUST terminate the connection with an "illegal_parameter" alert.

The KeyUpdate handshake message is used to indicate that the sender is updating its sending cryptographic keys. This message can be sent by either peer after it has sent a Finished message. Implementations that receive a KeyUpdate message prior to receiving a Finished message MUST terminate the connection with an "unexpected_message" alert. After sending a KeyUpdate message, the sender SHALL send all its traffic using the next generation of keys, computed as described in . Upon receiving a KeyUpdate, the receiver MUST update its receiving keys.

If the request_update field is set to "update_requested" then the receiver MUST send a KeyUpdate of its own with request_update set to "update_not_requested" prior to sending its next application data record. This mechanism allows either side to force an update to the entire connection, but causes an implementation which receives multiple KeyUpdates while it is silent to respond with a single update. Note that implementations may receive an arbitrary number of messages between sending a KeyUpdate with request_update set to update_requested and receiving the peer's KeyUpdate, because those messages may already be in flight. However, because send and receive keys are derived from independent traffic secrets, retaining the receive traffic secret does not threaten the forward secrecy of data sent before the sender changed keys.

If implementations independently send their own KeyUpdates with request_update set to "update_requested", and they cross in flight, then each side will also send a response, with the result that each side increments by two generations.

Both sender and receiver MUST encrypt their KeyUpdate messages with the old keys. Additionally, both sides MUST enforce that a KeyUpdate with the old key is received before accepting any messages encrypted with the new key. Failure to do so may allow message truncation attacks.

The way we view the KeyUpdate mechanism is as follows:

          Client                              Server

            senc{data1}kc1   ----->
                             <-----   senc{data2}ks1
            senc{data3}kc1   ----->

                              ...

KeyUpdate(update_requested)  ----->
kc2 = keygen(...)                                    kc2 = keygen(...)

            senc{data4}kc2   ----->      (not yet processed by Server)

                             <-----    KeyUpdate(update_not_requested)
ks2 = keygen(...)                                    ks2 = keygen(...)

                                                     (processes data4)
                             <-----   senc{data5}ks2

(And equivalently in the other direction)

When one actor requests a key update, the other party attempts to immediately respond with their own KeyUpdate message. However, clearly messages may arrive or be processed in a different order than they are sent.

We have a single rule update_recv_{client,server} which models receiving the initial KeyUpdate message, and immediately sending a new KeyUpdate message, updating both receiving and sendings keys. Technically, this means that the party cannot receive a message in between updating the receiving key and updating the sending key, however we argue (as shown above) that this is equivalent to the server not processing the received data until after they generate their new key.

While we could modify this, it would further increase the number of rules needed for modelling the post-handshake key update mechanism.

The messages themselves are very simply defined as:

define(<!KeyUpdate!>, <!handshake_record('24', update_requested)!>)
define(<!KeyUpdateReply!>, <!handshake_record('24', update_not_requested)!>)
define(<!update_not_requested!>, <!'0'!>)
define(<!update_requested!>, <!'1'!>)

To update the keys, the rules take in the old Send/RecvStream fact, and output a new one, with the updated keys. The KeyUpdate messages are encrypred with the old keys, as defined in the specification:

    [ ...
      SendStream(tid, S, C, prev_app_keys)
    ]
  --[ 
    ...
    ]->
    [ ...
      SendStream(tid, S, C, app_keys),
      Out(senc{KeyUpdate}prev_app_keys)
    ]

The TLS handshake establishes one or more input secrets which are combined to create the actual working keying material, as detailed below. The key derivation process incorporates both the input secrets and the handshake transcript. Note that because the handshake transcript includes the random values in the Hello messages, any given handshake will have different traffic secrets, even if the same input secrets are used, as is the case when the same PSK is used for multiple connections

The key derivation process makes use of the HKDF-Extract and HKDF-Expand functions as defined for HKDF , as well as the functions defined below:

    HKDF-Expand-Label(Secret, Label, HashValue, Length) =
         HKDF-Expand(Secret, HkdfLabel, Length)

    Where HkdfLabel is specified as:

    struct {
        uint16 length = Length;
        opaque label<7..255> = "tls13 " + Label;
        opaque hash_value<0..255> = HashValue;
    } HkdfLabel;

    Derive-Secret(Secret, Label, Messages) =
         HKDF-Expand-Label(Secret, Label,
                           Transcript-Hash(Messages), Hash.length)

The Hash function used by Transcript-Hash and HKDF is the cipher suite hash algorithm. Hash.length is its output length in bytes. Messages are the concatenation of the indicated handshake messages, including the handshake message type and length fields, but not including record layer headers. Note that in some cases a zero-length HashValue (indicated by "") is passed to HKDF-Expand-Label.

Note: with common hash functions, any label longer than 12 characters requires an additional iteration of the hash function to compute. The labels in this specification have all been chosen to fit within this limit.

Given a set of n InputSecrets, the final "master secret" is computed by iteratively invoking HKDF-Extract with InputSecret_1, InputSecret_2, etc. The initial secret is simply a string of Hash.length zero bytes. Concretely, for the present version of TLS 1.3, secrets are added in the following order:

• PSK (a pre-shared key established externally or a resumption_master_secret value from a previous connection)
• (EC)DHE shared secret ()

This produces a full key derivation schedule shown in the diagram below. In this diagram, the following formatting conventions apply:

• HKDF-Extract is drawn as taking the Salt argument from the top and the IKM argument from the left.
• Derive-Secret's Secret argument is indicated by the incoming arrow. For instance, the Early Secret is the Secret for generating the client_early_traffic_secret.

Though our assumption of perfect crypto makes many of these additional steps unnecessary, we attempt to stay as close to the design as possible.

  // Usage: HKDF_Expand_Label(Secret, Label, HashValue)
  define(<!HKDF_Expand_Label!>, <!Expand($1, HkdfLabel($2, $3, L), L)!>)
  define(<!HKDF_Expand_Label!>, <!Expand($1, HkdfLabel($2, $3, L), L)!>)
  define(<!HkdfLabel!>, <!<$3, 'TLS13_$1', $2>!> )

where Expand/3 is a perfect one-way function taking three inputs.

We leave the length variable L as implicit, and it is set to '32' everywhere.

Which leaves Derive-Secret to be defined as:

  dnl Usage: Derive_Secret(Secret, Label, HashValue)
  define(<!Derive_Secret!>, <!HKDF_Expand_Label($1, $2, <!$3!>)!>)

HashValue is defined to be h(messages), where messages is always defined locally.

                 0
                 |
                 v
   PSK ->  HKDF-Extract = Early Secret
                 |
                 +-----> Derive-Secret(.,
                 |                     "ext binder" |
                 |                     "res binder",
                 |                     "")
                 |                     = binder_key
                 |
                 +-----> Derive-Secret(., "c e traffic",
                 |                     ClientHello)
                 |                     = client_early_traffic_secret
                 |
                 +-----> Derive-Secret(., "e exp master",
                 |                     ClientHello)
                 |                     = early_exporter_master_secret
                 v
           Derive-Secret(., "derived", "")
                 |
                 v
(EC)DHE -> HKDF-Extract = Handshake Secret
                 |
                 +-----> Derive-Secret(., "c hs traffic",
                 |                     ClientHello...ServerHello)
                 |                     = client_handshake_traffic_secret
                 |
                 +-----> Derive-Secret(., "s hs traffic",
                 |                     ClientHello...ServerHello)
                 |                     = server_handshake_traffic_secret
                 v
           Derive-Secret(., "derived", "")
                 |
                 v
      0 -> HKDF-Extract = Master Secret
                 |
                 +-----> Derive-Secret(., "c ap traffic",
                 |                     ClientHello...server Finished)
                 |                     = client_application_traffic_secret_0
                 |
                 +-----> Derive-Secret(., "s ap traffic",
                 |                     ClientHello...server Finished)
                 |                     = server_application_traffic_secret_0
                 |
                 +-----> Derive-Secret(., "exp master",
                 |                     ClientHello...server Finished)
                 |                     = exporter_master_secret
                 |
                 +-----> Derive-Secret(., "res master",
                                       ClientHello...client Finished)
                                       = resumption_master_secret

---snip---

Following the key schedule diagram, we obtain:

                '0'
                 |
                 v
   res_psk ->  Extract(res_psk, '0') = EarlySecret ( = es )
                 |
                 +-----> Derive_Secret(es,
                 |                     "extbinder" |
                 |                     "resbinder",
                 |                     '0')
                 |                     = binder_key
                 |
                 +-----> Derive_Secret(es, "clientearlytrafficsecret",
                 |                     h(messages))
                 |                     = early_traffic_secret
                 |
                 +-----> Derive_Secret(es, "earlyexportermastersecret",
                 |                     h(messages))
                 |                     = early_exporter_secret (NOT USED)
                 v
gxy -> Extract(gxy, es) = HandshakeSecret ( = hs )
                 |
                 +-----> Derive-Secret(hs, "c hs traffic",
                 |                     h(messages))
                 |                     = client_handshake_traffic_secret
                 |
                 +-----> Derive-Secret(hs, "s hs traffic",
                 |                     h(messages))
                 |                     = server_handshake_traffic_secret
                 |
                 v
      '0' -> Extract('0', hs) = MasterSecret ( = ms )
                 |
                 +-----> Derive-Secret(ms, "c ap traffic",
                 |                     ClientHello...server Finished)
                 |                     = client_application_traffic_secret_0
                 |
                 +-----> Derive-Secret(ms, "s ap traffic",
                 |                     ClientHello...server Finished)
                 |                     = server_application_traffic_secret_0
                 |
                 +-----> Derive-Secret(ms, "exp master",
                 |                     ClientHello...server Finished)
                 |                     = exporter_master_secret
                 |
                 +-----> Derive-Secret(ms, "res master",
                                       ClientHello...client Finished)
                                       = resumption_master_secret

Hence care must be taken that messages is defined to be the correct sequence of messages.

early_traffic_secret is generated in {recv_}client_hello_psk and contains ClientHello.

*_handshake_traffic_secret is generated in {client,server}_gen_keys and contains ClientHello...ServerHello.

{client,server}_traffic_secret_0 is generated in {recv_}server_auth and contains ClientHello...ServerFinished

resumption_secret is generated in {recv_}client_auth{_cert} and contains ClientHello...ClientFinished.

Therefore messages is always defined as expected.

Once the handshake is complete, it is possible for either side to update its sending traffic keys using the KeyUpdate handshake message defined in . The next generation of traffic keys is computed by generating client_/server_application_traffic_secret_N+1 from client_/server_application_traffic_secret_N as described in this section then re-deriving the traffic keys as described in .

The next-generation application_traffic_secret is computed as:

    application_traffic_secret_N+1 =
        HKDF-Expand-Label(application_traffic_secret_N,
                          "traffic upd", "", Hash.length)

Once client/server_application_traffic_secret_N+1 and its associated traffic keys have been computed, implementations SHOULD delete client_/server_application_traffic_secret_N and its associated traffic keys.

We generate the new traffic secret as:

    cats = keygen(prev_cats, app_secret_label())
    sats = keygen(prev_sats, app_secret_label())

where keygen expands as: HKDF_Expand_Label($1, $2, '0'). I.e. is the usual exand macro with a zero-length hash value used and the label is applicationtrafficsecret.

The traffic keying material is generated from the following input values:

• A secret value
• A purpose value indicating the specific value being generated
• The length of the key

The traffic keying material is generated from an input traffic secret value using:

    [sender]_write_key = HKDF-Expand-Label(Secret, "key", "", key_length)
    [sender]_write_iv = HKDF-Expand-Label(Secret, "iv", "", iv_length)

[sender] denotes the sending side. The Secret value for each record type is shown in the table below.

All the traffic keying material is recomputed whenever the underlying Secret changes (e.g., when changing from the handshake to application data keys or upon a key update).

Due to our use of perfect crypto, we do not bother with generating IVs.

However, we generate keys as above using the keygen macro. For example, for the client keys we get:

// early application traffic keys
ead_keyc = keygen(early_traffic_secret(client), early_app_key_label())
// handshake keys
hs_keyc = keygen(handshake_traffic_secret(client), hs_key_label())
// application traffic keys
app_keys = keygen(sats, app_key_label())

A conventional Diffie-Hellman computation is performed. The negotiated key (Z) is converted to byte string by encoding in big-endian, padded with zeros up to the size of the prime. This byte string is used as the shared secret, and is used in the key schedule as specified above.

---snip---

None of this applies to our abstract model. We can simply use the raw value gxy = $g^(~x*~y).

defines keying material exporters for TLS in terms of the TLS PRF. This document replaces the PRF with HKDF, thus requiring a new construction. The exporter interface remains the same. If context is provided, the value is computed as:

HKDF-Expand-Label(Secret, label, Hash(context_value), key_length)

Where Secret is either the early_exporter_secret or the exporter_secret. Implementations MUST use the exporter_secret unless explicitly specified by the application. When adding TLS 1.3 to TLS 1.2 stacks, the exporter_secret MUST be for the existing exporter interface.

If no context is provided, the value is computed as above but with a zero-length context_value. Note that providing no context computes the same value as providing an empty context. As of this document's publication, no allocated exporter label is used with both modes. Future specifications MUST NOT provide an empty context and no context with the same label and SHOULD provide a context, possibly empty, in all exporter computations.

We do not currently make use of exporters, nor try to prove any properties. One can easily draw conclusions from our lemmas which prove secrecy properties of the base secret (e.g. MasterSecret) and the transcript agreement lemmas.