0 | module Network.TLS.HelloExtension
  1 |
  2 | import Data.List1
  3 | import Data.Vect
  4 | import Network.TLS.Magic
  5 | import Network.TLS.Parsing
  6 | import Utils.Bytes
  7 | import Utils.Misc
  8 | import Utils.Show
  9 |
 10 | public export
 11 | KeyBytes : Type
 12 | KeyBytes = List Bits8
 13 |
 14 | -- TODO: even more stuff
 15 | public export
 16 | data ServerNameEntry : Type where
 17 |   DNS : String -> ServerNameEntry
 18 |
 19 | public export
 20 | Show ServerNameEntry where
 21 |   show (DNS x) = show_record "DNS" [("name", show x)]
 22 |
 23 | XServerNameEntry : Type
 24 | XServerNameEntry = Eithers [String]
 25 |
 26 | hack_server_name_entry : ServerNameEntry -> XServerNameEntry
 27 | hack_server_name_entry (DNS x) = x
 28 |
 29 | fix_server_name_entry : XServerNameEntry -> ServerNameEntry
 30 | fix_server_name_entry x = (DNS x)
 31 |
 32 | namespace ClientExtension
 33 |   public export
 34 |   data ClientExtension : ExtensionType -> Type where
 35 |     ServerName : List1 ServerNameEntry -> ClientExtension ServerName
 36 |     SupportedGroups : List1 SupportedGroup -> ClientExtension SupportedGroups
 37 |     SignatureAlgorithms : List1 SignatureAlgorithm -> ClientExtension SignatureAlgorithms
 38 |     SupportedVersions : List1 TLSVersion -> ClientExtension SupportedVersions
 39 |     KeyShare : List1 (SupportedGroup, KeyBytes) -> ClientExtension KeyShare
 40 |     -- TODO: PSK
 41 |
 42 |   public export
 43 |   Show (ClientExtension type) where
 44 |     show (ServerName entries) = show_record "ServerName" [("entries", show entries)]
 45 |     show (SupportedGroups entries) = show_record "SupportedGroups" [("entries", show entries)]
 46 |     show (SignatureAlgorithms entries) = show_record "SignatureAlgorithms" [("entries", show entries)]
 47 |     show (SupportedVersions entries) = show_record "SupportedVersions" [("entries", show entries)]
 48 |     show (KeyShare entries) = show_record "KeyShare" [("entries", show entries)]
 49 |
 50 | XClientExtension : Type
 51 | XClientExtension = Eithers
 52 |   [ ClientExtension ServerName
 53 |   , ClientExtension SupportedGroups
 54 |   , ClientExtension SignatureAlgorithms
 55 |   , ClientExtension SupportedVersions
 56 |   , ClientExtension KeyShare
 57 |   ]
 58 |
 59 | hack_client_extension : DPair _ ClientExtension -> XClientExtension
 60 | hack_client_extension (ServerName ** x) = Left x
 61 | hack_client_extension (SupportedGroups ** x) = Right (Left x)
 62 | hack_client_extension (SignatureAlgorithms ** x) = Right (Right (Left x))
 63 | hack_client_extension (SupportedVersions ** x) = Right (Right (Right (Left x)))
 64 | hack_client_extension (KeyShare ** x) = Right (Right (Right (Right x)))
 65 |
 66 | fix_client_extension : XClientExtension -> DPair _ ClientExtension
 67 | fix_client_extension (Left x) = (_ ** x)
 68 | fix_client_extension (Right (Left x)) = (_ ** x)
 69 | fix_client_extension (Right (Right (Left x))) = (_ ** x)
 70 | fix_client_extension (Right (Right (Right (Left x)))) = (_ ** x)
 71 | fix_client_extension (Right (Right (Right (Right x)))) = (_ ** x)
 72 |
 73 | namespace ServerExtension
 74 |   public export
 75 |   data ServerExtension : ExtensionType -> Type where
 76 |     SupportedGroups : SupportedGroup -> ServerExtension SupportedGroups
 77 |     SignatureAlgorithms : SignatureAlgorithm -> ServerExtension SignatureAlgorithms
 78 |     SupportedVersions : TLSVersion -> ServerExtension SupportedVersions
 79 |     KeyShare : (SupportedGroup, KeyBytes) -> ServerExtension KeyShare
 80 |     Unknown : (id : (Bits8, Bits8)) -> List Bits8 -> ServerExtension (Unknown id)
 81 |
 82 |   public export
 83 |   Show (ServerExtension type) where
 84 |     show (SupportedGroups entries) = show_record "SupportedGroups" [("entry", show entries)]
 85 |     show (SignatureAlgorithms entries) = show_record "SignatureAlgorithms" [("entry", show entries)]
 86 |     show (SupportedVersions entries) = show_record "SupportedVersions" [("entry", show entries)]
 87 |     show (KeyShare entries) = show_record "KeyShare" [("entry", show entries)]
 88 |     show (Unknown (a, b) body) = show_record "Unknown" [("id", xxd $ the (List Bits8) [a, b]), ("body", xxd body)]
 89 |
 90 | XServerExtension : Type
 91 | XServerExtension = Eithers
 92 |   [ ServerExtension SupportedGroups
 93 |   , ServerExtension SignatureAlgorithms
 94 |   , ServerExtension SupportedVersions
 95 |   , ServerExtension KeyShare
 96 |   , (a ** ServerExtension (Unknown a))
 97 |   ]
 98 |
 99 | hack_server_extension : DPair _ ServerExtension -> XServerExtension
100 | hack_server_extension (SupportedGroups ** x)     = Left x
101 | hack_server_extension (SignatureAlgorithms ** x) = Right (Left x)
102 | hack_server_extension (SupportedVersions ** x)   = Right (Right (Left x))
103 | hack_server_extension (KeyShare ** x)            = Right (Right (Right (Left x)))
104 | hack_server_extension ((Unknown id) ** x)        = Right (Right (Right (Right (id ** x))))
105 |
106 | fix_server_extension : XServerExtension -> DPair _ ServerExtension
107 | fix_server_extension (Left x) = (_ ** x)
108 | fix_server_extension (Right (Left x)) = (_ ** x)
109 | fix_server_extension (Right (Right (Left x))) = (_ ** x)
110 | fix_server_extension (Right (Right (Right (Left x)))) = (_ ** x)
111 | fix_server_extension (Right (Right (Right (Right (x ** y))))) = (_ ** y)
112 |
113 | namespace Parsing
114 |   namespace Client
115 |     export
116 |     with_id : (Cons (Posed Bits8) i, Monoid i) => {type : ExtensionType} -> Parserializer Bits8 i (SimpleError String) (ClientExtension type) -> Parserializer Bits8 i (SimpleError String) (ClientExtension type)
117 |     with_id pser = under (show type <+> " extension") $ is (pair_to_vect $ extension_type_to_id type) *> pser
118 |
119 |     -- TODO: generalize
120 |     export
121 |     server_name_dns_entry : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) String
122 |     server_name_dns_entry = is [0x00] *> map ascii_to_string string_to_ascii (lengthed_list 2 token)
123 |
124 |     export
125 |     server_name_entry : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) ServerNameEntry
126 |     server_name_entry = map fix_server_name_entry hack_server_name_entry $ server_name_dns_entry
127 |
128 |     export
129 |     no_id_server_name : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ClientExtension ServerName)
130 |     no_id_server_name = lengthed 2 $ map ServerName (\(ServerName x) => x) $ lengthed_list1 2 server_name_entry
131 |
132 |     export
133 |     no_id_supported_groups : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ClientExtension SupportedGroups)
134 |     no_id_supported_groups = lengthed 2 $ map SupportedGroups (\(SupportedGroups x) => x) $ lengthed_list1 2 supported_group
135 |
136 |     export
137 |     no_id_signature_algorithms : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ClientExtension SignatureAlgorithms)
138 |     no_id_signature_algorithms = lengthed 2 $ map SignatureAlgorithms (\(SignatureAlgorithms x) => x) $ lengthed_list1 2 signature_algorithm
139 |
140 |     export
141 |     no_id_supported_versions : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ClientExtension SupportedVersions)
142 |     no_id_supported_versions = lengthed 2 $ map SupportedVersions (\(SupportedVersions x) => x) $ lengthed_list1 1 tls_version
143 |
144 |     export
145 |     no_id_key_share : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ClientExtension KeyShare)
146 |     no_id_key_share = lengthed 2 $ map KeyShare (\(KeyShare x) => x) $ lengthed_list1 2 (supported_group <*>> lengthed_list 2 token)
147 |
148 |     export
149 |     extension : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (DPair _ ClientExtension)
150 |     extension = map fix_client_extension hack_client_extension
151 |       $ (with_id no_id_server_name)
152 |       <|> (with_id no_id_supported_groups)
153 |       <|> (with_id no_id_signature_algorithms)
154 |       <|> (with_id no_id_supported_versions)
155 |       <|> (with_id no_id_key_share)
156 |
157 |   namespace Server
158 |     export
159 |     no_id_supported_groups : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ServerExtension SupportedGroups)
160 |     no_id_supported_groups = lengthed 2 $ map SupportedGroups (\(SupportedGroups x) => x) $ supported_group
161 |
162 |     export
163 |     no_id_signature_algorithms : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ServerExtension SignatureAlgorithms)
164 |     no_id_signature_algorithms = lengthed 2 $ map SignatureAlgorithms (\(SignatureAlgorithms x) => x) $ signature_algorithm
165 |
166 |     export
167 |     no_id_supported_versions : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ServerExtension SupportedVersions)
168 |     no_id_supported_versions = lengthed 2 $ map SupportedVersions (\(SupportedVersions x) => x) $ tls_version
169 |
170 |     export
171 |     no_id_key_share : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (ServerExtension KeyShare)
172 |     no_id_key_share = lengthed 2 $ map KeyShare (\(KeyShare x) => x) $ (supported_group <*>> lengthed_list 2 token)
173 |
174 |     export
175 |     with_id : (Cons (Posed Bits8) i, Monoid i) => {type : ExtensionType} -> Parserializer Bits8 i (SimpleError String) (ServerExtension type) -> Parserializer Bits8 i (SimpleError String) (ServerExtension type)
176 |     with_id pser = under (show type <+> " extension") $ is (pair_to_vect $ extension_type_to_id type) *> pser
177 |
178 |     export
179 |     with_id_unknown : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (rid ** ServerExtension (Unknown rid))
180 |     with_id_unknown = MkParserializer serialize deserialize
181 |       where
182 |         serialize : (rid ** ServerExtension (Unknown rid)) -> List Bits8
183 |         serialize ((a,b) ** (Unknown _ body)) = [a,b] <+> (prepend_length 2 body)
184 |         deserialize : Parser i (SimpleError String) (rid ** ServerExtension (Unknown rid))
185 |         deserialize = do
186 |           [a, b] <- count 2 p_get
187 |           body <- (lengthed_list 2 token).decode
188 |           pure ((a,b) ** Unknown (a,b) body)
189 |
190 |     export
191 |     extension : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (DPair _ ServerExtension)
192 |     extension = map fix_server_extension hack_server_extension
193 |       $ (with_id no_id_supported_groups)
194 |       <|> (with_id no_id_signature_algorithms)
195 |       <|> (with_id no_id_supported_versions)
196 |       <|> (with_id no_id_key_share)
197 |       <|> (with_id_unknown)
198 |
199 |