
  0 | module Network.TLS.Wrapper
  1 | 
  2 | import Data.Nat
  3 | import Utils.Misc
  4 | import Data.Vect
  5 | import Data.List
  6 | import Network.TLS.Magic
  7 | 
  8 | public export
  9 | record Wrapper (mac_size : Nat) where
 10 |   constructor MkWrapper
 11 |   encrypted_data : List Bits8
 12 |   auth_tag : Vect mac_size Bits8
 13 | 
 14 | public export
 15 | to_application_data : Wrapper mac_size -> List Bits8
 16 | to_application_data x = x.encrypted_data <+> toList x.auth_tag
 17 | 
 18 | public export
 19 | from_application_data : {mac_size : _} -> (application_data : List Bits8) -> Maybe (Wrapper mac_size)
 20 | from_application_data xs =
 21 |   let xs' = fromList xs in
 22 |   case isLTE mac_size (length xs) of
 23 |     Yes prf =>
 24 |       let
 25 |         (encrypted_data, auth_tag) = splitAt (minus (length xs) mac_size) $ replace_vect (sym $ plusMinusLte _ _ prf) xs'
 26 |       in
 27 |         Just $ MkWrapper (toList encrypted_data) auth_tag
 28 |     No contra => Nothing
 29 | 
 30 | public export
 31 | record Wrapper2 (iv_size : Nat) (mac_size : Nat) where
 32 |   constructor MkWrapper2
 33 |   iv_data : Vect iv_size Bits8
 34 |   encrypted_data : List Bits8
 35 |   auth_tag : Vect mac_size Bits8
 36 | 
 37 | public export
 38 | to_application_data2 : Wrapper2 iv_size mac_size -> List Bits8
 39 | to_application_data2 x = toList x.iv_data <+> x.encrypted_data <+> toList x.auth_tag
 40 | 
 41 | public export
 42 | from_application_data2 : {iv_size : _} -> {mac_size : _} -> (application_data : List Bits8) -> Maybe (Wrapper2 iv_size mac_size)
 43 | from_application_data2 xs = do
 44 |   let (iv, ciphertext) = splitAt iv_size xs
 45 |   iv' <- exactLength iv_size $ fromList iv
 46 |   w <- from_application_data ciphertext
 47 |   pure $ MkWrapper2 iv' w.encrypted_data w.auth_tag
 48 | 
 49 | namespace WrappedRecord
 50 |   public export
 51 |   record WrappedRecord where
 52 |     constructor MkWrappedRecord
 53 |     record_type : RecordType
 54 |     wrapped_data : List Bits8
 55 | 
 56 |   public export
 57 |   to_application_data : WrappedRecord -> List Bits8
 58 |   to_application_data x = x.wrapped_data <+> [record_type_to_id x.record_type]
 59 |