Network.TLS.HKDF

Definitions

hkdf_extract : (0 algo : Type) -> {auto {conArg:2850} : Hash algo} -> List Bits8 -> List Bits8 -> Vect digest_nbyte Bits8

Visibility: public export

hkdf_expand : (0 algo : Type) -> Hash algo => (l : Nat) -> List Bits8 -> List Bits8 -> Vect l Bits8

Visibility: public export

tls13_hkdf_expand_label : (0 algo : Type) -> Hash algo => List Bits8 -> List Bits8 -> List Bits8 -> (length : Nat) -> Vect length Bits8

Visibility: export

record HandshakeKeys : Nat -> Nat -> Type

Totality: total
Visibility: public export
Constructor: 

MkHandshakeKeys : List Bits8 -> Vect key Bits8 -> Vect key Bits8 -> Vect iv Bits8 -> Vect iv Bits8 -> List Bits8 -> List Bits8 -> HandshakeKeys iv key

Projections:

.client_handshake_iv : HandshakeKeys iv key -> Vect iv Bits8

.client_handshake_key : HandshakeKeys iv key -> Vect key Bits8

.client_traffic_secret : HandshakeKeys iv key -> List Bits8

.handshake_secret : HandshakeKeys iv key -> List Bits8

.server_handshake_iv : HandshakeKeys iv key -> Vect iv Bits8

.server_handshake_key : HandshakeKeys iv key -> Vect key Bits8

.server_traffic_secret : HandshakeKeys iv key -> List Bits8

.handshake_secret : HandshakeKeys iv key -> List Bits8

Visibility: public export

handshake_secret : HandshakeKeys iv key -> List Bits8

Visibility: public export

.client_handshake_key : HandshakeKeys iv key -> Vect key Bits8

Visibility: public export

client_handshake_key : HandshakeKeys iv key -> Vect key Bits8

Visibility: public export

.server_handshake_key : HandshakeKeys iv key -> Vect key Bits8

Visibility: public export

server_handshake_key : HandshakeKeys iv key -> Vect key Bits8

Visibility: public export

.client_handshake_iv : HandshakeKeys iv key -> Vect iv Bits8

Visibility: public export

client_handshake_iv : HandshakeKeys iv key -> Vect iv Bits8

Visibility: public export

.server_handshake_iv : HandshakeKeys iv key -> Vect iv Bits8

Visibility: public export

server_handshake_iv : HandshakeKeys iv key -> Vect iv Bits8

Visibility: public export

.client_traffic_secret : HandshakeKeys iv key -> List Bits8

Visibility: public export

client_traffic_secret : HandshakeKeys iv key -> List Bits8

Visibility: public export

.server_traffic_secret : HandshakeKeys iv key -> List Bits8

Visibility: public export

server_traffic_secret : HandshakeKeys iv key -> List Bits8

Visibility: public export

record ApplicationKeys : Nat -> Nat -> Type

Totality: total
Visibility: public export
Constructor: 

MkApplicationKeys : Vect key Bits8 -> Vect key Bits8 -> Vect iv Bits8 -> Vect iv Bits8 -> ApplicationKeys iv key

Projections:

.client_application_iv : ApplicationKeys iv key -> Vect iv Bits8

.client_application_key : ApplicationKeys iv key -> Vect key Bits8

.server_application_iv : ApplicationKeys iv key -> Vect iv Bits8

.server_application_key : ApplicationKeys iv key -> Vect key Bits8

.client_application_key : ApplicationKeys iv key -> Vect key Bits8

Visibility: public export

client_application_key : ApplicationKeys iv key -> Vect key Bits8

Visibility: public export

.server_application_key : ApplicationKeys iv key -> Vect key Bits8

Visibility: public export

server_application_key : ApplicationKeys iv key -> Vect key Bits8

Visibility: public export

.client_application_iv : ApplicationKeys iv key -> Vect iv Bits8

Visibility: public export

client_application_iv : ApplicationKeys iv key -> Vect iv Bits8

Visibility: public export

.server_application_iv : ApplicationKeys iv key -> Vect iv Bits8

Visibility: public export

server_application_iv : ApplicationKeys iv key -> Vect iv Bits8

Visibility: public export

tls13_handshake_derive : (0 algo : Type) -> Hash algo => (iv : Nat) -> (key : Nat) -> List Bits8 -> List Bits8 -> HandshakeKeys iv key

Visibility: export

tls13_application_derive : (0 algo : Type) -> Hash algo => HandshakeKeys iv key -> List Bits8 -> ApplicationKeys iv key

Visibility: public export

tls13_verify_data : (0 algo : Type) -> Hash algo => List Bits8 -> List Bits8 -> List Bits8

Visibility: public export

record Application2Keys : Nat -> Nat -> Nat -> Type

Totality: total
Visibility: public export
Constructor: 

MkApplication2Keys : Vect 48 Bits8 -> Vect mac Bits8 -> Vect mac Bits8 -> Vect key Bits8 -> Vect key Bits8 -> Vect iv Bits8 -> Vect iv Bits8 -> Application2Keys iv key mac

Projections:

.client_application_iv : Application2Keys iv key mac -> Vect iv Bits8

.client_application_key : Application2Keys iv key mac -> Vect key Bits8

.client_mac_key : Application2Keys iv key mac -> Vect mac Bits8

.master_secret : Application2Keys iv key mac -> Vect 48 Bits8

.server_application_iv : Application2Keys iv key mac -> Vect iv Bits8

.server_application_key : Application2Keys iv key mac -> Vect key Bits8

.server_mac_key : Application2Keys iv key mac -> Vect mac Bits8

.master_secret : Application2Keys iv key mac -> Vect 48 Bits8

Visibility: public export

master_secret : Application2Keys iv key mac -> Vect 48 Bits8

Visibility: public export

.client_mac_key : Application2Keys iv key mac -> Vect mac Bits8

Visibility: public export

client_mac_key : Application2Keys iv key mac -> Vect mac Bits8

Visibility: public export

.server_mac_key : Application2Keys iv key mac -> Vect mac Bits8

Visibility: public export

server_mac_key : Application2Keys iv key mac -> Vect mac Bits8

Visibility: public export

.client_application_key : Application2Keys iv key mac -> Vect key Bits8

Visibility: public export

client_application_key : Application2Keys iv key mac -> Vect key Bits8

Visibility: public export

.server_application_key : Application2Keys iv key mac -> Vect key Bits8

Visibility: public export

server_application_key : Application2Keys iv key mac -> Vect key Bits8

Visibility: public export

.client_application_iv : Application2Keys iv key mac -> Vect iv Bits8

Visibility: public export

client_application_iv : Application2Keys iv key mac -> Vect iv Bits8

Visibility: public export

.server_application_iv : Application2Keys iv key mac -> Vect iv Bits8

Visibility: public export

server_application_iv : Application2Keys iv key mac -> Vect iv Bits8

Visibility: public export

tls12_application_derive : Hash algo -> (iv : Nat) -> (key : Nat) -> (mac : Nat) -> List Bits8 -> List Bits8 -> List Bits8 -> Application2Keys iv key mac

Visibility: public export

tls12_client_verify_data : Hash algo -> (n : Nat) -> List Bits8 -> List Bits8 -> Vect n Bits8

Visibility: public export

tls12_server_verify_data : Hash algo -> (n : Nat) -> List Bits8 -> List Bits8 -> Vect n Bits8

Visibility: public export