-
Notifications
You must be signed in to change notification settings - Fork 0
/
CTLS.MessageFormats.fst
719 lines (613 loc) · 29.6 KB
/
CTLS.MessageFormats.fst
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
module CTLS.MessageFormats
open FStar.List.Tot
open Comparse
open TLS13.MessageFormats
open TLS13.OldExtensions
open CTLS.Profile
#set-options "--fuel 0 --ifuel 0"
noeq
type ctls_unknowns (bytes:Type0) {|bytes_like bytes|} = {
ctls_template_handshake_type: ht:handshake_type{HT_unknown_handshake_type? ht};
self_delimiting_extension: etype:extension_type{ET_unknown_extension_type? etype} -> option (typ:Type0 & parser_serializer_prefix bytes typ);
is_x509_certificate: bytes -> bool;
}
val no_template_dep: #bytes:Type0 -> {|bytes_like bytes|} -> a:Type0 -> (ctls_template bytes -> Type0)
let no_template_dep #bytes a t = a
val mk_templated_type:
#a:Type0 -> bytes:Type0 -> {|bytes_like bytes|} ->
(ctls_template bytes -> option a) ->
Type0 -> (a -> Type0) ->
(ctls_template bytes -> Type0)
let mk_templated_type #a bytes #bl get_template_elem default_ty parametric_ty template =
match get_template_elem template with
| None -> default_ty
| Some param -> parametric_ty param
val ps_mk_templated_type:
#a:Type0 ->
#default_ty:Type0 -> #parametric_ty:(a -> Type0) ->
bytes:Type0 -> {|bytes_like bytes|} ->
get_template_elem:(ctls_template bytes -> option a) ->
parser_serializer_prefix bytes default_ty ->
(param:a -> parser_serializer_prefix bytes (parametric_ty param)) ->
(template:ctls_template bytes -> parser_serializer_prefix bytes (mk_templated_type bytes get_template_elem default_ty parametric_ty template))
let ps_mk_templated_type #a #default_ty #parametric_ty bytes #bl get_template_elem ps_default_ty ps_parametric_ty template =
match get_template_elem template with
| None -> ps_default_ty
| Some param -> ps_parametric_ty param
(*** Ciphersuite ***)
val get_cipher_suite_template: #bytes:Type0 -> {|bytes_like bytes|} -> ctls_template bytes -> option (ctls_cipher_suite_template bytes)
let get_cipher_suite_template #bytes #bl t =
get_template_element ps_ctls_cipher_suite_template CTLSTET_cipher_suite t
[@@ can_be_unit]
type pre_ctls_cipher_suites (bytes:Type0) {|bytes_like bytes|} (cipher_suite:ctls_cipher_suite_template bytes) =
unit
%splice [ps_pre_ctls_cipher_suites] (gen_parser (`pre_ctls_cipher_suites))
type ctls_cipher_suites (bytes:Type0) {|bytes_like bytes|} =
mk_templated_type bytes get_cipher_suite_template (tls_list bytes (ps_cipher_suite) ({min=2; max=(pow2 16)-2})) (pre_ctls_cipher_suites bytes)
let ps_ctls_cipher_suites (bytes:Type0) {|bytes_like bytes|} =
ps_mk_templated_type bytes get_cipher_suite_template (ps_tls_list (ps_cipher_suite) ({min=2; max=(pow2 16)-2})) ps_pre_ctls_cipher_suites
[@@ can_be_unit]
type pre_ctls_cipher_suite (bytes:Type0) {|bytes_like bytes|} (cipher_suite:ctls_cipher_suite_template bytes) =
unit
%splice [ps_pre_ctls_cipher_suite] (gen_parser (`pre_ctls_cipher_suite))
type ctls_cipher_suite (bytes:Type0) {|bytes_like bytes|} =
mk_templated_type bytes get_cipher_suite_template cipher_suite (pre_ctls_cipher_suite bytes)
let ps_ctls_cipher_suite (bytes:Type0) {|bytes_like bytes|} =
ps_mk_templated_type bytes get_cipher_suite_template ps_cipher_suite ps_pre_ctls_cipher_suite
(*** DH group ***)
val get_dh_group_template: #bytes:Type0 -> {|bytes_like bytes|} -> ctls_template bytes -> option (ctls_dh_group_template bytes)
let get_dh_group_template #bytes #bl t =
get_template_element ps_ctls_dh_group_template CTLSTET_dh_group t
type pre_ctls_key_share_entry (bytes:Type0) {|bytes_like bytes|} (dh_group:ctls_dh_group_template bytes) = (
if dh_group.key_share_length = 0 then
// opaque key_exchange<1..2^16-1>;
tls_bytes bytes (({min=1; max=(pow2 16)-1}))
else
lbytes bytes dh_group.key_share_length
)
%splice [ps_pre_ctls_key_share_entry] (gen_parser (`pre_ctls_key_share_entry))
type pre_ctls_key_share_client_hello (bytes:Type0) {|bytes_like bytes|} (dh_group:ctls_dh_group_template bytes) = {
client_shares: pre_ctls_key_share_entry bytes dh_group;
}
%splice [ps_pre_ctls_key_share_client_hello] (gen_parser (`pre_ctls_key_share_client_hello))
type ctls_key_share_client_hello (bytes:Type0) {|bytes_like bytes|} =
mk_templated_type bytes get_dh_group_template (key_share_client_hello bytes) (pre_ctls_key_share_client_hello bytes)
let ps_ctls_key_share_client_hello (bytes:Type0) {|bytes_like bytes|} =
ps_mk_templated_type bytes get_dh_group_template ps_key_share_client_hello ps_pre_ctls_key_share_client_hello
type pre_ctls_key_share_server_hello (bytes:Type0) {|bytes_like bytes|} (dh_group:ctls_dh_group_template bytes) = {
server_share: pre_ctls_key_share_entry bytes dh_group;
}
%splice [ps_pre_ctls_key_share_server_hello] (gen_parser (`pre_ctls_key_share_server_hello))
type ctls_key_share_server_hello (bytes:Type0) {|bytes_like bytes|} =
mk_templated_type bytes get_dh_group_template (key_share_server_hello bytes) (pre_ctls_key_share_server_hello bytes)
let ps_ctls_key_share_server_hello (bytes:Type0) {|bytes_like bytes|} =
ps_mk_templated_type bytes get_dh_group_template ps_key_share_server_hello ps_pre_ctls_key_share_server_hello
(*** Signature algorithm ***)
val get_signature_algorithm_template: #bytes:Type0 -> {|bytes_like bytes|} -> ctls_template bytes -> option (ctls_signature_algorithm_template bytes)
let get_signature_algorithm_template #bytes #bl t =
get_template_element ps_ctls_signature_algorithm_template CTLSTET_signature_algorithm t
// Compression of CertificateVerify.algorithm
[@@ can_be_unit]
type pre_ctls_certificate_verify_algorithm (bytes:Type0) {|bytes_like bytes|} (signature_algorithm:ctls_signature_algorithm_template bytes) =
unit
%splice [ps_pre_ctls_certificate_verify_algorithm] (gen_parser (`pre_ctls_certificate_verify_algorithm))
type ctls_certificate_verify_algorithm (bytes:Type0) {|bytes_like bytes|} =
mk_templated_type bytes get_signature_algorithm_template (signature_scheme) (pre_ctls_certificate_verify_algorithm bytes)
let ps_ctls_certificate_verify_algorithm (bytes:Type0) {|bytes_like bytes|} =
ps_mk_templated_type bytes get_signature_algorithm_template ps_signature_scheme ps_pre_ctls_certificate_verify_algorithm
// Compression of CertificateVerify.signature
type pre_ctls_certificate_verify_signature (bytes:Type0) {|bytes_like bytes|} (signature_algorithm:ctls_signature_algorithm_template bytes) = (
if signature_algorithm.signature_length = 0 then
// opaque signature<0..2^16-1>;
tls_bytes bytes (({min=0; max=(pow2 16)-1}))
else
lbytes bytes signature_algorithm.signature_length
)
%splice [ps_pre_ctls_certificate_verify_signature] (gen_parser (`pre_ctls_certificate_verify_signature))
type ctls_certificate_verify_signature (bytes:Type0) {|bytes_like bytes|} =
mk_templated_type bytes get_signature_algorithm_template (tls_bytes bytes (({min=0; max=(pow2 16)-1}))) (pre_ctls_certificate_verify_signature bytes)
let ps_ctls_certificate_verify_signature (bytes:Type0) {|bytes_like bytes|} =
ps_mk_templated_type bytes get_signature_algorithm_template (ps_tls_bytes (({min=0; max=(pow2 16)-1}))) ps_pre_ctls_certificate_verify_signature
(*** Random ***)
val get_random_template: #bytes:Type0 -> {|bytes_like bytes|} -> ctls_template bytes -> option (ctls_random_template bytes)
let get_random_template #bytes #bl t =
get_template_element ps_ctls_random_template CTLSTET_random t
[@@ can_be_unit]
type pre_ctls_random (bytes:Type0) {|bytes_like bytes|} (rand_sz:ctls_random_template bytes) =
lbytes bytes rand_sz
%splice [ps_pre_ctls_random] (gen_parser (`pre_ctls_random))
type ctls_random (bytes:Type0) {|bytes_like bytes|} =
mk_templated_type bytes get_random_template (random bytes) (pre_ctls_random bytes)
let ps_ctls_random (bytes:Type0) {|bytes_like bytes|} =
ps_mk_templated_type bytes get_random_template ps_random ps_pre_ctls_random
(*** Extension ***)
type tls_extension_inner (bytes:Type0) {|bytes_like bytes|} = {
extension_data: tls_bytes bytes (({min=0; max=(pow2 16)-1}));
}
%splice [ps_tls_extension_inner] (gen_parser (`tls_extension_inner))
noeq
type one_extension_type (bytes:Type0) {|bytes_like bytes|} = {
typ: ctls_template bytes -> Type0;
parser: t:ctls_template bytes -> parser_serializer_prefix bytes (typ t);
}
noeq
type ctls_extensions_types (bytes:Type0) {|bytes_like bytes|} = {
expected_ty: extension_type -> one_extension_type bytes;
additional_ty: extension_type -> one_extension_type bytes;
}
#push-options "--ifuel 1"
val ctls_expected_extensions: #bytes:Type0 -> {|bytes_like bytes|} -> ctls_extensions_types bytes -> ctls_template bytes -> list extension_type -> Type0
let rec ctls_expected_extensions #bytes #bl comp temp ty_list =
match ty_list with
| [] -> unit
| h_ty::t_ty -> (comp.expected_ty h_ty).typ temp & (ctls_expected_extensions comp temp t_ty)
#pop-options
#push-options "--ifuel 1 --fuel 1"
val ps_ctls_expected_extensions: #bytes:Type0 -> {|bytes_like bytes|} -> comp:ctls_extensions_types bytes -> temp:ctls_template bytes -> ty_list:list extension_type -> parser_serializer_prefix bytes (ctls_expected_extensions comp temp ty_list)
let rec ps_ctls_expected_extensions #bytes #bl comp temp ty_list =
match ty_list with
| [] ->
mk_isomorphism
(ctls_expected_extensions comp temp ty_list)
ps_unit
(fun x -> x <: (ctls_expected_extensions comp temp []))
(fun (x:(ctls_expected_extensions comp temp [])) -> x)
| h_ty::t_ty -> (
let f ((|x,y|): (_:((comp.expected_ty h_ty).typ temp) & (ctls_expected_extensions comp temp t_ty))): ctls_expected_extensions comp temp (h_ty::t_ty) =
(x, y)
in
let g ((x,y): ctls_expected_extensions comp temp (h_ty::t_ty)): _:((comp.expected_ty h_ty).typ temp) & (ctls_expected_extensions comp temp t_ty) =
(|x, y|)
in
assert(forall x. f (g x) == x) by (
let open FStar.Tactics in
destruct (forall_intro ());
let _ = intro() in
let _ = intro() in
l_to_r [binder_to_term (intro ())];
trefl()
);
mk_isomorphism
(ctls_expected_extensions comp temp ty_list)
(bind ((comp.expected_ty h_ty).parser temp) (fun _ -> ps_ctls_expected_extensions comp temp t_ty))
f
g
)
#pop-options
noeq
type compressed_extension (bytes:Type0) {|bytes_like bytes|} (comp:ctls_extensions_types bytes) (temp:ctls_template bytes) = {
extension_type: extension_type;
[@@@ with_parser ((comp.additional_ty extension_type).parser temp)]
extension_data: (comp.additional_ty extension_type).typ temp;
}
%splice [ps_compressed_extension] (gen_parser (`compressed_extension))
noeq
type ctls_extensions_allow_additional_internal (bytes:Type0) {|bytes_like bytes|} (comp:ctls_extensions_types bytes) (expected_exts:list extension_type) (temp:ctls_template bytes) = {
expected_extensions: ctls_expected_extensions comp temp expected_exts;
additional_extensions: list (compressed_extension bytes comp temp);
}
val ps_whole_ctls_extensions_allow_additional_internal:
#bytes:Type0 -> {|bytes_like bytes|} ->
comp:ctls_extensions_types bytes -> expected_exts:list extension_type -> temp:ctls_template bytes ->
parser_serializer_whole bytes (ctls_extensions_allow_additional_internal bytes comp expected_exts temp)
let ps_whole_ctls_extensions_allow_additional_internal #bytes #bl comp expected_exts temp =
mk_isomorphism_whole
(ctls_extensions_allow_additional_internal bytes comp expected_exts temp)
(bind_whole (ps_ctls_expected_extensions comp temp expected_exts) (fun _ -> ps_whole_list (ps_compressed_extension comp temp)))
(fun (|expected_extensions, additional_extensions|) -> {expected_extensions; additional_extensions})
(fun {expected_extensions; additional_extensions} -> (|expected_extensions, additional_extensions|))
type fixed_length_ctls_extensions_allow_additional_internal (bytes:Type0) {|bytes_like bytes|} (comp:ctls_extensions_types bytes) (expected_exts:list extension_type) (temp:ctls_template bytes) (length:nat) =
refined (ctls_extensions_allow_additional_internal bytes comp expected_exts temp) (ps_whole_length_pred (ps_whole_ctls_extensions_allow_additional_internal comp expected_exts temp) length)
val ps_fixed_length_ctls_extensions_allow_additional_internal:
#bytes:Type0 -> {|bytes_like bytes|} ->
comp:ctls_extensions_types bytes -> expected_exts:list extension_type -> temp:ctls_template bytes -> length:nat ->
parser_serializer_prefix bytes (fixed_length_ctls_extensions_allow_additional_internal bytes comp expected_exts temp length)
let ps_fixed_length_ctls_extensions_allow_additional_internal #bytes #bl comp expected_exts temp length =
ps_whole_to_ps_prefix length (refine_whole (ps_whole_ctls_extensions_allow_additional_internal comp expected_exts temp) (ps_whole_length_pred (ps_whole_ctls_extensions_allow_additional_internal comp expected_exts temp) length))
noeq
type ctls_extensions_allow_additional (bytes:Type0) {|bytes_like bytes|} (comp:ctls_extensions_types bytes) (expected_exts:list extension_type) (temp:ctls_template bytes) = {
length: nat_lbytes 2;
content: fixed_length_ctls_extensions_allow_additional_internal bytes comp expected_exts temp length;
}
%splice [ps_ctls_extensions_allow_additional] (gen_parser(`ctls_extensions_allow_additional))
type ctls_extensions_template (bytes:Type0) {|bytes_like bytes|} = {
predefined_extensions: list (extension bytes);
expected_extensions: list extension_type;
allow_additional: bool;
}
[@@ can_be_unit]
val extensions_ctls_type:
#bytes:Type0 -> {|bytes_like bytes|} ->
ctls_extensions_types bytes -> (ctls_template bytes -> ctls_extensions_template bytes) ->
ctls_template bytes -> Type0
let extensions_ctls_type #bytes #bl ext_comp get_ext_temp temp =
let ext_temp = get_ext_temp temp in
if ext_temp.allow_additional then
ctls_extensions_allow_additional bytes ext_comp ext_temp.expected_extensions temp
else (
ctls_expected_extensions ext_comp temp ext_temp.expected_extensions
)
%splice [ps_extensions_ctls_type] (gen_parser (`extensions_ctls_type))
type extension_origin =
| ClientHello: extension_origin
| ServerHello: extension_origin
| EncryptedExtensions: extension_origin
| Certificate: extension_origin
| CertificateRequest: extension_origin
| NewSessionTicket: extension_origin
| HelloRetryRequest: extension_origin
val default_ext_temp:
#bytes:Type0 -> {|bytes_like bytes|} ->
ctls_extensions_template bytes
let default_ext_temp #bytes #bl = {
predefined_extensions = [];
expected_extensions = [];
allow_additional = true;
}
val get_ctls_extension_template:
#bytes:Type0 -> {|bytes_like bytes|} ->
extension_origin -> ctls_template bytes ->
option (ctls_extension_template bytes)
let get_ctls_extension_template #bytes #bl origin temp =
match origin with
| ClientHello ->
get_template_element ps_ctls_extension_template CTLSTET_client_hello_extensions temp
| ServerHello ->
get_template_element ps_ctls_extension_template CTLSTET_server_hello_extensions temp
| EncryptedExtensions ->
get_template_element ps_ctls_extension_template CTLSTET_encrypted_extensions temp
| CertificateRequest ->
get_template_element ps_ctls_extension_template CTLSTET_certificate_request_extensions temp
| _ -> None
val convert_ctls_extension_template:
#bytes:Type0 -> {|bytes_like bytes|} ->
ctls_extension_template bytes ->
ctls_extensions_template bytes
let convert_ctls_extension_template #bytes #bl t = {
predefined_extensions = t.predefined_extensions;
expected_extensions = t.expected_extensions;
allow_additional = t.allow_additional <> 0;
}
#push-options "--fuel 2 --ifuel 1 --z3rlimit 25"
val compute_ext_temp:
#bytes:Type0 -> {|bytes_like bytes|} ->
extension_origin -> ctls_template bytes ->
ctls_extensions_template bytes
let compute_ext_temp #bytes #bl origin temp =
let ext_temp =
match get_ctls_extension_template origin temp with
| None -> default_ext_temp
| Some x -> convert_ctls_extension_template x
in
let ext_temp =
match origin, get_dh_group_template temp with
| ClientHello, Some dh_group
| EncryptedExtensions, Some dh_group -> (
let supported_groups_ext: extension bytes = {
extension_type = ET_supported_groups;
extension_data = (ps_prefix_to_ps_whole #bytes ps_named_group_list).serialize ({
named_group_list_ = [dh_group.group_name];
})
} in
{ ext_temp with
predefined_extensions = supported_groups_ext::ext_temp.predefined_extensions;
}
)
| _ -> ext_temp
in
let ext_temp =
match origin, get_signature_algorithm_template temp with
| ClientHello, Some signature_algorithm
| CertificateRequest, Some signature_algorithm -> (
let supported_groups_ext: extension bytes = {
extension_type = ET_signature_algorithms;
extension_data = (ps_prefix_to_ps_whole #bytes ps_signature_scheme_list).serialize ({
supported_signature_algorithms = [signature_algorithm.signature_scheme];
})
} in
{ ext_temp with
predefined_extensions = supported_groups_ext::ext_temp.predefined_extensions;
}
)
| _ -> ext_temp
in
ext_temp
#pop-options
#push-options "--ifuel 1"
val extension_origin_to_handshake_type: extension_origin -> handshake_type
let extension_origin_to_handshake_type ext_orig =
match ext_orig with
| ClientHello -> HT_client_hello
| ServerHello -> HT_server_hello
| EncryptedExtensions -> HT_encrypted_extensions
| Certificate -> HT_certificate
| CertificateRequest -> HT_certificate_request
| NewSessionTicket -> HT_new_session_ticket
| HelloRetryRequest -> HT_server_hello // See RFC 8446, Section 4.1.3 and 4.1.4
#pop-options
val get_rfc8446_self_delimiting_extension_parser:
#bytes:Type0 -> {|bytes_like bytes|} ->
extension_origin -> extension_type ->
option (a:Type0 & parser_serializer_prefix bytes a)
let get_rfc8446_self_delimiting_extension_parser #bytes #bl ext_orig ext_ty =
let hs_ty = extension_origin_to_handshake_type ext_orig in
match ext_ty with
| ET_server_name ->
Some (|server_name bytes, ps_server_name|)
| ET_max_fragment_length ->
Some (|max_fragment_length, ps_max_fragment_length|)
| ET_status_request ->
Some (|ocsp_status_request bytes, ps_ocsp_status_request|)
| ET_supported_groups ->
Some (|named_group_list bytes, ps_named_group_list|)
| ET_signature_algorithms ->
Some (|signature_scheme_list bytes, ps_signature_scheme_list|)
| ET_use_srtp ->
Some (|use_srtp_data bytes, ps_use_srtp_data|)
| ET_heartbeat ->
Some (|heartbeat_extension bytes, ps_heartbeat_extension|)
| ET_application_layer_protocol_negotiation ->
Some (|protocol_name_list bytes, ps_protocol_name_list|)
| ET_signed_certificate_timestamp -> (
match ext_orig with
| Certificate ->
Some (|signed_certificate_timestamp_list bytes, ps_signed_certificate_timestamp_list|)
| ClientHello ->
Some (|empty, ps_empty|)
| _ ->
None
)
| ET_client_certificate_type -> (
match ext_orig with
| ClientHello ->
Some (|client_cert_type_extension bytes COSE_client, (ps_client_cert_type_extension COSE_client)|)
| EncryptedExtensions ->
Some (|client_cert_type_extension bytes COSE_server, (ps_client_cert_type_extension COSE_server)|)
| _ -> None
)
| ET_server_certificate_type -> (
match ext_orig with
| ClientHello ->
Some (|server_cert_type_extension bytes COSE_client, (ps_server_cert_type_extension COSE_client)|)
| EncryptedExtensions ->
Some (|server_cert_type_extension bytes COSE_server, (ps_server_cert_type_extension COSE_server)|)
| _ -> None
)
| ET_pre_shared_key ->
Some (|pre_shared_key_extension bytes hs_ty, (ps_pre_shared_key_extension hs_ty)|)
| ET_early_data ->
Some (|early_data_indication hs_ty, (ps_early_data_indication hs_ty)|)
| ET_supported_versions ->
Some (|supported_versions bytes hs_ty, (ps_supported_versions hs_ty)|)
| ET_cookie ->
Some (|cookie bytes, ps_cookie|)
| ET_psk_key_exchange_modes ->
Some (|psk_key_exchange_mode bytes, ps_psk_key_exchange_mode|)
| ET_certificate_authorities ->
Some (|certificate_authorities_extension bytes, ps_certificate_authorities_extension|)
| ET_oid_filters ->
Some (|oid_filter_extension bytes, ps_oid_filter_extension|)
| ET_post_handshake_auth ->
Some (|post_handshake_auth, ps_post_handshake_auth|)
| ET_signature_algorithms_cert ->
Some (|signature_scheme_list bytes, ps_signature_scheme_list|)
| ET_key_share -> (
match ext_orig with
| ClientHello ->
Some (|key_share_client_hello bytes, ps_key_share_client_hello|)
| HelloRetryRequest ->
Some (|key_share_hello_retry_request bytes, ps_key_share_hello_retry_request|)
| ServerHello ->
Some (|key_share_server_hello bytes, ps_key_share_server_hello|)
| _ ->
None
)
| _ -> None
val one_extension_type_for_self_delimiting_extension:
#bytes:Type0 -> {|bytes_like bytes|} ->
#tls_type:Type0 ->
parser_serializer_prefix bytes tls_type ->
one_extension_type bytes
let one_extension_type_for_self_delimiting_extension #bytes #bl #tls_type ps_tls_type = {
typ = (fun _ -> tls_type);
parser = (fun _ -> ps_tls_type);
}
val default_one_ext_type:
#bytes:Type0 -> {|bytes_like bytes|} ->
one_extension_type bytes
let default_one_ext_type #bytes #bl =
{
typ = (fun _ -> tls_extension_inner bytes);
parser = (fun _ -> ps_tls_extension_inner);
}
val compute_ext_type_aux:
#bytes:Type0 -> {|bytes_like bytes|} ->
ctls_unknowns bytes ->
extension_origin -> extension_type ->
one_extension_type bytes
let compute_ext_type_aux #bytes #bl unk origin ext_ty =
match origin, ext_ty with
| ClientHello, ET_key_share -> {
typ = ctls_key_share_client_hello bytes;
parser = ps_ctls_key_share_client_hello bytes;
}
| ServerHello, ET_key_share -> {
typ = ctls_key_share_server_hello bytes;
parser = ps_ctls_key_share_server_hello bytes;
}
| _, _ -> (
match get_rfc8446_self_delimiting_extension_parser origin ext_ty with
| Some (|tls_type, ps_tls_type|) ->
one_extension_type_for_self_delimiting_extension ps_tls_type
| None -> (
match ext_ty with
| ET_unknown_extension_type _ -> (
match unk.self_delimiting_extension ext_ty with
| Some (|ty, ps_ty|) -> {typ = no_template_dep ty; parser = (fun _ -> ps_ty);}
| None -> default_one_ext_type
)
| _ -> default_one_ext_type
)
)
val compute_ext_type:
#bytes:Type0 -> {|bytes_like bytes|} ->
ctls_unknowns bytes ->
extension_origin ->
ctls_extensions_types bytes
let compute_ext_type #bytes #bl unk origin =
{
expected_ty = compute_ext_type_aux unk origin;
additional_ty = compute_ext_type_aux unk origin;
}
[@@ can_be_unit]
type ctls_extensions (bytes:Type0) {|bytes_like bytes|} (unk:ctls_unknowns bytes) (ext_orig:extension_origin) (t:ctls_template bytes) =
extensions_ctls_type (compute_ext_type unk ext_orig) (compute_ext_temp ext_orig) t
%splice [ps_ctls_extensions] (gen_parser (`ctls_extensions))
(*** Handshake messages ***)
/// struct {
/// Random random;
/// CipherSuite cipher_suites<1..2^16-1>;
/// Extension extensions<1..2^16-1>;
/// } ClientHello;
[@@ can_be_unit]
noeq
type ctls_client_hello (bytes:Type0) {|bytes_like bytes|} (unk:ctls_unknowns bytes) (t:ctls_template bytes) = {
random: ctls_random bytes t;
cipher_suites: ctls_cipher_suites bytes t;
extensions: ctls_extensions bytes unk ClientHello t;
}
%splice [ps_ctls_client_hello] (gen_parser (`ctls_client_hello))
/// struct {
/// Random random;
/// CipherSuite cipher_suite;
/// Extension extensions<1..2^16-1>;
/// } ServerHello;
[@@ can_be_unit]
noeq
type ctls_server_hello (bytes:Type0) {|bytes_like bytes|} (unk:ctls_unknowns bytes) (t:ctls_template bytes) = {
random: ctls_random bytes t;
cipher_suite: ctls_cipher_suite bytes t;
extensions: ctls_extensions bytes unk ServerHello t;
}
%splice [ps_ctls_server_hello] (gen_parser (`ctls_server_hello))
/// struct {
/// CipherSuite cipher_suite;
/// Extension extensions<2..2^16-1>;
/// } HelloRetryRequest;
[@@ can_be_unit]
noeq
type ctls_hello_retry_request (bytes:Type0) {|bytes_like bytes|} (unk:ctls_unknowns bytes) (t:ctls_template bytes) = {
cipher_suite: ctls_cipher_suite bytes t;
extensions: ctls_extensions bytes unk HelloRetryRequest t;
}
%splice [ps_ctls_hello_retry_request] (gen_parser (`ctls_hello_retry_request))
/// Compression of:
///
/// struct {
/// SignatureScheme algorithm;
/// opaque signature<0..2^16-1>;
/// } CertificateVerify;
[@@ can_be_unit]
noeq
type ctls_certificate_verify (bytes:Type0) {|bytes_like bytes|} (t:ctls_template bytes) = {
algorithm: ctls_certificate_verify_algorithm bytes t;
signature: ctls_certificate_verify_signature bytes t;
}
%splice [ps_ctls_certificate_verify] (gen_parser (`ctls_certificate_verify))
/// struct {
/// Extension extensions<0..2^16-1>;
/// } EncryptedExtensions;
[@@ can_be_unit]
noeq
type ctls_encrypted_extensions (bytes:Type0) {|bytes_like bytes|} (unk:ctls_unknowns bytes) (t:ctls_template bytes) = {
extensions: ctls_extensions bytes unk EncryptedExtensions t;
}
%splice [ps_ctls_encrypted_extensions] (gen_parser (`ctls_encrypted_extensions))
/// struct {
/// opaque certificate_request_context<0..2^8-1>;
/// Extension extensions<2..2^16-1>;
/// } CertificateRequest;
noeq
type ctls_certificate_request (bytes:Type0) {|bytes_like bytes|} (unk:ctls_unknowns bytes) (t:ctls_template bytes) = {
certificate_request_context: tls_bytes bytes (({min=0; max=(pow2 8)-1}));
extensions: ctls_extensions bytes unk CertificateRequest t;
}
%splice [ps_ctls_certificate_request] (gen_parser (`ctls_certificate_request))
/// When computing the handshake transcript,
/// all handshake messages are represented in TLS Handshake messages,
/// as in DTLS 1.3 ([RFC9147], Section 5.2), regardless of template.handshake_framing.
/// Custom message format to represent a Handshake inside a cTLS transcript
///
/// struct {
/// HandshakeType msg_type; /* handshake type */
/// uint24 length; /* bytes in message */
/// select (CTLSTranscriptHandshake.msg_type) {
/// case client_hello: ClientHello;
/// case server_hello: ServerHello;
/// case hello_retry_request: HelloRetryRequest; /* New */
/// case end_of_early_data: EndOfEarlyData;
/// case encrypted_extensions: EncryptedExtensions;
/// case certificate_request: CertificateRequest;
/// case certificate: Certificate;
/// case certificate_verify: CertificateVerify;
/// case finished: Finished;
/// case new_session_ticket: NewSessionTicket;
/// case key_update: KeyUpdate;
/// case request_connection_id: RequestConnectionId;
/// case new_connection_id: NewConnectionId;
/// };
/// } CTLSTranscriptHandshake;
val ctls_transcript_handshake_message:
bytes:Type0 -> {|bytes_like bytes|} ->
ctls_unknowns bytes ->
ctls_template bytes -> handshake_type ->
Type0
let ctls_transcript_handshake_message bytes #bl unk t htype =
match htype with
| HT_client_hello -> ctls_client_hello bytes unk t
| HT_server_hello -> ctls_server_hello bytes unk t
| HT_hello_retry_request_RESERVED -> ctls_hello_retry_request bytes unk t
| HT_end_of_early_data -> end_of_early_data
| HT_encrypted_extensions -> ctls_encrypted_extensions bytes unk t
| HT_certificate_request -> ctls_certificate_request bytes unk t
| HT_certificate -> certificate bytes
| HT_certificate_verify -> ctls_certificate_verify bytes t
| HT_finished -> finished bytes
| HT_new_session_ticket -> new_session_ticket bytes
| HT_key_update -> key_update bytes
| _ -> bytes
val ps_whole_ctls_transcript_handshake_message:
#bytes:Type0 -> {|bytes_like bytes|} ->
unk:ctls_unknowns bytes ->
t:ctls_template bytes -> htype:handshake_type ->
parser_serializer_whole bytes (ctls_transcript_handshake_message bytes unk t htype)
let ps_whole_ctls_transcript_handshake_message #bytes #bl unk t htype =
match htype with
| HT_client_hello -> ps_prefix_to_ps_whole (ps_ctls_client_hello unk t)
| HT_server_hello -> ps_prefix_to_ps_whole (ps_ctls_server_hello unk t)
| HT_hello_retry_request_RESERVED -> ps_prefix_to_ps_whole (ps_ctls_hello_retry_request unk t)
| HT_end_of_early_data -> ps_prefix_to_ps_whole ps_end_of_early_data
| HT_encrypted_extensions -> ps_prefix_to_ps_whole (ps_ctls_encrypted_extensions unk t)
| HT_certificate_request -> ps_prefix_to_ps_whole (ps_ctls_certificate_request unk t)
| HT_certificate -> ps_prefix_to_ps_whole ps_certificate
| HT_certificate_verify -> ps_prefix_to_ps_whole (ps_ctls_certificate_verify t)
| HT_finished -> ps_whole_finished
| HT_new_session_ticket -> ps_prefix_to_ps_whole ps_new_session_ticket
| HT_key_update -> ps_prefix_to_ps_whole ps_key_update
| _ -> ps_whole_bytes
type fixed_length_ctls_transcript_handshake_message (bytes:Type0) {|bytes_like bytes|} (unk:ctls_unknowns bytes) (t:ctls_template bytes) (htype:handshake_type) (length:nat) =
refined (ctls_transcript_handshake_message bytes unk t htype) (ps_whole_length_pred (ps_whole_ctls_transcript_handshake_message unk t htype) length)
val ps_fixed_length_ctls_transcript_handshake_message:
#bytes:Type0 -> {|bytes_like bytes|} ->
unk:ctls_unknowns bytes ->
t:ctls_template bytes -> htype:handshake_type -> length:nat ->
parser_serializer_prefix bytes (fixed_length_ctls_transcript_handshake_message bytes unk t htype length)
let ps_fixed_length_ctls_transcript_handshake_message #bytes #bl unk t htype length =
ps_whole_to_ps_prefix length (refine_whole (ps_whole_ctls_transcript_handshake_message unk t htype) (ps_whole_length_pred (ps_whole_ctls_transcript_handshake_message unk t htype) length))
noeq
type ctls_transcript_handshake (bytes:Type0) {|bytes_like bytes|} (unk:ctls_unknowns bytes) (t:ctls_template bytes) = {
msg_type: handshake_type;
length: nat_lbytes 3;
msg: fixed_length_ctls_transcript_handshake_message bytes unk t msg_type length;
}
%splice [ps_ctls_transcript_handshake] (gen_parser (`ctls_transcript_handshake))