Network.TLS.AEAD

Definitions

interface AEAD : Type -> Type

Parameters: a
Methods:

fixed_iv_length : Nat

  IV generated during key exchange

enc_key_length : Nat

mac_length : Nat

mac_key_length : Nat

record_iv_length : Nat

  Part of IV that is sent along with the ciphertext, should always be 0 in TLS 1.3

encrypt : Vect enc_key_length Bits8 -> Vect fixed_iv_length Bits8 -> Vect mac_key_length Bits8 -> Nat -> List Bits8 -> List Bits8 -> (Vect record_iv_length Bits8, (List Bits8, Vect mac_length Bits8))

decrypt : Vect enc_key_length Bits8 -> Vect fixed_iv_length Bits8 -> Vect record_iv_length Bits8 -> Vect mac_key_length Bits8 -> Nat -> List Bits8 -> (List Bits8 -> List Bits8) -> List Bits8 -> (List Bits8, Bool)

Implementations:

AEAD TLS13_AES_128_GCM

AEAD TLS12_AES_128_GCM

AEAD TLS13_AES_256_GCM

AEAD TLS12_AES_256_GCM

AEAD TLS1213_ChaCha20_Poly1305

fixed_iv_length : AEAD a => Nat

  IV generated during key exchange

Visibility: public export

enc_key_length : AEAD a => Nat

Visibility: public export

mac_length : AEAD a => Nat

Visibility: public export

mac_key_length : AEAD a => Nat

Visibility: public export

record_iv_length : AEAD a => Nat

  Part of IV that is sent along with the ciphertext, should always be 0 in TLS 1.3

Visibility: public export

encrypt : {auto __con : AEAD a} -> Vect enc_key_length Bits8 -> Vect fixed_iv_length Bits8 -> Vect mac_key_length Bits8 -> Nat -> List Bits8 -> List Bits8 -> (Vect record_iv_length Bits8, (List Bits8, Vect mac_length Bits8))

Visibility: public export

decrypt : {auto __con : AEAD a} -> Vect enc_key_length Bits8 -> Vect fixed_iv_length Bits8 -> Vect record_iv_length Bits8 -> Vect mac_key_length Bits8 -> Nat -> List Bits8 -> (List Bits8 -> List Bits8) -> List Bits8 -> (List Bits8, Bool)

Visibility: public export

data TLS13_AES_128_GCM : Type

Totality: total
Visibility: public export
Hint: 

AEAD TLS13_AES_128_GCM

data TLS12_AES_128_GCM : Type

Totality: total
Visibility: public export
Hint: 

AEAD TLS12_AES_128_GCM

data TLS13_AES_256_GCM : Type

Totality: total
Visibility: public export
Hint: 

AEAD TLS13_AES_256_GCM

data TLS12_AES_256_GCM : Type

Totality: total
Visibility: public export
Hint: 

AEAD TLS12_AES_256_GCM

data TLS1213_ChaCha20_Poly1305 : Type

Totality: total
Visibility: public export
Hint: 

AEAD TLS1213_ChaCha20_Poly1305