0 | module Network.TLS.Handshake
  1 |
  2 | import Data.Either
  3 | import Data.List1
  4 | import Data.Vect
  5 | import Network.TLS.HelloExtension
  6 | import Network.TLS.Magic
  7 | import Network.TLS.Parsing
  8 | import Utils.Bytes
  9 | import Utils.Misc
 10 | import Utils.Show
 11 |
 12 | namespace Message
 13 |   public export
 14 |   record ClientHello where
 15 |     constructor MkClientHello
 16 |     version : TLSVersion
 17 |     random : Vect 32 Bits8
 18 |     session_id : List Bits8
 19 |     cipher_suites : List1 CipherSuite
 20 |     compression_levels : List1 CompressionLevel
 21 |     extensions : List (DPair _ ClientExtension)
 22 |
 23 |   public export
 24 |   Show ClientHello where
 25 |     show x = show_record "ClientHello"
 26 |       [ ("version", show x.version)
 27 |       , ("random", xxd $ toList x.random)
 28 |       , ("session_id", xxd x.session_id)
 29 |       , ("cipher_suites", show x.cipher_suites)
 30 |       , ("compression_levels", show x.compression_levels)
 31 |       , ("extensions", show $ map (\x => show x.snd) x.extensions)
 32 |       ]
 33 |
 34 |   public export
 35 |   record ServerHello where
 36 |     constructor MkServerHello
 37 |     version : TLSVersion
 38 |     random : Vect 32 Bits8
 39 |     session_id : List Bits8
 40 |     cipher_suite : CipherSuite
 41 |     compression_level : CompressionLevel
 42 |     extensions : List (DPair _ ServerExtension)
 43 |
 44 |   public export
 45 |   Show ServerHello where
 46 |     show x = show_record "ClientHello"
 47 |       [ ("version", show x.version)
 48 |       , ("random", xxd $ toList x.random)
 49 |       , ("session_id", xxd x.session_id)
 50 |       , ("cipher_suite", show x.cipher_suite)
 51 |       , ("compression_level", show x.compression_level)
 52 |       , ("extensions", show $ map (\x => show x.snd) x.extensions)
 53 |       ]
 54 |
 55 |   public export
 56 |   record EncryptedExtensions where
 57 |     constructor MkEncryptedExtensions
 58 |     get : List Bits8 -- TODO: how would it work?
 59 |
 60 |   public export
 61 |   Show EncryptedExtensions where
 62 |     show x = show_record "EncryptedExtensions"
 63 |       [ ("get", xxd x.get)
 64 |       ]
 65 |
 66 |   public export
 67 |   record CertificateEntry where
 68 |     constructor MkCertificateEntry
 69 |     body : List Bits8
 70 |     extensions : List Bits8
 71 |
 72 |   public export
 73 |   Show CertificateEntry where
 74 |     show x = show_record "CertificateEntry"
 75 |       [ ("certificate", show $ xxd $ x.body)
 76 |       , ("certificate_extension", xxd x.extensions)
 77 |       ]
 78 |
 79 |   public export
 80 |   record Certificate where
 81 |     constructor MkCertificate
 82 |     request_context : List Bits8
 83 |     certificates : List CertificateEntry
 84 |
 85 |   public export
 86 |   Show Certificate where
 87 |     show x = show_record "Certificate"
 88 |       [ ("request_context", xxd x.request_context)
 89 |       , ("certificates", foldl (<+>) "" $ map show $ x.certificates)
 90 |       ]
 91 |
 92 |   public export
 93 |   record CertificateVerify where
 94 |     constructor MkCertificateVerify
 95 |     signature_algorithm : SignatureAlgorithm
 96 |     signature : List Bits8
 97 |
 98 |   public export
 99 |   Show CertificateVerify where
100 |     show x = show_record "CertificateVerify"
101 |       [ ("signature_algorithm", show x.signature_algorithm)
102 |       , ("signature", xxd x.signature)
103 |       ]
104 |
105 |   public export
106 |   record Finished where
107 |     constructor MkFinished
108 |     verify_data : List Bits8
109 |
110 |   public export
111 |   Show Finished where
112 |     show x = show_record "Finished"
113 |       [ ("verify_data", show x.verify_data)
114 |       ]
115 |
116 |   public export
117 |   record NewSessionTicket where
118 |     constructor MkNewSessionTicket
119 |     lifetime_seconds : Nat
120 |     age_add_milliseconds : Nat
121 |     nonce : List Bits8
122 |     session_ticket : List Bits8
123 |     extensions : List ((Bits8, Bits8), List Bits8)
124 |
125 |   public export
126 |   Show NewSessionTicket where
127 |     show x = show_record "NewSesssionTicket"
128 |       [ ("lifetime_seconds", show x.lifetime_seconds)
129 |       , ("age_add_milliseconds", show x.age_add_milliseconds)
130 |       , ("nonce", show x.nonce)
131 |       , ("session_ticket", show x.session_ticket)
132 |       , ("extensions", show x.extensions)
133 |       ]
134 |
135 |   public export
136 |   record ServerKeyExchange where
137 |     constructor MkServerKeyExchange
138 |     server_pk_group : SupportedGroup
139 |     server_pk_body : List Bits8
140 |     signature_algo : SignatureAlgorithm
141 |     signature_body : List Bits8
142 |
143 |   public export
144 |   Show ServerKeyExchange where
145 |     show x = show_record "ServerKeyExchange"
146 |       [ ("server_pk_group", show x.server_pk_group)
147 |       , ("server_pk_body", xxd x.server_pk_body)
148 |       , ("signature_algo", show x.signature_algo)
149 |       , ("signature_body", xxd x.signature_body)
150 |       ]
151 |
152 |   public export
153 |   record ServerHelloDone where
154 |     constructor MkServerHelloDone
155 |
156 |   public export
157 |   Show ServerHelloDone where
158 |     show x = show_record "ServerHelloDone" []
159 |
160 |   public export
161 |   record ClientKeyExchange where
162 |     constructor MkClientKeyExchange
163 |     public_key : List Bits8
164 |
165 |   Show ClientKeyExchange where
166 |     show x = show_record "ClientKeyExchange"
167 |       [ ("public_key", show x.public_key)
168 |       ]
169 |
170 | public export
171 | data Handshake : HandshakeType -> Type where
172 |   ClientHello : ClientHello -> Handshake ClientHello
173 |   ServerHello : ServerHello -> Handshake ServerHello
174 |   EncryptedExtensions : EncryptedExtensions -> Handshake EncryptedExtensions
175 |   Certificate : Certificate -> Handshake Certificate
176 |   CertificateVerify : CertificateVerify -> Handshake CertificateVerify
177 |   Finished : Finished -> Handshake Finished
178 |   NewSessionTicket : NewSessionTicket -> Handshake NewSessionTicket
179 |   ServerKeyExchange : ServerKeyExchange -> Handshake ServerKeyExchange
180 |   ServerHelloDone : ServerHelloDone -> Handshake ServerHelloDone
181 |   ClientKeyExchange : ClientKeyExchange -> Handshake ClientKeyExchange
182 |
183 | public export
184 | Show (Handshake type) where
185 |   show (ClientHello x) = show x
186 |   show (ServerHello x) = show x
187 |   show (EncryptedExtensions x) = show x
188 |   show (Certificate x) = show x
189 |   show (CertificateVerify x) = show x
190 |   show (Finished x) = show x
191 |   show (NewSessionTicket x) = show x
192 |   show (ServerKeyExchange x) = show x
193 |   show (ServerHelloDone x) = show x
194 |   show (ClientKeyExchange x) = show x
195 |
196 | XHandshake : Type
197 | XHandshake = Eithers
198 |   [ Handshake ClientHello
199 |   , Handshake ServerHello
200 |   , Handshake EncryptedExtensions
201 |   , Handshake Certificate
202 |   , Handshake CertificateVerify
203 |   , Handshake Finished
204 |   , Handshake NewSessionTicket
205 |   , Handshake ServerKeyExchange
206 |   , Handshake ServerHelloDone
207 |   , Handshake ClientKeyExchange
208 |   ]
209 |
210 | hack_handshake : DPair _ Handshake -> XHandshake
211 | hack_handshake (ClientHello ** x)         = Left x
212 | hack_handshake (ServerHello ** x)         = Right (Left x)
213 | hack_handshake (EncryptedExtensions ** x) = Right (Right (Left x))
214 | hack_handshake (Certificate ** x)         = Right (Right (Right (Left x)))
215 | hack_handshake (CertificateVerify ** x)   = Right (Right (Right (Right (Left x))))
216 | hack_handshake (Finished ** x)            = Right (Right (Right (Right (Right (Left x)))))
217 | hack_handshake (NewSessionTicket ** x)    = Right (Right (Right (Right (Right (Right (Left x))))))
218 | hack_handshake (ServerKeyExchange ** x)   = Right (Right (Right (Right (Right (Right (Right (Left x)))))))
219 | hack_handshake (ServerHelloDone ** x)     = Right (Right (Right (Right (Right (Right (Right (Right (Left x))))))))
220 | hack_handshake (ClientKeyExchange ** x)   = Right (Right (Right (Right (Right (Right (Right (Right (Right x))))))))
221 |
222 | fix_handshake : XHandshake -> DPair _ Handshake
223 | fix_handshake (Left x)                                                                  = (ClientHello ** x)
224 | fix_handshake (Right (Left x))                                                          = (ServerHello ** x)
225 | fix_handshake (Right (Right (Left x)))                                                  = (EncryptedExtensions ** x)
226 | fix_handshake (Right (Right (Right (Left x))))                                          = (Certificate ** x)
227 | fix_handshake (Right (Right (Right (Right (Left x)))))                                  = (CertificateVerify ** x)
228 | fix_handshake (Right (Right (Right (Right (Right (Left x))))))                          = (Finished ** x)
229 | fix_handshake (Right (Right (Right (Right (Right (Right (Left x)))))))                  = (NewSessionTicket ** x)
230 | fix_handshake (Right (Right (Right (Right (Right (Right (Right (Left x))))))))          = (ServerKeyExchange ** x)
231 | fix_handshake (Right (Right (Right (Right (Right (Right (Right (Right (Left x)))))))))  = (ServerHelloDone ** x)
232 | fix_handshake (Right (Right (Right (Right (Right (Right (Right (Right (Right x))))))))) = (ClientKeyExchange ** x)
233 |
234 | namespace Parsing
235 |   export
236 |   handshake_id_with_length : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (HandshakeType, Nat)
237 |   handshake_id_with_length = handshake_type <*>> nat 3
238 |
239 |   export
240 |   no_id_client_hello : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ClientHello)
241 |   no_id_client_hello = map (\(a,b,c,d,e,f) => ClientHello (MkClientHello a b c d e f)) (\(ClientHello (MkClientHello a b c d e f)) => (a,b,c,d,e,f))
242 |     $ lengthed 3
243 |     $ under "client version" tls_version
244 |     <*>> (under "client random" $ ntokens 32)
245 |     <*>> (under "session id" $ lengthed_list 1 token)
246 |     <*>> (under "client proposed cipher suites" $ lengthed_list1 2 cipher_suite)
247 |     <*>> (under "client proposed compression levels" $ lengthed_list1 1 compression_level)
248 |     <*>> (under "client extensions" $ lengthed_list 2 extension)
249 |
250 |   export
251 |   no_id_server_hello : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ServerHello)
252 |   no_id_server_hello = map
253 |     ((\(a,b,c,d,e,f) => ServerHello (MkServerHello a b c d e f)) . fromEither) -- (\(a,b,c,d,e,f) => ServerHello (MkServerHello a b c d e f))
254 |     (\(ServerHello (MkServerHello a b c d e f)) => Left (a,b,c,d,e,f))
255 |     $ ( lengthed 3
256 |     $ (under "server version" tls_version)
257 |     <*>> (under "server random" $ ntokens 32)
258 |     <*>> (under "session id" $ lengthed_list 1 token)
259 |     <*>> (under "server chosen cipher suite" $ cipher_suite)
260 |     <*>> (under "server chosen compression level" $ compression_level)
261 |     <*>> (under "server extensions" $ lengthed_list 2 Server.extension)
262 |     )
263 |     <|> ( lengthed 3
264 |     $ (under "server version" tls_version)
265 |     <*>> (under "server random" $ ntokens 32)
266 |     <*>> (under "session id" $ lengthed_list 1 token)
267 |     <*>> (under "server chosen cipher suite" $ cipher_suite)
268 |     <*>> (under "server chosen compression level" $ compression_level)
269 |     <*>> (under "server extensions" $ MkParserializer (const []) (pure []))
270 |     )
271 |
272 |   export
273 |   no_id_encrypted_extensions : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake EncryptedExtensions)
274 |   no_id_encrypted_extensions = map (\a => EncryptedExtensions (MkEncryptedExtensions a)) (\(EncryptedExtensions (MkEncryptedExtensions a)) => a)
275 |     $ lengthed 3
276 |     $ (under "encrypted extensions body" $ lengthed_list 2 token)
277 |
278 |   export
279 |   no_id_certificate : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake Certificate)
280 |   no_id_certificate =
281 |     map
282 |     (\(a,b) => Certificate (MkCertificate a $ map (uncurry MkCertificateEntry) b))
283 |     (\(Certificate (MkCertificate a d)) => (a, map (\b => (b.body, b.extensions)) d))
284 |     $ lengthed 3
285 |     $ (under "request context" $ lengthed_list 1 token)
286 |     <*>> (under "certificates"
287 |          $ under "certificate list"
288 |          $ lengthed_list 3
289 |          $ under "certificate entry"
290 |          $ (lengthed_list 3 token <*>> (under "certificate extensions" $ lengthed_list 2 token)))
291 |
292 |   export
293 |   no_id_certificate2 : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake Certificate)
294 |   no_id_certificate2 = map
295 |     (\b => Certificate (MkCertificate [] $ map (\x => MkCertificateEntry x []) b))
296 |     (\(Certificate (MkCertificate a b)) => map body b)
297 |     $ lengthed 3
298 |     $ (under "certificate list 1.2" $ lengthed_list 3 $ under "certificate entry 1.2" $ lengthed_list 3 token)
299 |
300 |   export
301 |   no_id_certificate_verify : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake CertificateVerify)
302 |   no_id_certificate_verify = map (\(a,b) => CertificateVerify (MkCertificateVerify a b)) (\(CertificateVerify (MkCertificateVerify a b)) => (a,b))
303 |     $ lengthed 3
304 |     $ signature_algorithm
305 |     <*>> (under "signature" $ lengthed_list 2 token)
306 |
307 |   export
308 |   no_id_finished : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake Finished)
309 |   no_id_finished = map (\a => Finished (MkFinished a)) (\(Finished (MkFinished a)) => a)
310 |     $ lengthed_list 3 token
311 |
312 |   export
313 |   no_id_new_session_ticket : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake NewSessionTicket)
314 |   no_id_new_session_ticket = map
315 |     (\(a,b,c,d,e) => NewSessionTicket (MkNewSessionTicket a b c d e))
316 |     (\(NewSessionTicket (MkNewSessionTicket a b c d e)) => (a,b,c,d,e))
317 |     $ lengthed 3
318 |     $ (under "ticket lifetime seconds" $ nat 4)
319 |     <*>> (under "ticket age add milliseconds" $ nat 4)
320 |     <*>> (under "ticket nonce" $ lengthed_list 1 token)
321 |     <*>> (under "session ticket" $ lengthed_list 2 token)
322 |     <*>> (under "extensions" $ lengthed_list 2 ((token <*>> token) <*>> lengthed_list 2 token))
323 |
324 |   export
325 |   no_id_server_key_exchange : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ServerKeyExchange)
326 |   no_id_server_key_exchange = map
327 |     (\(a,b,c,d) => ServerKeyExchange (MkServerKeyExchange a b c d))
328 |     (\(ServerKeyExchange (MkServerKeyExchange a b c d)) => (a,b,c,d))
329 |     $ lengthed 3
330 |     $ (under "curve info" $ (is [0x03]) *> supported_group)
331 |     <*>> (under "public key" $ lengthed_list 1 token)
332 |     <*>> (under "signature algo" signature_algorithm)
333 |     <*>> (under "signature body" $ lengthed_list 2 token)
334 |
335 |   export
336 |   no_id_server_hello_done : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ServerHelloDone)
337 |   no_id_server_hello_done = map
338 |     (const (ServerHelloDone MkServerHelloDone))
339 |     (const ())
340 |     $ is [0x00, 0x00, 0x00]
341 |
342 |   export
343 |   no_id_client_key_exchange : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ClientKeyExchange)
344 |   no_id_client_key_exchange = map
345 |     (ClientKeyExchange . MkClientKeyExchange)
346 |     (\(ClientKeyExchange (MkClientKeyExchange x)) => x)
347 |     $ lengthed 3
348 |     $ (under "public key" $ lengthed_list 1 token)
349 |
350 |   export
351 |   with_id : (Cons (Posed Bits8) i, Monoid i) => {type : HandshakeType} -> Parserializer Bits8 i (SimpleError String) (Handshake type) -> Parserializer Bits8 i (SimpleError String) (Handshake type)
352 |   with_id pser = under (show type <+> " handshake") $ is (to_vect $ handshake_type_to_id type) *> pser
353 |
354 |   export
355 |   handshake : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (DPair _ Handshake)
356 |   handshake = map fix_handshake hack_handshake
357 |     $ (with_id no_id_client_hello)
358 |     <|> (with_id no_id_server_hello)
359 |     <|> (with_id no_id_encrypted_extensions)
360 |     <|> (with_id no_id_certificate)
361 |     <|> (with_id no_id_certificate_verify)
362 |     <|> (with_id no_id_finished)
363 |     <|> (with_id no_id_new_session_ticket)
364 |     <|> (with_id no_id_server_key_exchange)
365 |     <|> (with_id no_id_server_hello_done)
366 |     <|> (with_id no_id_client_key_exchange)
367 |
368 |   export
369 |   handshake2 : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (DPair _ Handshake)
370 |   handshake2 = map fix_handshake hack_handshake
371 |     $ (with_id no_id_client_hello)
372 |     <|> (with_id no_id_server_hello)
373 |     <|> (with_id no_id_encrypted_extensions)
374 |     <|> (with_id no_id_certificate2)
375 |     <|> (with_id no_id_certificate_verify)
376 |     <|> (with_id no_id_finished)
377 |     <|> (with_id no_id_new_session_ticket)
378 |     <|> (with_id no_id_server_key_exchange)
379 |     <|> (with_id no_id_server_hello_done)
380 |     <|> (with_id no_id_client_key_exchange)
381 |