0 | module Network.TLS.Magic

  2 | import Data.Vect

  3 | import Network.TLS.Parsing

  4 | import Network.TLS.AEAD

  5 | import Utils.Bytes

  6 | import Utils.Misc

  7 | import Crypto.Hash

  8 | import Crypto.ECDH

  9 | import Crypto.Curve

 10 | import Crypto.Curve.Weierstrass

 11 | import Derive.Prelude

 12 | import Generics.Derive

 14 | %hide Generics.Derive.Eq

 15 | %hide Generics.Derive.Ord

 16 | %hide Generics.Derive.Show

 18 | %language ElabReflection

 21 | public export

 22 | data AlertLevel : Type where

 23 |   Warning : AlertLevel

 24 |   Fatal : AlertLevel

 26 | %runElab derive "AlertLevel" [Generic, Meta, Eq, Show]

 28 | public export

 29 | alert_level_to_id : AlertLevel -> Bits8

 30 | alert_level_to_id Warning = 1

 31 | alert_level_to_id Fatal = 2

 33 | public export

 34 | id_to_alert_level : Bits8 -> Maybe AlertLevel

 35 | id_to_alert_level 1 = Just Warning

 36 | id_to_alert_level 2 = Just Warning

 37 | id_to_alert_level _ = Nothing

 39 | public export

 40 | data AlertDescription : Type where

 41 |   CloseNotify : AlertDescription

 42 |   UnexpectedMessage : AlertDescription

 43 |   BadRecordMac : AlertDescription

 44 |   RecordOverflow : AlertDescription

 45 |   HandshakeFailure : AlertDescription

 46 |   BadCertificate : AlertDescription

 47 |   UnsupportedCertificate : AlertDescription

 48 |   CertificateRevoked : AlertDescription

 49 |   CertificateExpired : AlertDescription

 50 |   CertificateUnknown : AlertDescription

 51 |   IllegalParameter : AlertDescription

 52 |   UnknownCA : AlertDescription

 53 |   AccessDenied : AlertDescription

 54 |   DecodeError : AlertDescription

 55 |   DecryptError : AlertDescription

 56 |   ProtocolVersion : AlertDescription

 57 |   InsufficientSecurity : AlertDescription

 58 |   InternalError : AlertDescription

 59 |   InappropriateFallback : AlertDescription

 60 |   UserCanceled : AlertDescription

 61 |   MissingExtension : AlertDescription

 62 |   UnsupportedExtension : AlertDescription

 63 |   UnrecognizedName : AlertDescription

 64 |   BadCertificateStatusResponse : AlertDescription

 65 |   UnknownPskIdentity : AlertDescription

 66 |   CertificateRequired : AlertDescription

 67 |   NoApplicationProtocol : AlertDescription

 69 | %runElab derive "AlertDescription" [Generic, Meta, Eq, Show]

 71 | public export

 72 | alert_description_to_id : AlertDescription -> Bits8

 73 | alert_description_to_id CloseNotify = 0

 74 | alert_description_to_id UnexpectedMessage = 10

 75 | alert_description_to_id BadRecordMac = 20

 76 | alert_description_to_id RecordOverflow = 22

 77 | alert_description_to_id HandshakeFailure = 40

 78 | alert_description_to_id BadCertificate = 42

 79 | alert_description_to_id UnsupportedCertificate = 43

 80 | alert_description_to_id CertificateRevoked = 44

 81 | alert_description_to_id CertificateExpired = 45

 82 | alert_description_to_id CertificateUnknown = 46

 83 | alert_description_to_id IllegalParameter = 47

 84 | alert_description_to_id UnknownCA = 48

 85 | alert_description_to_id AccessDenied = 49

 86 | alert_description_to_id DecodeError = 50

 87 | alert_description_to_id DecryptError = 51

 88 | alert_description_to_id ProtocolVersion = 70

 89 | alert_description_to_id InsufficientSecurity = 71

 90 | alert_description_to_id InternalError = 80

 91 | alert_description_to_id InappropriateFallback = 86

 92 | alert_description_to_id UserCanceled = 90

 93 | alert_description_to_id MissingExtension = 109

 94 | alert_description_to_id UnsupportedExtension = 110

 95 | alert_description_to_id UnrecognizedName = 112

 96 | alert_description_to_id BadCertificateStatusResponse = 113

 97 | alert_description_to_id UnknownPskIdentity = 115

 98 | alert_description_to_id CertificateRequired = 116

 99 | alert_description_to_id NoApplicationProtocol = 120

101 | public export

102 | id_to_alert_description : Bits8 -> Maybe AlertDescription

103 | id_to_alert_description 0 = Just CloseNotify

104 | id_to_alert_description 10 = Just UnexpectedMessage

105 | id_to_alert_description 20 = Just BadRecordMac

106 | id_to_alert_description 22 = Just RecordOverflow

107 | id_to_alert_description 40 = Just HandshakeFailure

108 | id_to_alert_description 42 = Just BadCertificate

109 | id_to_alert_description 43 = Just UnsupportedCertificate

110 | id_to_alert_description 44 = Just CertificateRevoked

111 | id_to_alert_description 45 = Just CertificateExpired

112 | id_to_alert_description 46 = Just CertificateUnknown

113 | id_to_alert_description 47 = Just IllegalParameter

114 | id_to_alert_description 48 = Just UnknownCA

115 | id_to_alert_description 49 = Just AccessDenied

116 | id_to_alert_description 50 = Just DecodeError

117 | id_to_alert_description 51 = Just DecryptError

118 | id_to_alert_description 70 = Just ProtocolVersion

119 | id_to_alert_description 71 = Just InsufficientSecurity

120 | id_to_alert_description 80 = Just InternalError

121 | id_to_alert_description 86 = Just InappropriateFallback

122 | id_to_alert_description 90 = Just UserCanceled

123 | id_to_alert_description 109 = Just MissingExtension

124 | id_to_alert_description 110 = Just UnsupportedExtension

125 | id_to_alert_description 112 = Just UnrecognizedName

126 | id_to_alert_description 113 = Just BadCertificateStatusResponse

127 | id_to_alert_description 115 = Just UnknownPskIdentity

128 | id_to_alert_description 116 = Just CertificateRequired

129 | id_to_alert_description 120 = Just NoApplicationProtocol

130 | id_to_alert_description _ = Nothing

132 | public export

133 | data SupportedGroup : Type where

134 |   X25519 : SupportedGroup

135 |   X448 : SupportedGroup

136 |   SECP256r1 : SupportedGroup

137 |   SECP384r1 : SupportedGroup

138 |   SECP521r1 : SupportedGroup

140 | %runElab derive "SupportedGroup" [Generic, Meta, Eq, Show]

142 | public export

143 | supported_group_to_id : SupportedGroup -> (Bits8, Bits8)

144 | supported_group_to_id X25519 = (0x00, 0x1d)

145 | supported_group_to_id X448 = (0x00, 0x1e)

146 | supported_group_to_id SECP256r1 = (0x00, 0x17)

147 | supported_group_to_id SECP384r1 = (0x00, 0x18)

148 | supported_group_to_id SECP521r1 = (0x00, 0x19)

150 | public export

151 | id_to_supported_group : (Bits8, Bits8) -> Maybe SupportedGroup

152 | id_to_supported_group (0x00, 0x1d) = Just X25519

153 | id_to_supported_group (0x00, 0x1e) = Just X448

154 | id_to_supported_group (0x00, 0x17) = Just SECP256r1

155 | id_to_supported_group (0x00, 0x18) = Just SECP384r1

156 | id_to_supported_group (0x00, 0x19) = Just SECP521r1

157 | id_to_supported_group _ = Nothing

159 | public export

160 | curve_group_to_type : SupportedGroup -> (DPair Type ECDHCyclicGroup)

161 | curve_group_to_type X25519 = MkDPair X25519_DH %search

162 | curve_group_to_type X448 = MkDPair X448_DH %search

163 | curve_group_to_type SECP256r1 = MkDPair P256 %search

164 | curve_group_to_type SECP384r1 = MkDPair P384 %search

165 | curve_group_to_type SECP521r1 = MkDPair P521 %search

167 | public export

168 | curve_group_to_scalar_type : SupportedGroup -> Type

169 | curve_group_to_scalar_type group = Scalar @{snd $ curve_group_to_type group}

171 | public export

172 | curve_group_to_element_type : SupportedGroup -> Type

173 | curve_group_to_element_type group = Element @{snd $ curve_group_to_type group}

175 | public export

176 | data SignatureAlgorithm : Type where

177 |   RSA_PKCS1_SHA256       : SignatureAlgorithm

178 |   RSA_PKCS1_SHA384       : SignatureAlgorithm

179 |   RSA_PKCS1_SHA512       : SignatureAlgorithm

181 |   ECDSA_SECP256r1_SHA256 : SignatureAlgorithm

182 |   ECDSA_SECP384r1_SHA384 : SignatureAlgorithm

183 |   ECDSA_SECP521r1_SHA512 : SignatureAlgorithm

185 |   RSA_PSS_RSAE_SHA256    : SignatureAlgorithm

186 |   RSA_PSS_RSAE_SHA384    : SignatureAlgorithm

187 |   RSA_PSS_RSAE_SHA512    : SignatureAlgorithm

189 | %runElab derive "SignatureAlgorithm" [Generic, Meta, Eq, Show]

191 | public export

192 | signature_algorithm_to_id : SignatureAlgorithm -> (Bits8, Bits8)

193 | signature_algorithm_to_id RSA_PKCS1_SHA256 = (0x04, 0x01)

194 | signature_algorithm_to_id RSA_PKCS1_SHA384 = (0x05, 0x01)

195 | signature_algorithm_to_id RSA_PKCS1_SHA512 = (0x06, 0x01)

197 | signature_algorithm_to_id ECDSA_SECP256r1_SHA256 = (0x04, 0x03)

198 | signature_algorithm_to_id ECDSA_SECP384r1_SHA384 = (0x05, 0x03)

199 | signature_algorithm_to_id ECDSA_SECP521r1_SHA512 = (0x06, 0x03)

201 | signature_algorithm_to_id RSA_PSS_RSAE_SHA256 = (0x08, 0x04)

202 | signature_algorithm_to_id RSA_PSS_RSAE_SHA384 = (0x08, 0x05)

203 | signature_algorithm_to_id RSA_PSS_RSAE_SHA512 = (0x08, 0x06)

205 | public export

206 | id_to_signature_algorithm : (Bits8, Bits8) -> Maybe SignatureAlgorithm

207 | id_to_signature_algorithm (0x04, 0x01) = Just RSA_PKCS1_SHA256

208 | id_to_signature_algorithm (0x05, 0x01) = Just RSA_PKCS1_SHA384

209 | id_to_signature_algorithm (0x06, 0x01) = Just RSA_PKCS1_SHA512

211 | id_to_signature_algorithm (0x04, 0x03) = Just ECDSA_SECP256r1_SHA256

212 | id_to_signature_algorithm (0x05, 0x03) = Just ECDSA_SECP384r1_SHA384

213 | id_to_signature_algorithm (0x06, 0x03) = Just ECDSA_SECP521r1_SHA512

215 | id_to_signature_algorithm (0x08, 0x04) = Just RSA_PSS_RSAE_SHA256

216 | id_to_signature_algorithm (0x08, 0x05) = Just RSA_PSS_RSAE_SHA384

217 | id_to_signature_algorithm (0x08, 0x06) = Just RSA_PSS_RSAE_SHA512

219 | id_to_signature_algorithm _ = Nothing

221 | public export

222 | data CompressionLevel : Type where

223 |   Null : CompressionLevel

225 | %runElab derive "CompressionLevel" [Generic, Meta, Eq, Show]

227 | public export

228 | compression_level_to_id : CompressionLevel -> Bits8

229 | compression_level_to_id Null = 0x00

231 | public export

232 | id_to_compression_level : Bits8 -> Maybe CompressionLevel

233 | id_to_compression_level 0x00 = Just Null

234 | id_to_compression_level _ = Nothing

236 | public export

237 | data CipherSuite : Type where

238 |   ||| TLS 1.3 Cipher Suites

239 |   TLS_AES_128_GCM_SHA256 : CipherSuite

240 |   TLS_AES_256_GCM_SHA384 : CipherSuite

241 |   TLS_CHACHA20_POLY1305_SHA256 : CipherSuite

242 |   ||| TLS 1.2 Cipher Suites

243 |   TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 : CipherSuite

244 |   TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 : CipherSuite

245 |   TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256 : CipherSuite

246 |   TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 : CipherSuite

247 |   TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256 : CipherSuite

248 |   TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256 : CipherSuite

250 | %runElab derive "CipherSuite" [Generic, Meta, Eq, Show]

252 | public export

253 | cipher_suite_to_id : CipherSuite -> (Bits8, Bits8)

254 | cipher_suite_to_id TLS_AES_128_GCM_SHA256 = (0x13, 0x01)

255 | cipher_suite_to_id TLS_AES_256_GCM_SHA384 = (0x13, 0x02)

256 | cipher_suite_to_id TLS_CHACHA20_POLY1305_SHA256 = (0x13, 0x03)

257 | cipher_suite_to_id TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 = (0xc0, 0x2f)

258 | cipher_suite_to_id TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 = (0xc0, 0x30)

259 | cipher_suite_to_id TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256 = (0xc0, 0x2b)

260 | cipher_suite_to_id TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 = (0xc0, 0x2c)

261 | cipher_suite_to_id TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256 = (0xcc, 0xa8)

262 | cipher_suite_to_id TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256 = (0xcc, 0xa9)

264 | public export

265 | id_to_cipher_suite : (Bits8, Bits8) -> Maybe CipherSuite

266 | id_to_cipher_suite (0x13, 0x01) = Just TLS_AES_128_GCM_SHA256

267 | id_to_cipher_suite (0x13, 0x02) = Just TLS_AES_256_GCM_SHA384

268 | id_to_cipher_suite (0x13, 0x03) = Just TLS_CHACHA20_POLY1305_SHA256

269 | id_to_cipher_suite (0xc0, 0x2f) = Just TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256

270 | id_to_cipher_suite (0xc0, 0x30) = Just TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384

271 | id_to_cipher_suite (0xc0, 0x2b) = Just TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256

272 | id_to_cipher_suite (0xc0, 0x2c) = Just TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384

273 | id_to_cipher_suite (0xcc, 0xa8) = Just TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256

274 | id_to_cipher_suite (0xcc, 0xa9) = Just TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256

275 | id_to_cipher_suite _ = Nothing

277 | public export

278 | ciphersuite_to_hash_type : CipherSuite -> (DPair Type Hash)

279 | ciphersuite_to_hash_type TLS_AES_128_GCM_SHA256 = MkDPair Sha256 %search

280 | ciphersuite_to_hash_type TLS_AES_256_GCM_SHA384 = MkDPair Sha384 %search

281 | ciphersuite_to_hash_type TLS_CHACHA20_POLY1305_SHA256 = MkDPair Sha256 %search

282 | ciphersuite_to_hash_type TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 = MkDPair Sha256 %search

283 | ciphersuite_to_hash_type TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 = MkDPair Sha384 %search

284 | ciphersuite_to_hash_type TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256 = MkDPair Sha256 %search

285 | ciphersuite_to_hash_type TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 = MkDPair Sha384 %search

286 | ciphersuite_to_hash_type TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256 = MkDPair Sha256 %search

287 | ciphersuite_to_hash_type TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256 = MkDPair Sha256 %search

289 | public export

290 | ciphersuite_to_prf_type : CipherSuite -> (DPair Type Hash)

291 | ciphersuite_to_prf_type TLS_AES_256_GCM_SHA384 = MkDPair Sha384 %search

292 | ciphersuite_to_prf_type TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 = MkDPair Sha384 %search

293 | ciphersuite_to_prf_type TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 = MkDPair Sha384 %search

294 | ciphersuite_to_prf_type _ = MkDPair Sha256 %search

296 | public export

297 | ciphersuite_to_verify_data_len : CipherSuite -> Nat

298 | ciphersuite_to_verify_data_len _ = 12

300 | public export

301 | ciphersuite_to_aead_type : CipherSuite -> (DPair Type AEAD)

302 | ciphersuite_to_aead_type TLS_AES_128_GCM_SHA256 = MkDPair TLS13_AES_128_GCM %search

303 | ciphersuite_to_aead_type TLS_AES_256_GCM_SHA384 = MkDPair TLS13_AES_256_GCM %search

305 | ciphersuite_to_aead_type TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 = MkDPair TLS12_AES_128_GCM %search

306 | ciphersuite_to_aead_type TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 = MkDPair TLS12_AES_256_GCM %search

307 | ciphersuite_to_aead_type TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256 = MkDPair TLS12_AES_128_GCM %search

308 | ciphersuite_to_aead_type TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 = MkDPair TLS12_AES_256_GCM %search

310 | ciphersuite_to_aead_type TLS_CHACHA20_POLY1305_SHA256 = MkDPair TLS1213_ChaCha20_Poly1305 %search

311 | ciphersuite_to_aead_type TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256 = MkDPair TLS1213_ChaCha20_Poly1305 %search

312 | ciphersuite_to_aead_type TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256 = MkDPair TLS1213_ChaCha20_Poly1305 %search

314 | public export

315 | data TLSVersion : Type where

316 |   TLS10 : TLSVersion

317 |   TLS11 : TLSVersion

318 |   TLS12 : TLSVersion

319 |   TLS13 : TLSVersion

321 | public export

322 | tls_version_to_id : TLSVersion -> (Bits8, Bits8)

323 | tls_version_to_id TLS10 = (0x03, 0x01)

324 | tls_version_to_id TLS11 = (0x03, 0x02)

325 | tls_version_to_id TLS12 = (0x03, 0x03)

326 | tls_version_to_id TLS13 = (0x03, 0x04)

328 | public export

329 | id_to_tls_version : (Bits8, Bits8) -> Maybe TLSVersion

330 | id_to_tls_version (0x03, 0x01) = Just TLS10

331 | id_to_tls_version (0x03, 0x02) = Just TLS11

332 | id_to_tls_version (0x03, 0x03) = Just TLS12

333 | id_to_tls_version (0x03, 0x04) = Just TLS13

334 | id_to_tls_version _ = Nothing

336 | %runElab derive "TLSVersion" [Generic, Meta, Eq, Ord, Show]

338 | public export

339 | data ExtensionType : Type where

340 |   ServerName : ExtensionType

341 |   SupportedGroups : ExtensionType

342 |   SupportedVersions : ExtensionType

343 |   SignatureAlgorithms : ExtensionType

344 |   KeyShare : ExtensionType

345 |   Unknown : (Bits8, Bits8) -> ExtensionType

347 | %runElab derive "ExtensionType" [Generic, Meta, Eq, Show]

349 | public export

350 | extension_type_to_id : ExtensionType -> (Bits8, Bits8)

351 | extension_type_to_id ServerName          = (0x00, 0x00)

352 | extension_type_to_id SupportedGroups     = (0x00, 0x0a)

353 | extension_type_to_id SignatureAlgorithms = (0x00, 0x0d)

354 | extension_type_to_id SupportedVersions   = (0x00, 0x2b)

355 | extension_type_to_id KeyShare            = (0x00, 0x33)

356 | extension_type_to_id (Unknown x)         = x

358 | public export

359 | id_to_extension_type : (Bits8, Bits8) -> ExtensionType

360 | id_to_extension_type (0x00, 0x00) = ServerName

361 | id_to_extension_type (0x00, 0x0a) = SupportedGroups

362 | id_to_extension_type (0x00, 0x0d) = SignatureAlgorithms

363 | id_to_extension_type (0x00, 0x2b) = SupportedVersions

364 | id_to_extension_type (0x00, 0x33) = KeyShare

365 | id_to_extension_type x = Unknown x

367 | public export

368 | data HandshakeType : Type where

369 |   ClientHello : HandshakeType

370 |   ServerHello : HandshakeType

371 |   NewSessionTicket : HandshakeType

372 |   EncryptedExtensions : HandshakeType

373 |   Certificate : HandshakeType

374 |   CertificateVerify : HandshakeType

375 |   Finished : HandshakeType

376 |   ServerKeyExchange : HandshakeType

377 |   ServerHelloDone : HandshakeType

378 |   ClientKeyExchange : HandshakeType

380 | %runElab derive "HandshakeType" [Generic, Meta, Eq, Show]

382 | public export

383 | handshake_type_to_id : HandshakeType -> Bits8

384 | handshake_type_to_id ClientHello = 0x01

385 | handshake_type_to_id ServerHello = 0x02

386 | handshake_type_to_id NewSessionTicket = 0x04

387 | handshake_type_to_id EncryptedExtensions = 0x08

388 | handshake_type_to_id Certificate = 0x0b

389 | handshake_type_to_id CertificateVerify = 0x0f

390 | handshake_type_to_id Finished = 0x14

391 | handshake_type_to_id ServerKeyExchange = 0x0c

392 | handshake_type_to_id ServerHelloDone = 0x0e

393 | handshake_type_to_id ClientKeyExchange = 0x10

395 | public export

396 | id_to_handshake_type : Bits8 -> Maybe HandshakeType

397 | id_to_handshake_type 0x01 = Just ClientHello

398 | id_to_handshake_type 0x02 = Just ServerHello

399 | id_to_handshake_type 0x04 = Just NewSessionTicket

400 | id_to_handshake_type 0x08 = Just EncryptedExtensions

401 | id_to_handshake_type 0x0b = Just Certificate

402 | id_to_handshake_type 0x0f = Just CertificateVerify

403 | id_to_handshake_type 0x14 = Just Finished

404 | id_to_handshake_type 0x0c = Just ServerKeyExchange

405 | id_to_handshake_type 0x0e = Just ServerHelloDone

406 | id_to_handshake_type 0x10 = Just ClientKeyExchange

407 | id_to_handshake_type _ = Nothing

409 | public export

410 | data RecordType : Type where

411 |   ChangeCipherSpec : RecordType

412 |   Handshake : RecordType

413 |   ApplicationData : RecordType

414 |   Alert : RecordType

416 | %runElab derive "RecordType" [Generic, Meta, Eq, Show]

418 | public export

419 | record_type_to_id : RecordType -> Bits8

420 | record_type_to_id ChangeCipherSpec = 0x14

421 | record_type_to_id Handshake = 0x16

422 | record_type_to_id ApplicationData = 0x17

423 | record_type_to_id Alert = 0x15

425 | public export

426 | id_to_record_type : Bits8 -> Maybe RecordType

427 | id_to_record_type 0x14 = Just ChangeCipherSpec

428 | id_to_record_type 0x15 = Just Alert

429 | id_to_record_type 0x16 = Just Handshake

430 | id_to_record_type 0x17 = Just ApplicationData

431 | id_to_record_type _ = Nothing

433 | namespace Parsing

434 |   ||| creates a parserializer given an isomorphism from a type to a constant

435 |   export

436 |   magic : (Cons (Posed Bits8) i, Monoid i) => {k : Nat} -> (a -> Vect (S k) Bits8) -> (Vect (S k) Bits8 -> Maybe a) -> Parserializer Bits8 i (SimpleError String) a

437 |   magic encode decode = MkParserializer (toList . encode) $ do

438 |     bs <- count (S k) token

439 |     let bytes = map get bs

440 |     let Just phi = decode bytes

441 |     | Nothing =>

442 |       let

443 |         (begin, end) = mapHom pos (head bs, last bs)

444 |       in

445 |         fail $ msg $ "at position " <+> show begin <+> "-" <+> show end <+> ", unknown id: " <+> xxd (toList bytes)

446 |     pure phi

448 |   export

449 |   alert_level : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) AlertLevel

450 |   alert_level = under "alert level" $ magic (to_vect . alert_level_to_id) (id_to_alert_level . from_vect)

452 |   export

453 |   alert_description : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) AlertDescription

454 |   alert_description = magic (to_vect . alert_description_to_id) (id_to_alert_description . from_vect)

456 |   export

457 |   tls_version : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) TLSVersion

458 |   tls_version = under "tls version" $ magic (pair_to_vect . tls_version_to_id) (id_to_tls_version . vect_to_pair)

460 |   export

461 |   cipher_suite : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) CipherSuite

462 |   cipher_suite = under "cipher suite" $ magic (pair_to_vect . cipher_suite_to_id) (id_to_cipher_suite . vect_to_pair)

464 |   export

465 |   supported_group : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) SupportedGroup

466 |   supported_group = under "supported group" $ magic (pair_to_vect . supported_group_to_id) (id_to_supported_group . vect_to_pair)

468 |   export

469 |   signature_algorithm : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) SignatureAlgorithm

470 |   signature_algorithm = under "signature algorithm" $ magic (pair_to_vect . signature_algorithm_to_id) (id_to_signature_algorithm . vect_to_pair)

472 |   export

473 |   compression_level : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) CompressionLevel

474 |   compression_level = under "compression level" $ magic (to_vect . compression_level_to_id) (id_to_compression_level . from_vect)

476 |   public export

477 |   extension_type : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) ExtensionType

478 |   extension_type = under "extension type" $ magic (pair_to_vect . extension_type_to_id) (Just . id_to_extension_type . vect_to_pair)

480 |   public export

481 |   handshake_type : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) HandshakeType

482 |   handshake_type = under "handshake type" $ magic (to_vect . handshake_type_to_id) (id_to_handshake_type . from_vect)

484 |   export

485 |   record_type : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) RecordType

486 |   record_type = under "record type" $ magic (to_vect . record_type_to_id) (id_to_record_type . from_vect)