0 | module Network.TLS.Core

  2 | import Crypto.Curve

  3 | import Crypto.Curve.Weierstrass

  4 | import Crypto.Curve.XCurves

  5 | import Crypto.ECDH

  6 | import Network.TLS.HKDF

  7 | import Network.TLS.AEAD

  8 | import Network.TLS.Signature

  9 | import Crypto.Hash

 10 | import Crypto.Hash.OID

 11 | import Crypto.Random

 12 | import Crypto.RSA

 13 | import Data.Bits

 14 | import Data.List

 15 | import Data.List1

 16 | import Data.Vect

 17 | import Data.DPair

 18 | import Network.Socket

 19 | import Network.TLS.Record

 20 | import Utils.Bytes

 21 | import Utils.Misc

 22 | import Utils.Parser

 23 | import Control.Monad.Error.Either

 25 | hash_to_digest : Hash algo -> Digest algo

 26 | hash_to_digest = %search

 29 | public export

 30 | tls13_supported_cipher_suites : List1 CipherSuite

 31 | tls13_supported_cipher_suites =

 32 |   TLS_AES_128_GCM_SHA256 ::: [ TLS_AES_256_GCM_SHA384, TLS_CHACHA20_POLY1305_SHA256 ]

 35 | public export

 36 | tls12_supported_cipher_suites : List1 CipherSuite

 37 | tls12_supported_cipher_suites =

 38 |   TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 :::

 39 |   [ TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256

 40 |   , TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384

 41 |   , TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384

 42 |   , TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256

 43 |   , TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256 ]

 46 | public export

 47 | supported_groups : List1 SupportedGroup

 48 | supported_groups = X25519 ::: [SECP256r1, X448, SECP384r1, SECP521r1]

 51 | public export

 52 | supported_signature_algorithms : List1 SignatureAlgorithm

 53 | supported_signature_algorithms =

 54 |   RSA_PKCS1_SHA256 :::

 55 |   [ RSA_PKCS1_SHA384

 56 |   , RSA_PKCS1_SHA512

 57 |   , ECDSA_SECP256r1_SHA256

 58 |   , ECDSA_SECP384r1_SHA384

 59 |   , ECDSA_SECP521r1_SHA512

 60 |   , RSA_PSS_RSAE_SHA256 

 61 |   , RSA_PSS_RSAE_SHA384 

 62 |   , RSA_PSS_RSAE_SHA512 

 63 |   ]

 65 | rsa_pss_params : (algo : _) -> (h : Hash algo) => SignatureParameter

 66 | rsa_pss_params algo = RSA_PSS (algo ** h) (digest_nbyte {algo}) (mgf1 {algo})

 69 | sig_alg_get_params : SignatureAlgorithm -> SignatureParameter

 70 | sig_alg_get_params RSA_PKCS1_SHA256 = RSA_PKCSv15 (MkDPair Sha256 %search)

 71 | sig_alg_get_params RSA_PKCS1_SHA384 = RSA_PKCSv15 (MkDPair Sha384 %search)

 72 | sig_alg_get_params RSA_PKCS1_SHA512 = RSA_PKCSv15 (MkDPair Sha512 %search)

 73 | sig_alg_get_params ECDSA_SECP256r1_SHA256 = ECDSA (MkDPair Sha256 %search)

 74 | sig_alg_get_params ECDSA_SECP384r1_SHA384 = ECDSA (MkDPair Sha384 %search)

 75 | sig_alg_get_params ECDSA_SECP521r1_SHA512 = ECDSA (MkDPair Sha512 %search)

 76 | sig_alg_get_params RSA_PSS_RSAE_SHA256 = rsa_pss_params Sha256

 77 | sig_alg_get_params RSA_PSS_RSAE_SHA384 = rsa_pss_params Sha384

 78 | sig_alg_get_params RSA_PSS_RSAE_SHA512 = rsa_pss_params Sha512

 86 | public export

 87 | get_server_version : ServerHello -> TLSVersion

 88 | get_server_version hello = go hello.extensions

 89 |   where

 90 |   go : List (DPair _ ServerExtension) -> TLSVersion

 91 |   go [] = hello.version

 92 |   go ((SupportedVersions ** (SupportedVersions version)) :: xs) = version

 93 |   go (x :: xs) = go xs

 96 | public export

 97 | get_server_handshake_key : ServerHello -> Either String (SupportedGroup, List Bits8)

 98 | get_server_handshake_key hello = go hello.extensions

 99 |   where

100 |   go : List (DPair _ ServerExtension) -> Either String (SupportedGroup, List Bits8)

101 |   go [] = Left "Server did not return any handshake keys"

102 |   go ((KeyShare ** (KeyShare x)) :: xs) = Right x

103 |   go (x :: xs) = go xs

109 | public export

110 | CertificateCheck : (Type -> Type) -> Type

111 | CertificateCheck m = Certificate -> m (Either String PublicKey)

114 | public export

115 | record TLSInitialState where

116 |   constructor MkTLSInitialState

117 |   server_hostname : String

118 |   client_random : Vect 32 Bits8

119 |   session_id : List Bits8

120 |   cipher_suites : List1 CipherSuite

121 |   signature_algos : List1 SignatureAlgorithm

122 |   dh_keys : List1 (DPair SupportedGroup (\g => Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g)))

126 | record TLSClientHelloState where

127 |   constructor MkTLSClientHelloState

128 |   b_client_hello : List Bits8

129 |   client_random : Vect 32 Bits8

130 |   dh_keys : List1 (DPair SupportedGroup (\g => Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g)))

134 | data TLS3ServerHelloVerificationState : Type where

135 |   NotVerified : TLS3ServerHelloVerificationState

136 |   HasCertificate : Certificate -> TLS3ServerHelloVerificationState

137 |   Verified : TLS3ServerHelloVerificationState

141 | data TLS3ServerHelloState : (aead : Type) -> AEAD aead -> (algo : Type) -> Hash algo -> Type where

142 |   MkTLS3ServerHelloState : TLS3ServerHelloVerificationState -> (a' : AEAD a) -> (h' : Hash h) -> h ->

143 |                            HandshakeKeys (fixed_iv_length {a=a}) (enc_key_length {a=a}) -> Nat -> TLS3ServerHelloState a a' h h'

147 | data TLS3ApplicationState : (aead : Type) -> AEAD aead -> Type where

148 |   MkTLS3ApplicationState : (a' : AEAD a) -> ApplicationKeys (fixed_iv_length {a=a}) (enc_key_length {a=a}) -> Nat -> Nat -> TLS3ApplicationState a a'

152 | record TLS2ServerHelloState algo where

153 |   constructor MkTLS2ServerHelloState

154 |   client_random : Vect 32 Bits8

155 |   server_random : Vect 32 Bits8

156 |   cipher_suite  : CipherSuite

157 |   dh_keys : List1 (DPair SupportedGroup (\g => Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g)))

158 |   digest_wit : Hash algo

159 |   digest_state : algo

163 | record TLS2ServerCertificateState algo where

164 |   constructor MkTLS2ServerCertificateState

165 |   server_hello : TLS2ServerHelloState algo

166 |   certificate : Certificate

167 |   cipher_suite : CipherSuite

168 |   dh_keys : List1 (DPair SupportedGroup (\g => Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g)))

169 |   digest_wit : Hash algo

170 |   digest_state : algo

175 | data TLS2ServerKEXState : (aead : Type) -> AEAD aead -> (algo : Type) -> Hash algo -> Type where

176 |   MkTLS2ServerKEXState : (a' : AEAD a) -> (h' : Hash h) -> h -> Nat -> List Bits8 ->

177 |                          (Application2Keys (fixed_iv_length @{a'}) (enc_key_length @{a'}) (mac_key_length @{a'})) ->

178 |                          TLS2ServerKEXState a a' h h'

182 | record TLS2ServerKEXDoneState a b c d where

183 |   constructor MkTLS2ServerKEXDoneState

184 |   kex_state : TLS2ServerKEXState a b c d

190 | record TLS2AppReadyState a b c d where

191 |   constructor MkTLS2AppReadyState

192 |   kex_state : TLS2ServerKEXState a b c d

196 | data TLS2ApplicationState : (aead : Type) -> AEAD aead -> Type where

197 |   MkTLS2ApplicationState : (a' : AEAD a) -> Application2Keys (fixed_iv_length {a=a}) (enc_key_length {a=a}) (mac_key_length @{a'}) -> Nat -> Nat ->

198 |                            TLS2ApplicationState a a'

200 | public export

201 | data TLSStep : Type where

202 |   Init : TLSStep

203 |   ClientHello : TLSStep

204 |   ServerHello2 : TLSStep

205 |   ServerHello3 : TLSStep

206 |   Application3 : TLSStep

207 |   ServerCert2 : TLSStep

208 |   ServerKEX2 : TLSStep

209 |   ServerKEXDone2 : TLSStep

210 |   AppReady2 : TLSStep

211 |   Application2 : TLSStep

213 | public export

214 | data TLSState : TLSStep -> Type where

215 |   TLS_Init : TLSInitialState -> TLSState Init

216 |   TLS_ClientHello : TLSClientHelloState -> TLSState ClientHello

217 |   TLS3_ServerHello : TLS3ServerHelloState a b algo d -> TLSState ServerHello3

218 |   TLS3_Application : TLS3ApplicationState a b -> TLSState Application3

219 |   TLS2_ServerHello : TLS2ServerHelloState algo -> TLSState ServerHello2

220 |   TLS2_ServerCertificate : TLS2ServerCertificateState algo -> TLSState ServerCert2

221 |   TLS2_ServerKEX : TLS2ServerKEXState a b algo d -> TLSState ServerKEX2

222 |   TLS2_ServerKEXDone : TLS2ServerKEXDoneState a b algo d -> TLSState ServerKEXDone2

223 |   TLS2_AppReady : TLS2AppReadyState a b algo d -> TLSState AppReady2

224 |   TLS2_Application : TLS2ApplicationState a b -> TLSState Application2

226 | encode_public_keys : (g : SupportedGroup) -> Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g) ->

227 |                      (SupportedGroup, List Bits8)

228 | encode_public_keys group (sk, pk) = (group, serialize_pk @{snd $ curve_group_to_type group} pk)

232 | key_exchange : (group : SupportedGroup) ->

233 |                List Bits8 ->

234 |                List (DPair SupportedGroup (\g => Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g))) ->

235 |                Maybe (List Bits8)

236 | key_exchange group pk [] = Nothing

237 | key_exchange group pk ((group' ** (sk, _)) :: xs) =

238 |   if group == group'

239 |     then deserialize_then_dh @{snd $ curve_group_to_type group'} sk pk

240 |     else key_exchange group pk xs

243 | parse_record : List Bits8 ->

244 |                (Parserializer Bits8 (List (Posed Bits8)) (SimpleError String) (Either (AlertLevel, AlertDescription) (TLSVersion, DPair _ Record))) ->

245 |                Either String (DPair _ Record)

246 | parse_record b_input parser = do

247 |   let (Pure [] $ Right (TLS12, record')) = feed (map (uncurry MkPosed) $ enumerate Z b_input) parser.decode

248 |   | (Pure [] $ Right (tlsver, _)) => Left $ "Unsupported TLS version: " <+> show tlsver

249 |   | (Pure [] $ Left (_, alert)) => Left $ "TLS alert: " <+> show alert

250 |   | (Pure leftover _) => Left $ "Parsing error: overfed, leftover: " <+> xxd (map get leftover)

251 |   | (Fail err) => Left $ "Parsing error: " <+> show err

252 |   | _ => Left "Parsing error: underfed"

253 |   case record' of

254 |     (_ ** Alert alert) => Left $ show alert

255 |     ok => pure ok

259 | public export

260 | tls_init_to_clienthello : TLSState Init -> (List Bits8, TLSState ClientHello)

261 | tls_init_to_clienthello (TLS_Init state) =

262 |   let client_hello_object = MkClientHello

263 |         TLS12

264 |         state.client_random

265 |         state.session_id

266 |         state.cipher_suites

267 |         (singleton Null)

268 |         [ (_ ** ServerName $ DNS state.server_hostname ::: [])

269 |         , (_ ** SupportedGroups $ map fst state.dh_keys)

270 |         , (_ ** SignatureAlgorithms state.signature_algos)

271 |         , (_ ** KeyShare $ map (uncurry encode_public_keys) state.dh_keys)

272 |         , (_ ** SupportedVersions $ TLS13 ::: [ TLS12 ])

273 |         ]

274 |       b_client_hello =

275 |         (arecord {i = List (Posed Bits8)}).encode (TLS12, (_ ** Handshake [(_ ** ClientHello client_hello_object)]))

276 |   in (b_client_hello, TLS_ClientHello $ MkTLSClientHelloState (drop 5 b_client_hello) state.client_random state.dh_keys)

281 | public export

282 | tls_clienthello_to_serverhello : TLSState ClientHello -> List Bits8 ->

283 |                                  Either String (Either (TLSState ServerHello2) (TLSState ServerHello3))

284 | tls_clienthello_to_serverhello (TLS_ClientHello state) b_server_hello = do

285 |   (MkDPair _ (Handshake [MkDPair _ (ServerHello server_hello)])) <- parse_record b_server_hello alert_or_arecord

286 |   | _ => Left $ "Parsing error: record not server_hello"

287 |   case get_server_version server_hello of

288 |     TLS13 => do

289 |       let (hash_algo ** hwit) = ciphersuite_to_hash_type server_hello.cipher_suite

290 |       let digest_state = update (drop 5 b_server_hello) $ update state.b_client_hello $ init hash_algo

291 |       (group, pk) <- get_server_handshake_key server_hello

292 |       shared_secret <- maybe_to_either (key_exchange group pk $ toList state.dh_keys) "server sent invalid key"

293 |       let (aead ** awit) = ciphersuite_to_aead_type server_hello.cipher_suite

294 |       let hk = tls13_handshake_derive hash_algo (fixed_iv_length {a=aead}) (enc_key_length {a=aead}) shared_secret $ toList $ finalize digest_state

295 |       Right $ Right $ TLS3_ServerHello $ MkTLS3ServerHelloState NotVerified awit hwit digest_state hk Z

296 |     TLS12 =>

297 |       let (hash_algo ** hwit) = ciphersuite_to_prf_type server_hello.cipher_suite

298 |           digest_state = update (drop 5 b_server_hello) $ update state.b_client_hello $ init hash_algo

299 |       in Right

300 |          $ Left

301 |          $ TLS2_ServerHello

302 |          $ MkTLS2ServerHelloState state.client_random server_hello.random server_hello.cipher_suite state.dh_keys hwit digest_state

303 |     tlsvr => Left $ "unsupported version: " <+> show tlsvr

306 | decrypt_hs_s_wrapper : TLS3ServerHelloState aead aead' algo algo' -> Wrapper (mac_length @{aead'}) -> List Bits8 ->

307 |                        Maybe (TLS3ServerHelloState aead aead' algo algo', List Bits8)

308 | decrypt_hs_s_wrapper (MkTLS3ServerHelloState cert a' h' digest_state hk counter) (MkWrapper ciphertext mac_tag) record_header =

309 |   case decrypt @{a'} hk.server_handshake_key hk.server_handshake_iv zeros zeros counter ciphertext (const record_header) $ toList mac_tag of

310 |     (_, False) => Nothing

311 |     (plaintext, True) => Just (MkTLS3ServerHelloState cert a' h' digest_state hk (S counter), plaintext)

313 | list_minus : List a -> List b -> List a

314 | list_minus a b = take (length a `minus` length b) a

321 | tls3_serverhello_to_application_go : Monad m =>

322 |                                      TLSState ServerHello3 ->

323 |                                      List Bits8 ->

324 |                                      CertificateCheck m ->

325 |                                      (EitherT String m (Either (TLSState ServerHello3) (List Bits8, TLSState Application3)))

326 | tls3_serverhello_to_application_go og [] cert_ok = pure $ Left og

327 | tls3_serverhello_to_application_go og@(TLS3_ServerHello {algo} server_hello@(MkTLS3ServerHelloState cert a' h' d' hk c')) plaintext cert_ok =

328 |   case feed (map (uncurry MkPosed) $ enumerate Z plaintext) handshake.decode of

329 |     -- since we do not support any encrypted extensions, it is ignored

330 |     Pure leftover (_ ** EncryptedExtensions x) =>

331 |       --- pass the plaintext bytes representing the record into the digest

332 |       let consumed = plaintext `list_minus` leftover

333 |           new = TLS3_ServerHello $ MkTLS3ServerHelloState cert a' h' (update consumed d') hk c'

334 |       in tls3_serverhello_to_application_go new (map get leftover) cert_ok

335 |     -- handle the server's certificate

336 |     Pure leftover (_ ** Certificate x) =>

337 |       case cert of

338 |         HasCertificate _ => throwE "Certificate was sent twice"

339 |         Verified => throwE "Certificate was sent after verification"

340 |         NotVerified => do

341 |           --- pass the plaintext bytes representing the record into the digest

342 |           let consumed = plaintext `list_minus` leftover

343 |           let new = TLS3_ServerHello $ MkTLS3ServerHelloState (HasCertificate x) a' h' (update consumed d') hk c'

344 |           tls3_serverhello_to_application_go new (map get leftover) cert_ok

345 |     -- handle the server's signature of a digest of all the handshake records received so far, signed by the server's certificate

346 |     Pure leftover (_ ** CertificateVerify x) => do

347 |       certificate' <- case cert of

348 |         NotVerified => throwE "CertificateVerify sent before Certificate"

349 |         Verified => throwE "CertificateVerify sent after verification"

350 |         HasCertificate cert => pure cert

351 |       let verify_token =

352 |             replicate 64 0x20 -- 64 spaces

353 |               <+> string_to_ascii "TLS 1.3, server CertificateVerify"

354 |               <+> [ 0x00 ] -- null

355 |               <+> toList (finalize d')

356 |       public_key <- MkEitherT $ cert_ok certificate'

357 |       let Right () = verify_signature (sig_alg_get_params x.signature_algorithm) public_key verify_token x.signature

358 |       | Left err => throwE $ "error while verifying handshake: " <+> err

359 |       let consumed = plaintext `list_minus` leftover

360 |       let new = TLS3_ServerHello $ MkTLS3ServerHelloState Verified a' h' (update consumed d') hk c'

361 |       tls3_serverhello_to_application_go new (map get leftover) cert_ok

362 |     -- handle the Finished record which contains a hash of all the handshake records received so far

363 |     Pure [] (_ ** Finished x) =>

364 |       case cert of

365 |         Verified =>

366 |           if (tls13_verify_data algo hk.server_traffic_secret $ toList $ finalize d') == verify_data x

367 |           then

368 |             let digest = update plaintext d'

369 |                 client_verify_data = tls13_verify_data algo hk.client_traffic_secret $ toList $ finalize digest

370 |                 client_handshake_finished =

371 |                   to_application_data

372 |                   $ MkWrappedRecord Handshake ((with_id no_id_finished).encode {i = List (Posed Bits8)}

373 |                   $ Finished

374 |                   $ MkFinished client_verify_data)

375 |                 record_length = (length client_handshake_finished) + mac_length @{a'}

376 |                 b_record = record_type_with_version_with_length.encode {i = List (Posed Bits8)} (ApplicationData, TLS12, record_length)

377 |                 (eiv, chf_encrypted, chf_mac_tag) =

378 |                   encrypt @{a'} hk.client_handshake_key hk.client_handshake_iv zeros Z client_handshake_finished b_record

379 |                 app_key = tls13_application_derive algo hk (toList $ finalize digest)

380 |                 verify_data_wrapped = MkWrapper chf_encrypted chf_mac_tag

381 |                 b_chf_wrapped =

382 |                   (arecord {i = List (Posed Bits8)}).encode (TLS12, MkDPair _ (ApplicationData $ to_application_data $ MkWrapper chf_encrypted chf_mac_tag))

383 |             in pure $ Right (b_chf_wrapped, TLS3_Application $ MkTLS3ApplicationState a' app_key Z Z)

384 |           else

385 |             throwE "verify data does not match"

386 |         _ => throwE "CertificateVerify was not sent"

387 |     Fail err => throwE $ "body: " <+> xxd plaintext <+> "\nbody length: " <+> (show $ length plaintext) <+> "\nparsing error: " <+> show err

388 |     _ => throwE "failed to parse plaintext"

393 | public export

394 | tls3_serverhello_to_application : Monad m => TLSState ServerHello3 -> List Bits8 -> CertificateCheck m ->

395 |                                               m (Either String (Either (TLSState ServerHello3) (List Bits8, TLSState Application3)))

396 | tls3_serverhello_to_application og@(TLS3_ServerHello server_hello@(MkTLS3ServerHelloState cert a' h' d' hk c')) b_wrapper cert_ok = runEitherT $ do

397 |   let Right (MkDPair _ (ApplicationData application_data)) = parse_record b_wrapper alert_or_arecord

398 |   | Right (MkDPair _ (ChangeCipherSpec _)) => pure $ Left og

399 |   | Left err => throwE err

400 |   | _ => throwE $ "Parsing error: record not application data"

401 |   let Just wrapper = from_application_data {mac_size = (mac_length @{a'})} application_data

402 |   | Nothing => throwE $ "malformed wrapper:" <+> xxd application_data

403 |   let Just (server_hello, plaintext') = decrypt_hs_s_wrapper server_hello wrapper (take 5 b_wrapper)

404 |   | Nothing => throwE "cannot decrypt wrapper"

405 |   let Just (plaintext, 0x16) = uncons1 <$> toList1' plaintext'

406 |   | Just ([_, alert], 0x15) => throwE $ "alert: " <+> (show $ id_to_alert_description alert)

407 |   | Just (plaintext, i) => throwE $ "invalid record id: " <+> show i <+> " body: " <+> xxd plaintext

408 |   | Nothing => throwE "plaintext is empty"

409 |   tls3_serverhello_to_application_go (TLS3_ServerHello server_hello) plaintext cert_ok

412 | decrypt_ap_s_wrapper : TLS3ApplicationState aead aead' -> Wrapper (mac_length @{aead'}) -> List Bits8 ->

413 |                        Maybe (TLS3ApplicationState aead aead', List Bits8)

414 | decrypt_ap_s_wrapper (MkTLS3ApplicationState a' ak c_counter s_counter) (MkWrapper ciphertext mac_tag) record_header =

415 |   case decrypt @{a'} ak.server_application_key ak.server_application_iv zeros zeros s_counter ciphertext (const record_header) $ toList mac_tag of

416 |      (_, False) => Nothing

417 |      (plaintext, True) => Just (MkTLS3ApplicationState a' ak c_counter (S s_counter), plaintext)

420 | public export

421 | decrypt_from_record : TLSState Application3 -> List Bits8 -> Either String (TLSState Application3, List Bits8)

422 | decrypt_from_record og@(TLS3_Application app_state@(MkTLS3ApplicationState a' ak c_counter s_counter)) b_wrapper = do

423 |   (MkDPair _ (ApplicationData application_data)) <- parse_record b_wrapper alert_or_arecord

424 |   | _ => Left $ "Parsing error: record not application data"

425 |   let Just wrapper = from_application_data {mac_size = (mac_length @{a'})} application_data

426 |   | Nothing => Left $ "malformed wrapper:" <+> xxd application_data

427 |   let Just (app_state, plaintext') = decrypt_ap_s_wrapper app_state wrapper (take 5 b_wrapper)

428 |   | Nothing => Left "cannot decrypt wrapper"

429 |   let Just (plaintext, 0x17) = uncons1 <$> toList1' plaintext'

430 |   | Just (plaintext, 0x16) => Right (TLS3_Application app_state, []) -- implement session ticket in the future?

431 |   | Just ([_, alert], 0x15) => Left $ "alert: " <+> (show $ id_to_alert_description alert)

432 |   | Just (plaintext, i) => Left $ "invalid record id: " <+> show i <+> " body: " <+> xxd plaintext

433 |   | Nothing => Left "plaintext is empty"

434 |   Right (TLS3_Application app_state, plaintext)

437 | public export

438 | encrypt_to_record : TLSState Application3 -> List Bits8 -> (TLSState Application3, List Bits8)

439 | encrypt_to_record (TLS3_Application $ MkTLS3ApplicationState a' ak c_counter s_counter) plaintext =

440 |   let b_application_data = to_application_data $ MkWrappedRecord ApplicationData plaintext

441 |       record_length = (length b_application_data) + mac_length @{a'}

442 |       b_record_header = (record_type_with_version_with_length {i = List (Posed Bits8)}).encode (ApplicationData, TLS12, record_length)

443 |       (eiv, app_encrypted, app_mac_tag) =

444 |         encrypt @{a'} ak.client_application_key ak.client_application_iv zeros c_counter b_application_data b_record_header

445 |       b_app_wrapped =

446 |         arecord.encode {i = List (Posed Bits8)} (TLS12, MkDPair _ (ApplicationData $ to_application_data $ MkWrapper app_encrypted app_mac_tag))

447 |   in (TLS3_Application $ MkTLS3ApplicationState a' ak (S c_counter) s_counter, b_app_wrapped)

450 | public export

451 | serverhello2_to_servercert : TLSState ServerHello2 -> List Bits8 -> Either String (TLSState ServerCert2)

452 | serverhello2_to_servercert (TLS2_ServerHello server_hello) b_cert = do

453 |   (MkDPair _ (Handshake [MkDPair _ (Certificate server_cert)])) <- parse_record b_cert alert_or_arecord2

454 |   | _ => Left "Parsing error: record not server_hello"

455 |   pure $ TLS2_ServerCertificate

456 |        $ MkTLS2ServerCertificateState

457 |            server_hello

458 |            server_cert

459 |            server_hello.cipher_suite

460 |            server_hello.dh_keys

461 |            server_hello.digest_wit

462 |            (update @{hash_to_digest server_hello.digest_wit} (drop 5 b_cert) server_hello.digest_state)

467 | public export

468 | servercert_to_serverkex : Monad m => TLSState ServerCert2 -> List Bits8 -> CertificateCheck m -> m (Either String (TLSState ServerKEX2))

469 | servercert_to_serverkex (TLS2_ServerCertificate server_cert) b_kex cert_ok = runEitherT $ do

470 |   let Right (MkDPair _ (Handshake [MkDPair _ (ServerKeyExchange server_kex)])) = parse_record b_kex alert_or_arecord2

471 |   | _ => throwE "Parsing error: record not server_hello"

472 |   let Just shared_secret = key_exchange (server_kex.server_pk_group) (server_kex.server_pk_body) (toList server_cert.dh_keys)

473 |   | Nothing => throwE "cannot parse server public key"

474 |   let (aead ** awit) = ciphersuite_to_aead_type server_cert.cipher_suite

475 |   let app_key =

476 |         tls12_application_derive server_cert.digest_wit

477 |           (fixed_iv_length {a=aead})

478 |           (enc_key_length {a=aead})

479 |           (mac_key_length {a=aead})

480 |           shared_secret

481 |           (toList server_cert.server_hello.client_random)

482 |           (toList server_cert.server_hello.server_random)

483 |   let Just (_, chosen_pk) = find (\(g,_) => g == server_kex.server_pk_group) $ toList $ map (uncurry encode_public_keys) server_cert.dh_keys

484 |   | Nothing => throwE "cannot find public key that match the server's"

485 |   let (curve_info_a, curve_info_b) = supported_group_to_id server_kex.server_pk_group

486 |   let verify_token =

487 |         toList server_cert.server_hello.client_random

488 |         <+> toList server_cert.server_hello.server_random

489 |         <+> [ 0x03, curve_info_a, curve_info_b, cast (length server_kex.server_pk_body) ] -- 0x03 hard coded, value for "named curve"

490 |         <+> server_kex.server_pk_body

491 |   public_key <- MkEitherT $ cert_ok server_cert.certificate

492 |   let Right () = verify_signature (sig_alg_get_params server_kex.signature_algo) public_key verify_token server_kex.signature_body

493 |   | Left err => throwE $ "error while verifying handshake: " <+> err

494 |   pure $ TLS2_ServerKEX

495 |        $ MkTLS2ServerKEXState

496 |            awit

497 |            server_cert.digest_wit

498 |            (update @{hash_to_digest server_cert.digest_wit} (drop 5 b_kex) server_cert.digest_state)

499 |            (ciphersuite_to_verify_data_len server_cert.cipher_suite)

500 |            chosen_pk

501 |            app_key

504 | encrypt_to_wrapper2 : AEAD a => Vect (enc_key_length {a=a}) Bits8 -> Vect (fixed_iv_length {a=a}) Bits8 -> Vect (mac_key_length {a=a}) Bits8 ->

505 |                       List Bits8 -> RecordType -> Nat -> List Bits8

506 | encrypt_to_wrapper2 key iv mac_key plaintext record_id sequence =

507 |   let aad =

508 |         (toList $ to_be {n=8} (cast {to=Bits64} sequence))

509 |         <+> [record_type_to_id record_id, 0x03, 0x03] -- 0x03 0x03 is the byte representation of TLS 1.2

510 |         <+> (toList $ to_be {n=2} (cast {to=Bits16} $ length plaintext))

511 |       (eiv, ciphertext, mac) = encrypt key iv mac_key sequence plaintext aad

512 |       wrapper = MkWrapper2 eiv ciphertext mac

513 |       b_wrapper = (wrapper2 {i = List (Posed Bits8)}).encode (record_id, TLS12, wrapper)

514 |   in b_wrapper

519 | public export

520 | serverkex_process_serverhellodone : TLSState ServerKEX2 -> List Bits8 -> Either String (TLSState ServerKEXDone2, List Bits8)

521 | serverkex_process_serverhellodone og@(TLS2_ServerKEX (MkTLS2ServerKEXState a' h' digest_state vdlen chosen_pk app_key)) b_hello_done = do

522 |   (MkDPair _ (Handshake [MkDPair _ (ServerHelloDone _)])) <- parse_record b_hello_done alert_or_arecord2

523 |   | _ => Left $ "Parsing error: record not server_hello"

524 |   let b_client_kex =

525 |         (arecord {i = List (Posed Bits8)}).encode (TLS12, (_ ** Handshake [(_ ** ClientKeyExchange $ MkClientKeyExchange chosen_pk)]))

526 |   let b_client_change_cipher_spec =

527 |         (arecord {i = List (Posed Bits8)}).encode (TLS12, (_ ** ChangeCipherSpec [0x01]))

528 |   let digest_state =

529 |         update (drop 5 b_client_kex) $ update (drop 5 b_hello_done) digest_state

530 |   let client_verify_data = (with_id no_id_finished).encode {i = List (Posed Bits8)}

531 |         $ Finished

532 |         $ MkFinished

533 |         $ toList

534 |         (tls12_client_verify_data h' vdlen (toList app_key.master_secret) (toList $ finalize digest_state))

535 |   let b_client_verify_data =

536 |         encrypt_to_wrapper2 app_key.client_application_key app_key.client_application_iv app_key.client_mac_key client_verify_data Handshake Z

537 |   let digest_state =

538 |         update client_verify_data digest_state

539 |   Right (TLS2_ServerKEXDone $ MkTLS2ServerKEXDoneState $ MkTLS2ServerKEXState a' h' digest_state vdlen chosen_pk app_key

540 |         , b_client_kex <+> b_client_change_cipher_spec <+> b_client_verify_data)

543 | public export

544 | serverhellodone_to_applicationready2 : TLSState ServerKEXDone2 -> List Bits8 -> Either String (TLSState AppReady2)

545 | serverhellodone_to_applicationready2 (TLS2_ServerKEXDone state) b_changecipherspec = do

546 |   (MkDPair _ (ChangeCipherSpec _)) <- parse_record b_changecipherspec alert_or_arecord2

547 |   | _ => Left $ "Parsing error: record not ChangeCipherSpec"

548 |   pure $ TLS2_AppReady $ MkTLS2AppReadyState state.kex_state

551 | parse_tls12_wrapper : AEAD a => RecordType -> List Bits8 -> Either String (Wrapper2 (record_iv_length {a=a}) (mac_length {a=a}))

552 | parse_tls12_wrapper recordtype b_input = do

553 |   let (Pure [] (recordtype', TLS12, record')) = feed (map (uncurry MkPosed) $ enumerate Z b_input) (wrapper2 {i = List (Posed Bits8)}).decode

554 |   | (Pure [] (_, tlsver, _)) => Left $ "Unsupported TLS version: " <+> show tlsver

555 |   | (Pure leftover _) => Left $ "Parsing error: overfed, leftover: " <+> xxd (map get leftover)

556 |   | (Fail err) => Left $ "Parsing error: " <+> show err

557 |   | _ => Left "Parsing error: underfed"

558 |   if recordtype == recordtype'

559 |      then pure record'

560 |      else Left $ "expected record type: " <+> show recordtype <+> ", but got: " <+> show recordtype'

563 | decrypt_from_wrapper2 : AEAD a =>

564 |                         Nat ->

565 |                         RecordType ->

566 |                         Wrapper2 (record_iv_length {a=a}) (mac_length {a=a}) ->

567 |                         Vect (fixed_iv_length {a=a}) Bits8 ->

568 |                         Vect (enc_key_length {a=a}) Bits8 ->

569 |                         Vect (mac_key_length {a=a}) Bits8 ->

570 |                         Either String (List Bits8)

571 | decrypt_from_wrapper2 sequence record_type wrapper iv key mac_key =

572 |   let aadf = (\plaintext =>

573 |         (toList $ to_be {n=8} (cast {to=Bits64} sequence))

574 |         <+> [record_type_to_id record_type, 0x03, 0x03] -- 0x03 0x03 is the byte representation of TLS 1.2

575 |         <+> (toList $ to_be {n=2} (cast {to=Bits16} $ length plaintext)))

576 |       (plaintext, ok) = decrypt key iv wrapper.iv_data mac_key sequence wrapper.encrypted_data aadf (toList wrapper.auth_tag)

577 |   in if ok then Right $ plaintext else Left "cannot decrypt wrapper"

581 | public export

582 | applicationready2_to_application2 : TLSState AppReady2 -> List Bits8 -> Either String (TLSState Application2)

583 | applicationready2_to_application2 (TLS2_AppReady state) b_verifydata = do

584 |   let (MkTLS2ServerKEXState a' h' digest_state vdlen chosen_pk app_key) = state.kex_state

585 |   wrapper <- parse_tls12_wrapper @{a'} Handshake b_verifydata

586 |   plaintext <-

587 |     decrypt_from_wrapper2 Z Handshake wrapper app_key.server_application_iv app_key.server_application_key app_key.server_mac_key

588 |   let result = feed (map (uncurry MkPosed) $ enumerate Z plaintext) $ (with_id no_id_finished).decode {i = List (Posed Bits8)}

589 |   let (Pure [] (Finished $ MkFinished verify_data')) = result

590 |   | _ => Left $ "Parsing error: decrypted record not Finished"

591 |   let verify_data = tls12_server_verify_data h' vdlen (toList app_key.master_secret) (toList $ finalize digest_state)

592 |   maybe_to_either (guard $ toList verify_data `s_eq'` toList verify_data') "Verify data not match"

593 |   pure $ TLS2_Application $ MkTLS2ApplicationState a' app_key 1 1

596 | public export

597 | encrypt_to_record2 : TLSState Application2 -> List Bits8 -> (TLSState Application2, List Bits8)

598 | encrypt_to_record2 (TLS2_Application $ MkTLS2ApplicationState a' ak c_counter s_counter) plaintext =

599 |    let b_wrapper = encrypt_to_wrapper2 ak.client_application_key ak.client_application_iv ak.client_mac_key plaintext ApplicationData c_counter

600 |    in (TLS2_Application $ MkTLS2ApplicationState a' ak (S c_counter) s_counter, b_wrapper)

603 | public export

604 | decrypt_from_record2 : TLSState Application2 -> List Bits8 -> Either String (TLSState Application2, List Bits8)

605 | decrypt_from_record2 (TLS2_Application $ MkTLS2ApplicationState a' ak c_counter s_counter) ciphertext = do

606 |   wrapper <- parse_tls12_wrapper @{a'} ApplicationData ciphertext

607 |   plaintext <- decrypt_from_wrapper2 s_counter ApplicationData wrapper ak.server_application_iv ak.server_application_key ak.server_mac_key

608 |   Right (TLS2_Application $ MkTLS2ApplicationState a' ak c_counter (S s_counter), plaintext)