@@ -42,13 +42,52 @@ prop_tls_hs_encode_decode() ->
4242 ? FORALL ({Handshake , TLSVersion }, ? LET (Version , tls_version (), {tls_msg (Version ), Version }),
4343 try
4444 [Type , _Length , Data ] = tls_handshake :encode_handshake (Handshake , TLSVersion ),
45- tls_handshake :decode_handshake (TLSVersion , Type , Data ) == Handshake
45+ DecHandshake = tls_handshake :decode_handshake (TLSVersion , Type , Data ),
46+ RawHandshke = raw_handshake (DecHandshake ),
47+ RawHandshke == Handshake
4648 catch
4749 throw :# alert {} ->
4850 true
4951 end
5052 ).
5153
54+ raw_handshake (# client_hello {extensions = Ext } = Hello ) ->
55+ NewExt = raw_ext (Ext ),
56+ Hello # client_hello {extensions = NewExt };
57+ raw_handshake (Handshake ) ->
58+ Handshake .
59+
60+ % % binder_length is saved in decode because we need it later to
61+ % % truncates client hello in handshake history, but it is not defined
62+ % % as part of the handshake record but calculated at TLS record
63+ % % layer. So we want to "unset" it for being able to have a simple
64+ % % property for encoding/decoding testing. Same goes for hybrid
65+ % % key_exchange where the decode functions splits the key-share into
66+ % % the two individual key-share values to use.
67+ raw_ext (Exts0 ) ->
68+ Exts = case maps :get (pre_shared_key , Exts0 , undefined ) of
69+ # pre_shared_key_client_hello {} = PSKCH ->
70+ NewPSKCH = PSKCH # pre_shared_key_client_hello {binder_length = undefined },
71+ Exts0 #{pre_shared_key => NewPSKCH };
72+ _ ->
73+ Exts0
74+ end ,
75+ case maps :get (key_share , Exts , undefined ) of
76+ # key_share_client_hello {client_shares = CShares } ->
77+ NewCShares = [# key_share_entry {group = G , key_exchange = raw_kex (G , Kex )}
78+ || # key_share_entry {group = G , key_exchange = Kex } <- CShares ],
79+ Exts #{key_share => # key_share_client_hello {client_shares = NewCShares }};
80+ _ ->
81+ Exts
82+ end .
83+
84+ raw_kex (Group , {Bin1 , Bin2 }) when Group == x25519mlkem768 ;
85+ Group == secp256r1mlkem768 ;
86+ Group == secp384r1mlkem1024 ->
87+ <<Bin1 /binary , Bin2 /binary >>;
88+ raw_kex (_ , Kex ) ->
89+ Kex .
90+
5291% %--------------------------------------------------------------------
5392% % Message Generators -----------------------------------------------
5493% %--------------------------------------------------------------------
@@ -249,8 +288,8 @@ pre_shared_keyextension() ->
249288extensions (? TLS_1_3 = Version , MsgType = client_hello ) ->
250289 ? LET ({
251290 ServerName ,
252- % % MaxFragmentLength,
253- % % StatusRequest,
291+ MaxFragmentLength ,
292+ StatusRequest ,
254293 SupportedGroups ,
255294 SignatureAlgorithms ,
256295 UseSrtp ,
@@ -263,19 +302,19 @@ extensions(?TLS_1_3 = Version, MsgType = client_hello) ->
263302 KeyShare ,
264303 PreSharedKey ,
265304 PSKKeyExchangeModes ,
266- % % EarlyData,
267- % % Cookie,
305+ EarlyData ,
306+ Cookie ,
268307 SupportedVersions ,
269308 CertAuthorities ,
270309 % % PostHandshakeAuth,
271310 SignatureAlgorithmsCert
272311 },
273312 {
274313 oneof ([server_name (), undefined ]),
275- % % oneof([max_fragment_length(), undefined]),
276- % % oneof([status_request(), undefined]),
314+ oneof ([max_fragment_length (), undefined ]),
315+ oneof ([status_request (), undefined ]),
277316 oneof ([supported_groups (Version ), undefined ]),
278- oneof ([signature_algs (Version ), undefined ]),
317+ oneof ([signature_algs (Version )]),
279318 oneof ([use_srtp (), undefined ]),
280319 % % oneof([heartbeat(), undefined]),
281320 oneof ([alpn (), undefined ]),
@@ -286,8 +325,8 @@ extensions(?TLS_1_3 = Version, MsgType = client_hello) ->
286325 oneof ([key_share (MsgType ), undefined ]),
287326 oneof ([pre_shared_key (MsgType ), undefined ]),
288327 oneof ([psk_key_exchange_modes (), undefined ]),
289- % % oneof([early_data (), undefined]),
290- % % oneof([cookie(), undefined]),
328+ oneof ([early_data_indication (), undefined ]),
329+ oneof ([cookie (), undefined ]),
291330 oneof ([client_hello_versions (Version )]),
292331 oneof ([cert_auths (), undefined ]),
293332 % % oneof([post_handshake_auth(), undefined]),
@@ -300,8 +339,8 @@ extensions(?TLS_1_3 = Version, MsgType = client_hello) ->
300339 end ,
301340 #{
302341 sni => ServerName ,
303- % % max_fragment_length => MaxFragmentLength,
304- % % status_request => StatusRequest,
342+ max_frag_enum => MaxFragmentLength ,
343+ status_request => StatusRequest ,
305344 elliptic_curves => SupportedGroups ,
306345 signature_algs => SignatureAlgorithms ,
307346 use_srtp => UseSrtp ,
@@ -314,8 +353,8 @@ extensions(?TLS_1_3 = Version, MsgType = client_hello) ->
314353 key_share => KeyShare ,
315354 pre_shared_key => PreSharedKey ,
316355 psk_key_exchange_modes => PSKKeyExchangeModes ,
317- % % early_data => EarlyData,
318- % % cookie => Cookie,
356+ early_data => EarlyData ,
357+ cookie => Cookie ,
319358 client_hello_versions => SupportedVersions ,
320359 certificate_authorities => CertAuthorities ,
321360 % % post_handshake_auth => PostHandshakeAuth,
@@ -402,25 +441,25 @@ extensions(Version, server_hello) ->
402441extensions (? TLS_1_3 = Version , encrypted_extensions ) ->
403442 ? LET ({
404443 ServerName ,
405- % % MaxFragmentLength,
444+ MaxFragmentLength ,
406445 SupportedGroups ,
407- % % UseSrtp,
446+ UseSrtp ,
408447 % % Heartbeat,
409- ALPN
448+ ALPN ,
410449 % % ClientCertiticateType,
411450 % % ServerCertificateType,
412- % % EarlyData
451+ EarlyData
413452 },
414453 {
415454 oneof ([server_name (), undefined ]),
416- % % oneof([max_fragment_length(), undefined]),
455+ oneof ([max_fragment_length (), undefined ]),
417456 oneof ([supported_groups (Version ), undefined ]),
418- % % oneof([use_srtp(), undefined]),
457+ oneof ([use_srtp (), undefined ]),
419458 % % oneof([heartbeat(), undefined]),
420- oneof ([alpn (), undefined ])
459+ oneof ([alpn (), undefined ]),
421460 % % oneof([client_cert_type(), undefined]),
422461 % % oneof([server_cert_type(), undefined]),
423- % % oneof([early_data (), undefined])
462+ oneof ([early_data_indication (), undefined ])
424463 },
425464 maps :filter (fun (_ , undefined ) ->
426465 false ;
@@ -429,21 +468,35 @@ extensions(?TLS_1_3 = Version, encrypted_extensions) ->
429468 end ,
430469 #{
431470 sni => ServerName ,
432- % % max_fragment_length => MaxFragmentLength,
471+ max_frag_enum => MaxFragmentLength ,
433472 elliptic_curves => SupportedGroups ,
434- % % use_srtp => UseSrtp,
473+ use_srtp => UseSrtp ,
435474 % % heartbeat => Heartbeat,
436- alpn => ALPN
475+ alpn => ALPN ,
437476 % % client_cert_type => ClientCertificateType,
438477 % % server_cert_type => ServerCertificateType,
439- % % early_data => EarlyData
478+ early_data => EarlyData
440479 })).
441480
442481server_name () ->
443482 ? LET (ServerName , sni (),
444483 ServerName ).
445484 % % sni().
446485
486+ max_fragment_length () ->
487+ ? LET (Enum , elements ([1 ,2 ,3 ,4 ]), # max_frag_enum {enum = Enum }).
488+
489+ status_request () ->
490+ % % TODO real impl
491+ undefined .
492+
493+ early_data_indication () ->
494+ elements ([# early_data_indication {}, # early_data_indication_nst {indication = 500 }]).
495+
496+ cookie () ->
497+ % % TODO real impl
498+ undefined .
499+
447500signature_algs_cert () ->
448501 ? LET (List , sig_scheme_list (),
449502 # signature_algorithms_cert {signature_scheme_list = List }).
@@ -471,7 +524,7 @@ sig_scheme_list() ->
471524 rsa_pss_pss_sha256 ,
472525 rsa_pss_pss_sha384 ,
473526 rsa_pss_pss_sha512 ,
474- rsa_pkcs1_sha1 ,
527+ rsa_pkcs1_sha1 ,
475528 ecdsa_sha1 ]
476529 ]).
477530
0 commit comments