// This module provides an specification of the TLS 1.2 handshake message
// state machine according to RFCs 5246, 5077 and 6066 (OCSP extension only).
// The NPN extension is based on the draft
// https://datatracker.ietf.org/doc/html/draft-agl-tls-nextprotoneg-03


module rfc_handshake_tls12 where

import s2n_handshake_io

// Main correctness property: a simulation of the S2N handshake state
// machine by an RFC-derived state machine. Every pair of related initial
// 'connection' and 'Parameters' generates the same sequence of messages.
tls12rfcSimulatesS2N : {len} (fin len) => connection -> Parameters -> Bool
tls12rfcSimulatesS2N conn pars =
   initial_connection conn /\ connectionParameters conn pars ==>
   map rfc2S2N (traceRFC `{n = len} pars) == traceS2N `{n = len} conn

// Generate a sequence of states for the the RFC handshake state machine given
// handshake parameters
traceRFC : {n} (fin n) => Parameters -> [n]Message
traceRFC params = take (map message (iterate (handshakeTransition params) clientHelloSent))

// RFC Handshake states
type State = [5]

// Handshake states
(helloRequestSent : State) = 0
(clientHelloSent : State) = 1
(serverHelloSent : State) = 2
(serverCertificateSent : State) = 3
(serverKeyExchangeSent : State) = 4
(certificateRequestSent : State) = 5
(serverHelloDoneSent : State) = 6
(serverHelloDoneSentCertRequested : State) = 7
(clientCertificateSent : State) = 8
(clientKeyExchangeSent : State) = 9
(clientKeyExchangeSentCertSent : State) = 10
(certificateVerifySent : State) = 11
(clientChangeCipherSpecSent : State) = 12
(clientFinishedSent : State) = 13
(serverChangeCipherSpecSent : State) = 14
(serverFinishedSent : State) = 15
(applicationDataTransmission : State) = 16
(serverNewSessionTicketSent : State) = 17
(serverRenewSessionTicketSent : State) = 18
(serverChangeCipherSpecWithTicketSent : State) = 19
(serverFinishedWithTicketSent : State) = 20
(clientChangeCipherSpecWithTicketSent : State) = 21
(clientFinishedWithTicketSent : State) = 22
(serverCertificateStatusSent : State) = 23
(nextProtocolSent : State) = 24
(nextProtocolWithTicketSent : State) = 25

// TLS protocol types
type Protocol = [2]
(handshake : Protocol) = 0
(changeCipherSpec : Protocol) = 1
(alert : Protocol) = 2
(data : Protocol) = 3

// TLS Message types
type MessageType = [4]
//handshake message types
(helloRequest       : MessageType) = 0
(clientHello        : MessageType) = 1
(serverHello        : MessageType) = 2
(certificate        : MessageType) = 3
(serverKeyExchange  : MessageType) = 4
(certificateRequest : MessageType) = 5
(serverHelloDone    : MessageType) = 6
(certificateVerify  : MessageType) = 7
(clientKeyExchange  : MessageType) = 8
(finished           : MessageType) = 9
(newSessionTicket   : MessageType) = 10
(certificateStatus  : MessageType) = 11
(nextProtocol       : MessageType) = 12

// ChangeCipherSpec message types
(changeCipherSpecMessage : MessageType) = 0

// Data message types
(applicationData : MessageType) = 0
(error : MessageType) = 1

// Sender (data flow direction)
type Sender = [2]
(server   : Sender) = 0
(client   : Sender) = 1
(both     : Sender) = 2
(noSender : Sender) = 3

// Key exchange algorithms
type KeyExchange = [3]
(DH_anon : KeyExchange) = 0
(DHE_DSS : KeyExchange) = 1
(DHE_RSA : KeyExchange) = 2
(RSA     : KeyExchange) = 3
(DH_DSS  : KeyExchange) = 4
(DH_RSA  : KeyExchange) = 5

// TLS protocol parameters that determine the transition to take in each state.
// Some of these fields are set as a configuration to the end-point, while others
// are determined from the messages send by the counterparty. We model both as
// parameters since the state machine model reasons about both end-points.
type Parameters = {keyExchange : KeyExchange
                   //^ Negotiated key exchange algorithm
                  ,sessionTicket : Bit
                   //^ The client had a session ticket
                  ,renewSessionTicket : Bit
                   //^ Whether the server decides to renew a session ticket
                  ,sendCertificateStatus : Bit
                   //^ Whether the server decides to send the certificate status
                   //  message
                  ,requestClientCert : Bit
                   //^ Whether the server requests a certificate from the client
                  ,includeSessionTicket : Bit
                   //^ Whether the server includes a session ticket extension in
                   //  SERVER_HELLO
                  ,npnNegotiated : Bit
                   //^ Whether the client sends a ``NextProtocol'' message.
                   // This allows the application layer to negotiate which
                   // protocol should be performed over the secure connection.
                  }

// A relation between the s2n_connection struct and the parameters
connectionParameters : connection -> Parameters -> Bit
connectionParameters conn params =
    conn.server_can_send_ocsp == params.sendCertificateStatus
 /\ ((conn.key_exchange_eph /\ ~keyExchangeNonEphemeral params /\ params.keyExchange != DH_anon) \/
     (~conn.key_exchange_eph /\ keyExchangeNonEphemeral params))
 /\ (conn.is_caching_enabled /\ ~conn.resume_from_cache) == params.sessionTicket
 /\ (~params.includeSessionTicket) // s2n server does not issue tickets at this time
 /\ (~params.renewSessionTicket) // s2n server does not issue tickets at this time
 /\ conn.client_auth_flag == params.requestClientCert
 /\ conn.npn_negotiated == params.npnNegotiated
 /\ conn.actual_protocol_version != S2N_TLS13

// A predicate that tells whether key-exchange is non-ephemeral and uses server certificate
// data for exchanging a premaster secret (RFC 5246 7.4.3). In this case the key exchange
// algorithm does not require KeyExchange messages.
keyExchangeNonEphemeral : Parameters -> Bit
keyExchangeNonEphemeral params = params.keyExchange == RSA \/ params.keyExchange == DH_DSS \/ params.keyExchange == DH_RSA

// Handshake state transition relation per the RFCs. Given handshake parameters
// and a handshake state, return the next state. If there is no valid next state,
// the state machine stutters (returns the previous state).
handshakeTransition : Parameters -> State -> State
handshakeTransition params old =
  snd (find fst (True, old) [ (old == from /\ p, to) | (from, p, to) <- valid_transitions])
  where // The encoding of the transition relation of the state machine is a triple
        // (oldState, transitionCondition, newState) with the meaning "if we are
        // in the oldState, the transitionCondition is True (for the given
        // Parameters) then the next state is newState.
        valid_transitions =
          [(helloRequestSent, True, clientHelloSent)
          
          ,(clientHelloSent,  True, serverHelloSent)
          
          ,(serverHelloSent, params.keyExchange != DH_anon /\ ~params.sessionTicket, serverCertificateSent)
          ,(serverHelloSent, params.keyExchange == DH_anon /\ ~params.sessionTicket, serverKeyExchangeSent)
          ,(serverHelloSent, params.sessionTicket /\ params.renewSessionTicket,  serverNewSessionTicketSent)
          ,(serverHelloSent, params.sessionTicket /\ ~params.renewSessionTicket, serverChangeCipherSpecWithTicketSent)

          ,(serverCertificateSent, keyExchangeNonEphemeral params /\ ~params.requestClientCert /\ ~params.sendCertificateStatus, serverHelloDoneSent)
          ,(serverCertificateSent, keyExchangeNonEphemeral params /\ params.requestClientCert /\ ~params.sendCertificateStatus, certificateRequestSent)
          ,(serverCertificateSent, ~(keyExchangeNonEphemeral params) /\ ~params.sendCertificateStatus, serverKeyExchangeSent)
          ,(serverCertificateSent, params.sendCertificateStatus,  serverCertificateStatusSent)

          ,(serverKeyExchangeSent, ~params.requestClientCert, serverHelloDoneSent)
          ,(serverKeyExchangeSent, params.requestClientCert, certificateRequestSent)

          ,(certificateRequestSent, True, serverHelloDoneSentCertRequested)

          ,(serverHelloDoneSent, True, clientKeyExchangeSent)

          ,(clientKeyExchangeSent, True, clientChangeCipherSpecSent)

          ,(serverHelloDoneSentCertRequested, True, clientCertificateSent)

          ,(clientCertificateSent, True, clientKeyExchangeSentCertSent)

          ,(clientKeyExchangeSentCertSent, True, certificateVerifySent)

          ,(certificateVerifySent, True, clientChangeCipherSpecSent)

          ,(clientChangeCipherSpecSent, ~params.npnNegotiated, clientFinishedSent)
          ,(clientChangeCipherSpecSent, params.npnNegotiated, nextProtocolSent)

          ,(nextProtocolSent, True, clientFinishedSent)

          ,(clientFinishedSent, ~params.includeSessionTicket, serverChangeCipherSpecSent)
          ,(clientFinishedSent, params.includeSessionTicket, serverNewSessionTicketSent)
          
          ,(serverNewSessionTicketSent, True, serverChangeCipherSpecSent)
          
          ,(serverChangeCipherSpecSent, True, serverFinishedSent)
          
          ,(serverFinishedSent, True, applicationDataTransmission)
          
          ,(serverChangeCipherSpecWithTicketSent, True, serverFinishedWithTicketSent)
          
          ,(serverFinishedWithTicketSent, True, clientChangeCipherSpecWithTicketSent)
          
          ,(clientChangeCipherSpecWithTicketSent, ~params.npnNegotiated, clientFinishedWithTicketSent)
          ,(clientChangeCipherSpecWithTicketSent, params.npnNegotiated, nextProtocolWithTicketSent)
          ,(nextProtocolWithTicketSent, True, clientFinishedWithTicketSent)
          
          ,(clientFinishedWithTicketSent, True, applicationDataTransmission)

          ,(serverCertificateStatusSent, keyExchangeNonEphemeral params /\ ~params.requestClientCert, serverHelloDoneSent)
          ,(serverCertificateStatusSent, keyExchangeNonEphemeral params /\ params.requestClientCert, certificateRequestSent)
          ,(serverCertificateStatusSent, ~(keyExchangeNonEphemeral params), serverKeyExchangeSent)
          ]

// Abstraction of the TLS message which records the protocol, message type and
// direction
type Message = {messageType : MessageType
               ,protocol : Protocol
               ,sender : Sender
               }

mkMessage : Sender -> Protocol -> MessageType -> Message
mkMessage s p mt = {sender = s, protocol = p, messageType = mt}

// Message sent in each handshake state
message : State -> Message
message = lookupDefault messages (mkMessage noSender data error)
    where messages =
            [(helloRequestSent, mkMessage server handshake helloRequest)
            ,(clientHelloSent, mkMessage client handshake clientHello)
            ,(serverHelloSent, mkMessage server handshake serverHello)
            ,(serverCertificateSent, mkMessage server handshake certificate)
            ,(serverKeyExchangeSent, mkMessage server handshake serverKeyExchange)
            ,(certificateRequestSent, mkMessage server handshake certificateRequest)
            ,(serverHelloDoneSent, mkMessage server handshake serverHelloDone)
            ,(serverHelloDoneSentCertRequested, mkMessage server handshake serverHelloDone)
            ,(clientCertificateSent, mkMessage client handshake certificate)
            ,(clientKeyExchangeSent, mkMessage client handshake clientKeyExchange)
            ,(clientKeyExchangeSentCertSent, mkMessage client handshake clientKeyExchange)
            ,(certificateVerifySent, mkMessage client handshake certificateVerify)
            ,(clientChangeCipherSpecSent, mkMessage client changeCipherSpec changeCipherSpecMessage)
            ,(clientFinishedSent, mkMessage client handshake finished)
            ,(serverChangeCipherSpecSent, mkMessage server changeCipherSpec changeCipherSpecMessage)
            ,(serverFinishedSent, mkMessage server handshake finished)
            ,(applicationDataTransmission, mkMessage both data applicationData)
            ,(serverNewSessionTicketSent, mkMessage server handshake newSessionTicket)
            ,(serverChangeCipherSpecWithTicketSent, mkMessage server changeCipherSpec changeCipherSpecMessage)
            ,(serverFinishedWithTicketSent, mkMessage server handshake finished)
            ,(clientChangeCipherSpecWithTicketSent, mkMessage client changeCipherSpec changeCipherSpecMessage)
            ,(clientFinishedWithTicketSent, mkMessage client handshake finished)
            ,(serverCertificateStatusSent, mkMessage server handshake certificateStatus)
            ,(nextProtocolSent, mkMessage client handshake nextProtocol)
            ,(nextProtocolWithTicketSent, mkMessage client handshake nextProtocol)
            ]

// a mapping from RFC messages to s2n handshake_action's
rfc2S2N : Message -> handshake_action
rfc2S2N msg = {writer = sender2writer msg.sender
              ,record_type = protocol2recordType msg.protocol
              ,message_type = s2nMessageType msg
              }

// an equality relation between RFC and s2n messages
msgRFCS2N : Message -> handshake_action -> Bool
msgRFCS2N msg hsa = rfc2S2N msg == hsa

// convert a specification representation of sender to a 'writer' character in s2n.
sender2writer : Sender -> [8]
sender2writer sndr = if sndr == server then 'S'
                else if sndr == client then 'C'
                else if sndr == both   then 'B'
                else                        'E'

// Convert the RFC protocol number to s2n TLS record type constant
protocol2recordType : Protocol -> [8]
protocol2recordType = lookupDefault protocols TLS_APPLICATION_DATA
   where protocols = [(handshake, TLS_HANDSHAKE)
                     ,(changeCipherSpec, TLS_CHANGE_CIPHER_SPEC)
                     ,(alert, TLS_ALERT)
                     ,(data, TLS_APPLICATION_DATA)
                     ]

// Returns the s2n message type for a given RFC Message
s2nMessageType : Message -> [8]
s2nMessageType msg =
  if prot == handshake then (if mt == helloRequest then TLS_HELLO_REQUEST
                       else if mt == clientHello  then TLS_CLIENT_HELLO
                       else if mt == serverHello  then TLS_SERVER_HELLO
                       else if mt == certificate  then TLS_CERTIFICATE
                       else if mt == serverKeyExchange then TLS_SERVER_KEY
                       else if mt == certificateRequest then TLS_CERTIFICATE_REQ
                       else if mt == serverHelloDone then TLS_SERVER_HELLO_DONE
                       else if mt == certificateVerify then TLS_CERT_VERIFY
                       else if mt == clientKeyExchange then TLS_CLIENT_KEY
                       else if mt == finished then TLS_FINISHED
                       else if mt == newSessionTicket then TLS_SERVER_NEW_SESSION_TICKET
                       else if mt == certificateStatus then TLS_CERTIFICATE_STATUS
                       else if mt == nextProtocol then TLS_NPN
                       else ERROR_MESSAGE)

  else 0
     where mt = msg.messageType
           send = msg.sender
           prot = msg.protocol

ERROR_MESSAGE = 10 // unused in current s2n