Idris2Doc : Network.TLS.Handshake

Network.TLS.Handshake

(source)
Definitions
record ClientHello : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkClientHello : TLSVersion -> Vect 32 Bits8 -> List Bits8 -> List1 CipherSuite -> List1 CompressionLevel -> List (DPair ExtensionType ClientExtension) -> ClientHello

  Projections:
  
.cipher_suites : ClientHello -> List1 CipherSuite
  
.compression_levels : ClientHello -> List1 CompressionLevel
  
.extensions : ClientHello -> List (DPair ExtensionType ClientExtension)
  
.random : ClientHello -> Vect 32 Bits8
  
.session_id : ClientHello -> List Bits8
  
.version : ClientHello -> TLSVersion

  Hint: 
Show ClientHello
.version : ClientHello -> TLSVersion
  Visibility: public export
version : ClientHello -> TLSVersion
  Visibility: public export
.random : ClientHello -> Vect 32 Bits8
  Visibility: public export
random : ClientHello -> Vect 32 Bits8
  Visibility: public export
.session_id : ClientHello -> List Bits8
  Visibility: public export
session_id : ClientHello -> List Bits8
  Visibility: public export
.cipher_suites : ClientHello -> List1 CipherSuite
  Visibility: public export
cipher_suites : ClientHello -> List1 CipherSuite
  Visibility: public export
.compression_levels : ClientHello -> List1 CompressionLevel
  Visibility: public export
compression_levels : ClientHello -> List1 CompressionLevel
  Visibility: public export
.extensions : ClientHello -> List (DPair ExtensionType ClientExtension)
  Visibility: public export
extensions : ClientHello -> List (DPair ExtensionType ClientExtension)
  Visibility: public export
record ServerHello : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkServerHello : TLSVersion -> Vect 32 Bits8 -> List Bits8 -> CipherSuite -> CompressionLevel -> List (DPair ExtensionType ServerExtension) -> ServerHello

  Projections:
  
.cipher_suite : ServerHello -> CipherSuite
  
.compression_level : ServerHello -> CompressionLevel
  
.extensions : ServerHello -> List (DPair ExtensionType ServerExtension)
  
.random : ServerHello -> Vect 32 Bits8
  
.session_id : ServerHello -> List Bits8
  
.version : ServerHello -> TLSVersion

  Hint: 
Show ServerHello
.version : ServerHello -> TLSVersion
  Visibility: public export
version : ServerHello -> TLSVersion
  Visibility: public export
.random : ServerHello -> Vect 32 Bits8
  Visibility: public export
random : ServerHello -> Vect 32 Bits8
  Visibility: public export
.session_id : ServerHello -> List Bits8
  Visibility: public export
session_id : ServerHello -> List Bits8
  Visibility: public export
.cipher_suite : ServerHello -> CipherSuite
  Visibility: public export
cipher_suite : ServerHello -> CipherSuite
  Visibility: public export
.compression_level : ServerHello -> CompressionLevel
  Visibility: public export
compression_level : ServerHello -> CompressionLevel
  Visibility: public export
.extensions : ServerHello -> List (DPair ExtensionType ServerExtension)
  Visibility: public export
extensions : ServerHello -> List (DPair ExtensionType ServerExtension)
  Visibility: public export
record EncryptedExtensions : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkEncryptedExtensions : List Bits8 -> EncryptedExtensions

  Projection: 
.get : EncryptedExtensions -> List Bits8

  Hint: 
Show EncryptedExtensions
.get : EncryptedExtensions -> List Bits8
  Visibility: public export
get : EncryptedExtensions -> List Bits8
  Visibility: public export
record CertificateEntry : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCertificateEntry : List Bits8 -> List Bits8 -> CertificateEntry

  Projections:
  
.body : CertificateEntry -> List Bits8
  
.extensions : CertificateEntry -> List Bits8

  Hint: 
Show CertificateEntry
.body : CertificateEntry -> List Bits8
  Visibility: public export
body : CertificateEntry -> List Bits8
  Visibility: public export
.extensions : CertificateEntry -> List Bits8
  Visibility: public export
extensions : CertificateEntry -> List Bits8
  Visibility: public export
record Certificate : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCertificate : List Bits8 -> List CertificateEntry -> Certificate

  Projections:
  
.certificates : Certificate -> List CertificateEntry
  
.request_context : Certificate -> List Bits8

  Hint: 
Show Certificate
.request_context : Certificate -> List Bits8
  Visibility: public export
request_context : Certificate -> List Bits8
  Visibility: public export
.certificates : Certificate -> List CertificateEntry
  Visibility: public export
certificates : Certificate -> List CertificateEntry
  Visibility: public export
record CertificateVerify : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCertificateVerify : SignatureAlgorithm -> List Bits8 -> CertificateVerify

  Projections:
  
.signature : CertificateVerify -> List Bits8
  
.signature_algorithm : CertificateVerify -> SignatureAlgorithm

  Hint: 
Show CertificateVerify
.signature_algorithm : CertificateVerify -> SignatureAlgorithm
  Visibility: public export
signature_algorithm : CertificateVerify -> SignatureAlgorithm
  Visibility: public export
.signature : CertificateVerify -> List Bits8
  Visibility: public export
signature : CertificateVerify -> List Bits8
  Visibility: public export
record Finished : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkFinished : List Bits8 -> Finished

  Projection: 
.verify_data : Finished -> List Bits8

  Hint: 
Show Finished
.verify_data : Finished -> List Bits8
  Visibility: public export
verify_data : Finished -> List Bits8
  Visibility: public export
record NewSessionTicket : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkNewSessionTicket : Nat -> Nat -> List Bits8 -> List Bits8 -> List ((Bits8, Bits8), List Bits8) -> NewSessionTicket

  Projections:
  
.age_add_milliseconds : NewSessionTicket -> Nat
  
.extensions : NewSessionTicket -> List ((Bits8, Bits8), List Bits8)
  
.lifetime_seconds : NewSessionTicket -> Nat
  
.nonce : NewSessionTicket -> List Bits8
  
.session_ticket : NewSessionTicket -> List Bits8

  Hint: 
Show NewSessionTicket
.lifetime_seconds : NewSessionTicket -> Nat
  Visibility: public export
lifetime_seconds : NewSessionTicket -> Nat
  Visibility: public export
.age_add_milliseconds : NewSessionTicket -> Nat
  Visibility: public export
age_add_milliseconds : NewSessionTicket -> Nat
  Visibility: public export
.nonce : NewSessionTicket -> List Bits8
  Visibility: public export
nonce : NewSessionTicket -> List Bits8
  Visibility: public export
.session_ticket : NewSessionTicket -> List Bits8
  Visibility: public export
session_ticket : NewSessionTicket -> List Bits8
  Visibility: public export
.extensions : NewSessionTicket -> List ((Bits8, Bits8), List Bits8)
  Visibility: public export
extensions : NewSessionTicket -> List ((Bits8, Bits8), List Bits8)
  Visibility: public export
record ServerKeyExchange : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkServerKeyExchange : SupportedGroup -> List Bits8 -> SignatureAlgorithm -> List Bits8 -> ServerKeyExchange

  Projections:
  
.server_pk_body : ServerKeyExchange -> List Bits8
  
.server_pk_group : ServerKeyExchange -> SupportedGroup
  
.signature_algo : ServerKeyExchange -> SignatureAlgorithm
  
.signature_body : ServerKeyExchange -> List Bits8

  Hint: 
Show ServerKeyExchange
.server_pk_group : ServerKeyExchange -> SupportedGroup
  Visibility: public export
server_pk_group : ServerKeyExchange -> SupportedGroup
  Visibility: public export
.server_pk_body : ServerKeyExchange -> List Bits8
  Visibility: public export
server_pk_body : ServerKeyExchange -> List Bits8
  Visibility: public export
.signature_algo : ServerKeyExchange -> SignatureAlgorithm
  Visibility: public export
signature_algo : ServerKeyExchange -> SignatureAlgorithm
  Visibility: public export
.signature_body : ServerKeyExchange -> List Bits8
  Visibility: public export
signature_body : ServerKeyExchange -> List Bits8
  Visibility: public export
data ServerHelloDone : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkServerHelloDone : ServerHelloDone

  Hint: 
Show ServerHelloDone
record ClientKeyExchange : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkClientKeyExchange : List Bits8 -> ClientKeyExchange

  Projection: 
.public_key : ClientKeyExchange -> List Bits8

  Hint: 
Show ClientKeyExchange
.public_key : ClientKeyExchange -> List Bits8
  Visibility: public export
public_key : ClientKeyExchange -> List Bits8
  Visibility: public export
data Handshake : HandshakeType -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
ClientHello : ClientHello -> Handshake ClientHello
  
ServerHello : ServerHello -> Handshake ServerHello
  
EncryptedExtensions : EncryptedExtensions -> Handshake EncryptedExtensions
  
Certificate : Certificate -> Handshake Certificate
  
CertificateVerify : CertificateVerify -> Handshake CertificateVerify
  
Finished : Finished -> Handshake Finished
  
NewSessionTicket : NewSessionTicket -> Handshake NewSessionTicket
  
ServerKeyExchange : ServerKeyExchange -> Handshake ServerKeyExchange
  
ServerHelloDone : ServerHelloDone -> Handshake ServerHelloDone
  
ClientKeyExchange : ClientKeyExchange -> Handshake ClientKeyExchange

  Hint: 
Show (Handshake type)
handshake_id_with_length : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (HandshakeType, Nat)
  Visibility: export
no_id_client_hello : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ClientHello)
  Visibility: export
no_id_server_hello : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ServerHello)
  Visibility: export
no_id_encrypted_extensions : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake EncryptedExtensions)
  Visibility: export
no_id_certificate : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake Certificate)
  Visibility: export
no_id_certificate2 : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake Certificate)
  Visibility: export
no_id_certificate_verify : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake CertificateVerify)
  Visibility: export
no_id_finished : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake Finished)
  Visibility: export
no_id_new_session_ticket : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake NewSessionTicket)
  Visibility: export
no_id_server_key_exchange : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ServerKeyExchange)
  Visibility: export
no_id_server_hello_done : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ServerHelloDone)
  Visibility: export
no_id_client_key_exchange : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ClientKeyExchange)
  Visibility: export
with_id : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake type) -> Parserializer Bits8 i (SimpleError String) (Handshake type)
  Visibility: export
handshake : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (DPair HandshakeType Handshake)
  Visibility: export
handshake2 : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (DPair HandshakeType Handshake)
  Visibility: export