From f57dc7d109e9d189616f8bea9522e8fe470d15d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Mon, 22 Jul 2024 16:26:46 +0200 Subject: [PATCH] chore: update F* and DY* --- flake.lock | 12 +++--- fstar/symbolic/MLS.Symbolic.fst | 72 ++++++++++++++++++--------------- 2 files changed, 45 insertions(+), 39 deletions(-) diff --git a/flake.lock b/flake.lock index e2cad64..ea39fd7 100644 --- a/flake.lock +++ b/flake.lock @@ -36,11 +36,11 @@ ] }, "locked": { - "lastModified": 1716558569, - "narHash": "sha256-pZ/O9UslWHEJDRHfitlvkWy/Tu89iF/PlF4r0znpBjw=", + "lastModified": 1721649266, + "narHash": "sha256-M5zka8Ig1K/XY4SxeiOL0G4jQrrOM7YQtuA6A329Vg8=", "owner": "REPROSEC", "repo": "dolev-yao-star-extrinsic", - "rev": "32994e43100e7d915c48e4ed25e60acfb3a28339", + "rev": "ee46696a0c4ac9789c72d12e3234f429388303d3", "type": "github" }, "original": { @@ -72,11 +72,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1710871305, - "narHash": "sha256-4bqvrVXX8JVlvswJx9apdVJu/HvoAEVsYxGI8IZt14s=", + "lastModified": 1721552334, + "narHash": "sha256-FDfp4JquvP5e4obYdG7hpe5hwMOTxYwe4ArtNXKHvcY=", "owner": "FStarLang", "repo": "FStar", - "rev": "41299bb12072a7475c036262b9851f7cdc287387", + "rev": "e5cef6f266ece8a8b55ef4cd9b61cdf103520d38", "type": "github" }, "original": { diff --git a/fstar/symbolic/MLS.Symbolic.fst b/fstar/symbolic/MLS.Symbolic.fst index 89dce41..f319db4 100644 --- a/fstar/symbolic/MLS.Symbolic.fst +++ b/fstar/symbolic/MLS.Symbolic.fst @@ -4,7 +4,7 @@ open Comparse open DY.Core open MLS.Crypto open MLS.NetworkTypes -open DY.Lib.SplitPredicate +open DY.Lib.SplitFunction open MLS.Result #push-options "--fuel 0 --ifuel 0" @@ -124,34 +124,42 @@ type mls_sign_pred {|crypto_usages|} = { ; } -let split_sign_pred_func {|crypto_usages|}: split_predicate_input_values = { - local_pred = mls_sign_pred; - global_pred = trace -> verif_key_t -> dy_bytes -> prop; +let split_sign_pred_params {|crypto_usages|}: split_function_parameters = { + tag_set_t = valid_label; + tag_t = mls_ascii_string; + is_disjoint = unequal; + tag_belong_to = (fun tag tag_set -> + tag = get_mls_label tag_set + ); + cant_belong_to_disjoint_sets = (fun tag tag_set_1 tag_set_2 -> + FStar.Classical.move_requires_2 get_mls_label_inj tag_set_1 tag_set_2 + ); - raw_data_t = (trace & verif_key_t & dy_bytes); tagged_data_t = (trace & verif_key_t & dy_bytes); - - apply_local_pred = (fun pred (tr, vk, content) -> pred.pred tr vk content); - apply_global_pred = (fun pred (tr, vk, msg) -> pred tr vk msg); - mk_global_pred = (fun pred tr vk msg -> pred (tr, vk, msg)); - apply_mk_global_pred = (fun _ _ -> ()); - - tag_t = valid_label; - encoded_tag_t = mls_ascii_string; - - encode_tag = get_mls_label; - encode_tag_inj = get_mls_label_inj; + raw_data_t = (trace & verif_key_t & dy_bytes); + output_t = prop; decode_tagged_data = (fun (tr, key, data) -> ( match parse (sign_content_nt dy_bytes) data with | Some ({label; content}) -> Some (label, (tr, key, content)) | None -> None )); + + local_fun_t = mls_sign_pred; + global_fun_t = trace -> verif_key_t -> dy_bytes -> prop; + + default_global_fun = (fun tr vk content -> False); + + + apply_local_fun = (fun pred (tr, vk, content) -> pred.pred tr vk content); + apply_global_fun = (fun pred (tr, vk, msg) -> pred tr vk msg); + mk_global_fun = (fun pred tr vk msg -> pred (tr, vk, msg)); + apply_mk_global_fun = (fun _ _ -> ()); } val has_sign_pred: crypto_invariants -> (valid_label & mls_sign_pred) -> prop let has_sign_pred ci (lab, spred) = - has_local_pred split_sign_pred_func (sign_pred #ci) (lab, spred) + has_local_fun split_sign_pred_params (sign_pred #ci) (lab, spred) #push-options "--z3rlimit 25" val bytes_invariant_sign_with_label: @@ -180,7 +188,7 @@ let bytes_invariant_sign_with_label #ci spred tr sk lab msg nonce = serialize_wf_lemma (sign_content_nt dy_bytes) (bytes_invariant tr) sign_content; serialize_wf_lemma (sign_content_nt dy_bytes) (is_knowable_by (get_label msg) tr) sign_content; let sign_content_bytes = serialize _ sign_content in - assert(split_sign_pred_func.decode_tagged_data (tr, (vk sk), sign_content_bytes) == Some (split_sign_pred_func.encode_tag lab, (tr, (vk sk), msg))) + assert(split_sign_pred_params.decode_tagged_data (tr, (vk sk), sign_content_bytes) == Some (get_mls_label lab, (tr, (vk sk), msg))) #pop-options val bytes_invariant_verify_with_label: @@ -210,7 +218,7 @@ let bytes_invariant_verify_with_label #ci spred tr vk lab content signature = serialize_wf_lemma (sign_content_nt dy_bytes) (bytes_invariant tr) sign_content; let sign_content_bytes = serialize _ sign_content in if SigKey? (get_signkey_usage vk) then - assert(split_sign_pred_func.decode_tagged_data (tr, vk, sign_content_bytes) == Some (split_sign_pred_func.encode_tag lab, (tr, vk, content))) + assert(split_sign_pred_params.decode_tagged_data (tr, vk, sign_content_bytes) == Some (get_mls_label lab, (tr, vk, content))) else () val mk_sign_pred: @@ -219,7 +227,7 @@ val mk_sign_pred: trace -> verif_key_t -> dy_bytes -> prop let mk_sign_pred l tr key msg = - mk_global_pred split_sign_pred_func l tr key msg + mk_global_fun split_sign_pred_params l tr key msg #push-options "--ifuel 1" val mk_sign_pred_later: @@ -234,18 +242,15 @@ val mk_sign_pred_later: ) (ensures mk_sign_pred lspred tr2 vk msg) let mk_sign_pred_later lspred tr1 tr2 vk msg = - mk_global_pred_eq split_sign_pred_func lspred (tr1, vk, msg); - eliminate exists tag spred raw_data. - List.Tot.memP (tag, spred) lspred /\ - split_sign_pred_func.apply_local_pred spred raw_data /\ - split_sign_pred_func.decode_tagged_data (tr1, vk, msg) == Some (split_sign_pred_func.encode_tag tag, raw_data) - returns mk_sign_pred lspred tr2 vk msg - with _. ( - let Some (_, (_, _, msg_sub)) = split_sign_pred_func.decode_tagged_data (tr1, vk, msg) in - spred.pred_later tr1 tr2 vk msg_sub; - mk_global_pred_eq split_sign_pred_func lspred (tr2, vk, msg); - assert(split_sign_pred_func.apply_local_pred spred (tr2, vk, msg_sub)) - ) + mk_global_fun_eq split_sign_pred_params lspred (tr1, vk, msg); + mk_global_fun_eq split_sign_pred_params lspred (tr2, vk, msg); + + introduce forall lpred content. split_sign_pred_params.apply_local_fun lpred (tr1, vk, content) ==> split_sign_pred_params.apply_local_fun lpred (tr2, vk, content) with ( + introduce _ ==> _ with _. lpred.pred_later tr1 tr2 vk content + ); + match parse (sign_content_nt dy_bytes) msg with + | Some _ -> () + | None -> () #pop-options #push-options "--ifuel 1" @@ -259,5 +264,6 @@ val mk_sign_pred_correct: (ensures for_allP (has_sign_pred ci) lspred) let mk_sign_pred_correct ci lspred = for_allP_eq (has_sign_pred ci) lspred; - FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_pred_correct split_sign_pred_func lspred)) + no_repeats_p_implies_for_all_pairsP_unequal (List.Tot.map fst lspred); + FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_sign_pred_params lspred)) #pop-options