
   0 | module Network.TLS.Record
   1 | 
   2 | import Utils.Bytes
   3 | import Utils.Misc
   4 | import Utils.Show
   5 | import Data.Vect
   6 | import public Network.TLS.HelloExtension
   7 | import public Network.TLS.Handshake
   8 | import public Network.TLS.Magic
   9 | import public Network.TLS.Parsing
  10 | import public Network.TLS.Wrapper
  11 | 
  12 | public export
  13 | data Record : RecordType -> Type where
  14 |   ChangeCipherSpec : (body : List Bits8) -> Record ChangeCipherSpec
  15 |   Handshake : (handshakes : List (DPair _ Handshake)) -> Record Handshake
  16 |   ApplicationData : (body : List Bits8) -> Record ApplicationData
  17 |   Alert : (AlertLevel, AlertDescription) -> Record Alert
  18 | 
  19 | public export
  20 | Show (Record type) where
  21 |   show (ChangeCipherSpec body) = show_record "ChangeCipherSpec"
  22 |     [ ("body", xxd body)
  23 |     ]
  24 |   show (Handshake handshakes) = show_record "Handshake"
  25 |     [ ("handshakes", show (map (\x => show x.snd) handshakes))
  26 |     ]
  27 |   show (ApplicationData body) = show_record "ApplicationData"
  28 |     [ ("body", xxd body)
  29 |     ]
  30 |   show (Alert (lvl, desc)) = show_record "Alert"
  31 |     [ ("alert_level", show lvl)
  32 |     , ("alert", show desc)
  33 |     ]
  34 | 
  35 | XRecord : Type
  36 | XRecord = Eithers [Record ChangeCipherSpec, Record Handshake, Record ApplicationData, Record Alert]
  37 | 
  38 | hack_record : DPair _ Record -> XRecord
  39 | hack_record (ChangeCipherSpec ** x) = Left x
  40 | hack_record (Handshake ** x)        = Right (Left x)
  41 | hack_record (ApplicationData  ** x) = Right (Right (Left x))
  42 | hack_record (Alert ** x)            = Right (Right (Right x))
  43 | 
  44 | fix_record : XRecord -> DPair _ Record
  45 | fix_record (Left x)                  = (ChangeCipherSpec ** x)
  46 | fix_record (Right (Left x))          = (Handshake ** x)
  47 | fix_record (Right (Right (Left x)))  = (ApplicationData ** x)
  48 | fix_record (Right (Right (Right x))) = (Alert ** x)
  49 | 
  50 | XRecordWithVersion : Type
  51 | XRecordWithVersion = Eithers
  52 |   [ (TLSVersion, Record ChangeCipherSpec)
  53 |   , (TLSVersion, Record Handshake)
  54 |   , (TLSVersion, Record ApplicationData)
  55 |   , (TLSVersion, Record Alert)
  56 |   ]
  57 | 
  58 | hack_record_with_version : (TLSVersion, DPair _ Record) -> XRecordWithVersion
  59 | hack_record_with_version (v, (ChangeCipherSpec ** x)) = Left (v, x)
  60 | hack_record_with_version (v, (Handshake ** x))        = Right (Left (v, x))
  61 | hack_record_with_version (v, (ApplicationData  ** x)) = Right (Right (Left (v, x)))
  62 | hack_record_with_version (v, (Alert ** x))            = Right (Right (Right (v, x)))
  63 | 
  64 | fix_record_with_version : XRecordWithVersion -> (TLSVersion, DPair _ Record)
  65 | fix_record_with_version (Left (v, x))                  = (v, (ChangeCipherSpec ** x))
  66 | fix_record_with_version (Right (Left (v, x)))          = (v, (Handshake ** x))
  67 | fix_record_with_version (Right (Right (Left (v, x))))  = (v, (ApplicationData ** x))
  68 | fix_record_with_version (Right (Right (Right (v, x)))) = (v, (Alert ** x))
  69 | 
  70 | namespace Parsing
  71 |   export
  72 |   no_id_change_cipher_spec : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Record ChangeCipherSpec)
  73 |   no_id_change_cipher_spec = map (\a => ChangeCipherSpec a) (\(ChangeCipherSpec a) => a)
  74 |     $ lengthed_list 2 token
  75 | 
  76 |   export
  77 |   no_id_handshake : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Record Handshake)
  78 |   no_id_handshake = map (\a => Handshake a) (\(Handshake a) => a)
  79 |     $ lengthed_list 2 handshake
  80 | 
  81 |   export
  82 |   no_id_handshake2 : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Record Handshake)
  83 |   no_id_handshake2 = map (\a => Handshake a) (\(Handshake a) => a)
  84 |     $ lengthed_list 2 handshake2
  85 | 
  86 |   export
  87 |   no_id_application_data : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Record ApplicationData)
  88 |   no_id_application_data = map (\a => ApplicationData a) (\(ApplicationData a) => a)
  89 |     $ lengthed_list 2 token
  90 | 
  91 |   export
  92 |   record_type_with_version : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (RecordType, TLSVersion)
  93 |   record_type_with_version = record_type <*>> tls_version
  94 | 
  95 |   export
  96 |   record_type_with_version_with_length : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (RecordType, TLSVersion, Nat)
  97 |   record_type_with_version_with_length = record_type <*>> tls_version <*>> nat 2
  98 | 
  99 |   export
 100 |   alert : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (AlertLevel, AlertDescription)
 101 |   alert = under "alert protocol" $ alert_level <*>> alert_description
 102 | 
 103 |   export
 104 |   no_id_alert : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Record Alert)
 105 |   no_id_alert = map (\((), a) => Alert a) (\(Alert a) => ((), a)) $ is [0x00, 0x02] <*>> alert
 106 | 
 107 |   export
 108 |   with_id_with_version : (Cons (Posed Bits8) i, Monoid i) => {type : RecordType} -> Parserializer Bits8 i (SimpleError String) (Record type) -> Parserializer Bits8 i (SimpleError String) (TLSVersion, Record type)
 109 |   with_id_with_version pser = under (show type <+> " record") $ is (to_vect $ record_type_to_id type) *> (tls_version <*>> pser)
 110 | 
 111 |   export
 112 |   arecord : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (TLSVersion, DPair _ Record)
 113 |   arecord =
 114 |     map fix_record_with_version hack_record_with_version
 115 |     $ (with_id_with_version no_id_change_cipher_spec)
 116 |     <|> (with_id_with_version no_id_handshake)
 117 |     <|> (with_id_with_version no_id_application_data)
 118 |     <|> (with_id_with_version no_id_alert)
 119 | 
 120 |   export
 121 |   arecord2 : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (TLSVersion, DPair _ Record)
 122 |   arecord2 =
 123 |     map fix_record_with_version hack_record_with_version
 124 |     $ (with_id_with_version no_id_change_cipher_spec)
 125 |     <|> (with_id_with_version no_id_handshake2)
 126 |     <|> (with_id_with_version no_id_application_data)
 127 |     <|> (with_id_with_version no_id_alert)
 128 | 
 129 |   export
 130 |   alert_or_arecord : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Either (AlertLevel, AlertDescription) (TLSVersion, DPair _ Record))
 131 |   alert_or_arecord = alert <|> arecord
 132 | 
 133 |   export
 134 |   alert_or_arecord2 : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Either (AlertLevel, AlertDescription) (TLSVersion, DPair _ Record))
 135 |   alert_or_arecord2 = alert <|> arecord2
 136 | 
 137 |   export
 138 |   wrapper2 : (Cons (Posed Bits8) i, Monoid i) => {iv_size : Nat} -> {mac_size : Nat} -> Parserializer Bits8 i (SimpleError String) (RecordType, TLSVersion, Wrapper2 iv_size mac_size)
 139 |   wrapper2 =
 140 |     record_type
 141 |     <*>> tls_version
 142 |     <*>> (mapEither (\x => maybe_to_either (from_application_data2 x) (msg "cannot parse wrapper")) to_application_data2 $ lengthed_list 2 token)
 143 |