Idris2Doc : Network.TLS.Core

Network.TLS.Core

(source)
Definitions
tls13_supported_cipher_suites : List1 CipherSuite
  All the implemented TLS 1.3 cipher suites

  Visibility: public export
tls12_supported_cipher_suites : List1 CipherSuite
  All the implemented TLS 1.2 cipher suites

  Visibility: public export
supported_groups : List1 SupportedGroup
  All the implemented groups for key exchange

  Visibility: public export
supported_signature_algorithms : List1 SignatureAlgorithm
  All the implemented signature algorithms for handshake verification

  Visibility: public export
sig_alg_get_params : SignatureAlgorithm -> SignatureParameter
  Visibility: export
get_server_version : ServerHello -> TLSVersion
  Get the server's TLS version from the ServerHello record
  Since TLS 1.3 records are masqueraded as TLS 1.2 records
  Using (.version) directly may not yield the current result
  This function checks for the SupportedVersions extension
  If there is one, the version specified in the extension will
  be used, otherwise, returns the specified version in the main body

  Visibility: public export
get_server_handshake_key : ServerHello -> Either String (SupportedGroup, List Bits8)
  Get the server's handshake public key for key exchange

  Visibility: public export
CertificateCheck : (Type -> Type) -> Type
  A type alias for a function that will be used to verify handshake
  It takes a Certificate record extension, containing all the certificates
  as raw bytes, along with the certificate extensions fields, and returns a
  public key that will be used to verify the current handshake hash digest

  Visibility: public export
record TLSInitialState : Type
  The initial TLS state, before any communication with the server is made

  Totality: total
  Visibility: public export
  Constructor: 
MkTLSInitialState : String -> Vect 32 Bits8 -> List Bits8 -> List1 CipherSuite -> List1 SignatureAlgorithm -> List1 (g : SupportedGroup ** (curve_group_to_scalar_type g, curve_group_to_element_type g)) -> TLSInitialState

  Projections:
  
.cipher_suites : TLSInitialState -> List1 CipherSuite
  
.client_random : TLSInitialState -> Vect 32 Bits8
  
.dh_keys : TLSInitialState -> List1 (g : SupportedGroup ** (curve_group_to_scalar_type g, curve_group_to_element_type g))
  
.server_hostname : TLSInitialState -> String
  
.session_id : TLSInitialState -> List Bits8
  
.signature_algos : TLSInitialState -> List1 SignatureAlgorithm
.server_hostname : TLSInitialState -> String
  Visibility: public export
server_hostname : TLSInitialState -> String
  Visibility: public export
.client_random : TLSInitialState -> Vect 32 Bits8
  Visibility: public export
client_random : TLSInitialState -> Vect 32 Bits8
  Visibility: public export
.session_id : TLSInitialState -> List Bits8
  Visibility: public export
session_id : TLSInitialState -> List Bits8
  Visibility: public export
.cipher_suites : TLSInitialState -> List1 CipherSuite
  Visibility: public export
cipher_suites : TLSInitialState -> List1 CipherSuite
  Visibility: public export
.signature_algos : TLSInitialState -> List1 SignatureAlgorithm
  Visibility: public export
signature_algos : TLSInitialState -> List1 SignatureAlgorithm
  Visibility: public export
.dh_keys : TLSInitialState -> List1 (g : SupportedGroup ** (curve_group_to_scalar_type g, curve_group_to_element_type g))
  Visibility: public export
dh_keys : TLSInitialState -> List1 (g : SupportedGroup ** (curve_group_to_scalar_type g, curve_group_to_element_type g))
  Visibility: public export
record TLSClientHelloState : Type
  The TLS state after sending client hello to the server

  Totality: total
  Visibility: export
  Constructor: 
MkTLSClientHelloState : List Bits8 -> Vect 32 Bits8 -> List1 (g : SupportedGroup ** (curve_group_to_scalar_type g, curve_group_to_element_type g)) -> TLSClientHelloState

  Projections:
  
.b_client_hello : TLSClientHelloState -> List Bits8
  
.client_random : TLSClientHelloState -> Vect 32 Bits8
  
.dh_keys : TLSClientHelloState -> List1 (g : SupportedGroup ** (curve_group_to_scalar_type g, curve_group_to_element_type g))
data TLS3ServerHelloVerificationState : Type
  ADT to represent the state of certificate verification in TLS 1.3 handshake

  Totality: total
  Visibility: export
  Constructors:
  
NotVerified : TLS3ServerHelloVerificationState
  
HasCertificate : Certificate -> TLS3ServerHelloVerificationState
  
Verified : TLS3ServerHelloVerificationState
data TLS3ServerHelloState : (aead : Type) -> AEAD aead -> (algo : Type) -> Hash algo -> Type
  The TLS state after receiving server hello from a TLS 1.3 server

  Totality: total
  Visibility: export
  Constructor: 
MkTLS3ServerHelloState : TLS3ServerHelloVerificationState -> (a' : AEAD a) -> (h' : Hash h) -> h -> HandshakeKeys fixed_iv_length enc_key_length -> Nat -> TLS3ServerHelloState a a' h h'
data TLS3ApplicationState : (aead : Type) -> AEAD aead -> Type
  The TLS state when communication over TLS 1.3 is ready

  Totality: total
  Visibility: export
  Constructor: 
MkTLS3ApplicationState : (a' : AEAD a) -> ApplicationKeys fixed_iv_length enc_key_length -> Nat -> Nat -> TLS3ApplicationState a a'
record TLS2ServerHelloState : Type -> Type
  The TLS state after receiving server hello from a TLS 1.2 server

  Totality: total
  Visibility: export
  Constructor: 
MkTLS2ServerHelloState : Vect 32 Bits8 -> Vect 32 Bits8 -> CipherSuite -> List1 (g : SupportedGroup ** (curve_group_to_scalar_type g, curve_group_to_element_type g)) -> Hash algo -> algo -> TLS2ServerHelloState algo

  Projections:
  
.cipher_suite : TLS2ServerHelloState algo -> CipherSuite
  
.client_random : TLS2ServerHelloState algo -> Vect 32 Bits8
  
.dh_keys : TLS2ServerHelloState algo -> List1 (g : SupportedGroup ** (curve_group_to_scalar_type g, curve_group_to_element_type g))
  
.digest_state : TLS2ServerHelloState algo -> algo
  
.digest_wit : TLS2ServerHelloState algo -> Hash algo
  
.server_random : TLS2ServerHelloState algo -> Vect 32 Bits8
record TLS2ServerCertificateState : Type -> Type
  The TLS state after receiving server certificate from a TLS 1.2 server

  Totality: total
  Visibility: export
  Constructor: 
MkTLS2ServerCertificateState : TLS2ServerHelloState algo -> Certificate -> CipherSuite -> List1 (g : SupportedGroup ** (curve_group_to_scalar_type g, curve_group_to_element_type g)) -> Hash algo -> algo -> TLS2ServerCertificateState algo

  Projections:
  
.certificate : TLS2ServerCertificateState algo -> Certificate
  
.cipher_suite : TLS2ServerCertificateState algo -> CipherSuite
  
.dh_keys : TLS2ServerCertificateState algo -> List1 (g : SupportedGroup ** (curve_group_to_scalar_type g, curve_group_to_element_type g))
  
.digest_state : TLS2ServerCertificateState algo -> algo
  
.digest_wit : TLS2ServerCertificateState algo -> Hash algo
  
.server_hello : TLS2ServerCertificateState algo -> TLS2ServerHelloState algo
data TLS2ServerKEXState : (aead : Type) -> AEAD aead -> (algo : Type) -> Hash algo -> Type
  The TLS state after receiving server key exchange from a TLS 1.2 server

  Totality: total
  Visibility: export
  Constructor: 
MkTLS2ServerKEXState : (a' : AEAD a) -> (h' : Hash h) -> h -> Nat -> List Bits8 -> Application2Keys fixed_iv_length enc_key_length mac_key_length -> TLS2ServerKEXState a a' h h'
record TLS2ServerKEXDoneState : (a : Type) -> AEAD a -> (c : Type) -> Hash c -> Type
  The TLS state after receiving server key exchange done from a TLS 1.2 server

  Totality: total
  Visibility: export
  Constructor: 
MkTLS2ServerKEXDoneState : TLS2ServerKEXState a b c d -> TLS2ServerKEXDoneState a b c d

  Projection: 
.kex_state : TLS2ServerKEXDoneState a b c d -> TLS2ServerKEXState a b c d
record TLS2AppReadyState : (a : Type) -> AEAD a -> (c : Type) -> Hash c -> Type
  The TLS state after receiving change cipher spec done from a TLS 1.2 server
  This indicates the server will now begin communicating over an encrypted channel,
  and that the server is ready to receive application data from the client

  Totality: total
  Visibility: export
  Constructor: 
MkTLS2AppReadyState : TLS2ServerKEXState a b c d -> TLS2AppReadyState a b c d

  Projection: 
.kex_state : TLS2AppReadyState a b c d -> TLS2ServerKEXState a b c d
data TLS2ApplicationState : (aead : Type) -> AEAD aead -> Type
  The TLS state when communication over TLS 1.2 is ready

  Totality: total
  Visibility: export
  Constructor: 
MkTLS2ApplicationState : (a' : AEAD a) -> Application2Keys fixed_iv_length enc_key_length mac_key_length -> Nat -> Nat -> TLS2ApplicationState a a'
data TLSStep : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Init : TLSStep
  
ClientHello : TLSStep
  
ServerHello2 : TLSStep
  
ServerHello3 : TLSStep
  
Application3 : TLSStep
  
ServerCert2 : TLSStep
  
ServerKEX2 : TLSStep
  
ServerKEXDone2 : TLSStep
  
AppReady2 : TLSStep
  
Application2 : TLSStep
data TLSState : TLSStep -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
TLS_Init : TLSInitialState -> TLSState Init
  
TLS_ClientHello : TLSClientHelloState -> TLSState ClientHello
  
TLS3_ServerHello : TLS3ServerHelloState a b algo d -> TLSState ServerHello3
  
TLS3_Application : TLS3ApplicationState a b -> TLSState Application3
  
TLS2_ServerHello : TLS2ServerHelloState algo -> TLSState ServerHello2
  
TLS2_ServerCertificate : TLS2ServerCertificateState algo -> TLSState ServerCert2
  
TLS2_ServerKEX : TLS2ServerKEXState a b algo d -> TLSState ServerKEX2
  
TLS2_ServerKEXDone : TLS2ServerKEXDoneState a b algo d -> TLSState ServerKEXDone2
  
TLS2_AppReady : TLS2AppReadyState a b algo d -> TLSState AppReady2
  
TLS2_Application : TLS2ApplicationState a b -> TLSState Application2
tls_init_to_clienthello : TLSState Init -> (List Bits8, TLSState ClientHello)
  Transition from TLS Init state to TLS Client Hello state,
  and returning the payload that should be sent to the server

  Visibility: public export
tls_clienthello_to_serverhello : TLSState ClientHello -> List Bits8 -> Either String (Either (TLSState ServerHello2) (TLSState ServerHello3))
  Transition from TLS Client Hello to TLS Server Hello state after receiving Server Hello,
  return the new state depending on the server's TLS version

  Visibility: public export
tls3_serverhello_to_application : Monad m => TLSState ServerHello3 -> List Bits8 -> CertificateCheck m -> m (Either String (Either (TLSState ServerHello3) (List Bits8, TLSState Application3)))
  Transition from TLS Server Hello to TLS communication ready state after receiving server's handshake data
  note that the encrypted records containing the handshake records can be sent seperately as different records,
  or a bunch of handshake records can be concatenated into one encrypted record

  Visibility: public export
decrypt_from_record : TLSState Application3 -> List Bits8 -> Either String (TLSState Application3, List Bits8)
  Decrypt an application wrapper from the server, and updates the TLS state

  Visibility: public export
encrypt_to_record : TLSState Application3 -> List Bits8 -> (TLSState Application3, List Bits8)
  Encrypt an application data wrapper to the server, and updates the TLS state

  Visibility: public export
serverhello2_to_servercert : TLSState ServerHello2 -> List Bits8 -> Either String (TLSState ServerCert2)
  Transition from TLS Server Hello to TLS Certificate state after receiving server's certificate

  Visibility: public export
servercert_to_serverkex : Monad m => TLSState ServerCert2 -> List Bits8 -> CertificateCheck m -> m (Either String (TLSState ServerKEX2))
  Transition from TLS Server Hello to TLS Certificate state after receiving server's public key for key exchange
  This also contains a signature of the public key signed by the server's certificate
  The handshake verification step will be done here

  Visibility: public export
serverkex_process_serverhellodone : TLSState ServerKEX2 -> List Bits8 -> Either String (TLSState ServerKEXDone2, List Bits8)
  Transition from TLS Key Exchange to TLS Hello Done state after receiving server hello done
  Also returns a payload to be sent to the server

  Visibility: public export
serverhellodone_to_applicationready2 : TLSState ServerKEXDone2 -> List Bits8 -> Either String (TLSState AppReady2)
  Transition from TLS Hello Done to TLS server application ready state after receiving change cipher spec

  Visibility: public export
applicationready2_to_application2 : TLSState AppReady2 -> List Bits8 -> Either String (TLSState Application2)
  Transition from TLS server application ready state to TLS communication ready state after receiving handshake finished from server

  Visibility: public export
encrypt_to_record2 : TLSState Application2 -> List Bits8 -> (TLSState Application2, List Bits8)
  Encrypt data into TLS payload to be sent to the server

  Visibility: public export
decrypt_from_record2 : TLSState Application2 -> List Bits8 -> Either String (TLSState Application2, List Bits8)
  Decrypt TLS payload into data from the server

  Visibility: public export