From 444133549dd1cc072a94c9ba324f427acdc6f959 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Tue, 7 Jan 2025 11:24:23 +0100 Subject: [PATCH] chore: update F* and DY* --- flake.lock | 12 ++-- ....Crypto.Derived.Symbolic.SignWithLabel.fst | 70 ++++++++++--------- fstar/treemath/MLS.TreeMath.Internal.fst | 4 ++ ...LS.TreeSync.Symbolic.LeafNodeSignature.fst | 6 +- 4 files changed, 49 insertions(+), 43 deletions(-) diff --git a/flake.lock b/flake.lock index a88f58a..75b54de 100644 --- a/flake.lock +++ b/flake.lock @@ -36,11 +36,11 @@ ] }, "locked": { - "lastModified": 1732872022, - "narHash": "sha256-NzxnEUE3HjEe152T+ttCBb+PbHHtMgHZ8GGrYcHkMV8=", + "lastModified": 1736245409, + "narHash": "sha256-zh6HWSn4LbaTuD94UjfJXL1PbH5mVg7o3vncttCwyC4=", "owner": "REPROSEC", "repo": "dolev-yao-star-extrinsic", - "rev": "f3e40496fb1a3431323974baac3b46f316a78166", + "rev": "906bffb44d21beb7466719533d606d4bd396b3f7", "type": "github" }, "original": { @@ -72,11 +72,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1729012249, - "narHash": "sha256-8u6ceb4RpCJ1GMBen+9luyxc/YKU9im90zmsbb8hYt8=", + "lastModified": 1736182344, + "narHash": "sha256-kjD4Vf+nhV1P5ui1C63iRHcZgFn2yWPPC5G3GJKZVVs=", "owner": "FStarLang", "repo": "FStar", - "rev": "6e8b1573b5137c59004c715b229d5dfb4754adbf", + "rev": "7cb8a9b63fba47364dcaaf457bf8e7d2bb20506d", "type": "github" }, "original": { diff --git a/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst b/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst index 5fc399d..56bfcd4 100644 --- a/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst +++ b/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst @@ -15,17 +15,18 @@ open MLS.Result noeq type signwithlabel_crypto_pred {|crypto_usages|} = { - pred: trace -> sk_usg:usage{SigKey? sk_usg} -> msg:bytes -> prop; + pred: trace -> sk_usg:usage{SigKey? sk_usg} -> vk:bytes -> msg:bytes -> prop; pred_later: tr1:trace -> tr2:trace -> - sk_usg:usage{SigKey? sk_usg} -> msg:bytes -> + sk_usg:usage{SigKey? sk_usg} -> vk:bytes -> msg:bytes -> Lemma (requires - pred tr1 sk_usg msg /\ + pred tr1 sk_usg vk msg /\ + bytes_well_formed tr1 vk /\ bytes_well_formed tr1 msg /\ tr1 <$ tr2 ) - (ensures pred tr2 sk_usg msg) + (ensures pred tr2 sk_usg vk msg) ; } @@ -40,38 +41,38 @@ let split_signwithlabel_crypto_pred_params {|crypto_usages|}: split_function_par FStar.Classical.move_requires_2 get_mls_label_inj tag_set_1 tag_set_2 ); - tagged_data_t = (trace & (sk_usg:usage{SigKey? sk_usg}) & bytes); - raw_data_t = (trace & (sk_usg:usage{SigKey? sk_usg}) & bytes); + tagged_data_t = (trace & (sk_usg:usage{SigKey? sk_usg}) & bytes & bytes); + raw_data_t = (trace & (sk_usg:usage{SigKey? sk_usg}) & bytes & bytes); output_t = prop; - decode_tagged_data = (fun (tr, vk, data) -> ( + decode_tagged_data = (fun (tr, sk_usage, vk, data) -> ( match parse (sign_content_nt bytes) data with - | Some ({label; content}) -> Some (label, (tr, vk, content)) + | Some ({label; content}) -> Some (label, (tr, sk_usage, vk, content)) | None -> None )); local_fun_t = mk_dependent_type signwithlabel_crypto_pred; - global_fun_t = trace -> sk_usg:usage{SigKey? sk_usg} -> bytes -> prop; + global_fun_t = trace -> sk_usg:usage{SigKey? sk_usg} -> bytes -> bytes -> prop; - default_global_fun = (fun tr vk content -> False); + default_global_fun = (fun tr sk_usage 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_local_fun = (fun pred (tr, sk_usage, vk, content) -> pred.pred tr sk_usage vk content); + apply_global_fun = (fun pred (tr, sk_usage, vk, msg) -> pred tr sk_usage vk msg); + mk_global_fun = (fun pred tr sk_usage vk msg -> pred (tr, sk_usage, vk, msg)); apply_mk_global_fun = (fun _ _ -> ()); } #push-options "--ifuel 1" val has_signwithlabel_pred: {|crypto_usages|} -> sign_crypto_predicate -> (valid_label & signwithlabel_crypto_pred) -> prop let has_signwithlabel_pred #cusgs sign_pred (lab, local_pred) = - forall tr vk msg. - {:pattern sign_pred.pred tr vk msg} + forall tr sk_usage vk msg. + {:pattern sign_pred.pred tr sk_usage vk msg} match parse (sign_content_nt bytes) msg with | Some {label; content} -> ( label == get_mls_label lab ==> ( - sign_pred.pred tr vk msg == - local_pred.pred tr vk content + sign_pred.pred tr sk_usage vk msg == + local_pred.pred tr sk_usage vk content ) ) | _ -> True @@ -85,47 +86,48 @@ val intro_has_signwithlabel_pred: (ensures has_signwithlabel_pred sign_pred (tag, local_pred)) let intro_has_signwithlabel_pred #cusgs sign_pred tag local_pred = introduce - forall tr vk msg. + forall tr sk_usage vk msg. match parse (sign_content_nt bytes) msg with | Some {label; content} -> ( label == get_mls_label tag ==> ( - sign_pred.pred tr vk msg == - local_pred.pred tr vk content + sign_pred.pred tr sk_usage vk msg == + local_pred.pred tr sk_usage vk content ) ) | _ -> True with ( - has_local_fun_elim split_signwithlabel_crypto_pred_params sign_pred.pred tag local_pred (tr, vk, msg) + has_local_fun_elim split_signwithlabel_crypto_pred_params sign_pred.pred tag local_pred (tr, sk_usage, vk, msg) ) val mk_global_mls_sign_pred: {|crypto_usages|} -> list (valid_label & signwithlabel_crypto_pred) -> - trace -> sk_usg:usage{SigKey? sk_usg} -> bytes -> + trace -> sk_usg:usage{SigKey? sk_usg} -> bytes -> bytes -> prop -let mk_global_mls_sign_pred tagged_local_preds vk msg = - mk_global_fun split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) vk msg +let mk_global_mls_sign_pred tagged_local_preds sk_usage vk msg = + mk_global_fun split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) sk_usage vk msg #push-options "--ifuel 2" val mk_global_mls_sign_pred_later: {|crypto_usages|} -> tagged_local_preds:list (valid_label & signwithlabel_crypto_pred) -> tr1:trace -> tr2:trace -> - sk_usg:usage{SigKey? sk_usg} -> msg:bytes -> + sk_usg:usage{SigKey? sk_usg} -> vk:bytes -> msg:bytes -> Lemma (requires - mk_global_mls_sign_pred tagged_local_preds tr1 sk_usg msg /\ + mk_global_mls_sign_pred tagged_local_preds tr1 sk_usg vk msg /\ + bytes_well_formed tr1 vk /\ bytes_well_formed tr1 msg /\ tr1 <$ tr2 ) - (ensures mk_global_mls_sign_pred tagged_local_preds tr2 sk_usg msg) -let mk_global_mls_sign_pred_later tagged_local_preds tr1 tr2 sk_usg msg = - mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr1, sk_usg, msg); - mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr2, sk_usg, msg); + (ensures mk_global_mls_sign_pred tagged_local_preds tr2 sk_usg vk msg) +let mk_global_mls_sign_pred_later tagged_local_preds tr1 tr2 sk_usg vk msg = + mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr1, sk_usg, vk, msg); + mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr2, sk_usg, vk, msg); FStar.Classical.move_requires (parse_wf_lemma (sign_content_nt bytes) (bytes_well_formed tr1)) msg; - introduce forall tag_set lpred content. bytes_well_formed tr1 content /\ split_signwithlabel_crypto_pred_params.apply_local_fun lpred (tr1, sk_usg, content) ==> split_signwithlabel_crypto_pred_params.apply_local_fun #tag_set lpred (tr2, sk_usg, content) with ( + introduce forall tag_set lpred content. bytes_well_formed tr1 content /\ split_signwithlabel_crypto_pred_params.apply_local_fun lpred (tr1, sk_usg, vk, content) ==> split_signwithlabel_crypto_pred_params.apply_local_fun #tag_set lpred (tr2, sk_usg, vk, content) with ( introduce _ ==> _ with _. ( - lpred.pred_later tr1 tr2 sk_usg content + lpred.pred_later tr1 tr2 sk_usg vk content ) ) #pop-options @@ -180,7 +182,7 @@ val bytes_invariant_sign_with_label: sk `has_usage tr` mk_mls_sigkey_usage prin /\ nonce `has_usage tr` SigNonce /\ (get_label tr sk) `can_flow tr` (get_label tr nonce) /\ ( - spred.pred tr (mk_mls_sigkey_usage prin) msg + spred.pred tr (mk_mls_sigkey_usage prin) (vk sk) msg \/ get_label tr sk `can_flow tr` public ) /\ @@ -213,7 +215,7 @@ val bytes_invariant_verify_with_label: ) (ensures ( - spred.pred tr (mk_mls_sigkey_usage prin) content + spred.pred tr (mk_mls_sigkey_usage prin) vk content ) \/ ( (get_signkey_label tr vk) `can_flow tr` public ) diff --git a/fstar/treemath/MLS.TreeMath.Internal.fst b/fstar/treemath/MLS.TreeMath.Internal.fst index b42be86..b3f4efa 100644 --- a/fstar/treemath/MLS.TreeMath.Internal.fst +++ b/fstar/treemath/MLS.TreeMath.Internal.fst @@ -294,6 +294,7 @@ let get_bit_lemma x k = lemma_lemma q k; FStar.Math.Lemmas.small_mod (((q%2)*(pow2 k)) + (x%(pow2 k))) (pow2 (k+1)) +#push-options "--z3rlimit 500" val is_left_node_left: x:nat{level x <> 0} -> Lemma (is_left_node (left x) == true) let is_left_node_left x = //Z3 really has troube proving this inside the proof, hence this separate lemma @@ -312,7 +313,9 @@ let is_left_node_left x = is_left_node_lemma x xl q k; FStar.Math.Lemmas.small_div (x % (pow2 (k-1))) (pow2 k); FStar.Math.Lemmas.cancel_mul_mod q 2 +#pop-options +#push-options "--z3rlimit 500" val is_right_node_right: x:nat{level x <> 0} -> Lemma (is_left_node (right x) == false) let is_right_node_right x = //Z3 really has troube proving this inside the proof, hence this separate lemma @@ -334,6 +337,7 @@ let is_right_node_right x = assert (xr/(pow2 k) == 1 + 2*q); FStar.Math.Lemmas.lemma_mod_plus_distr_r 1 (2*q) 2; FStar.Math.Lemmas.cancel_mul_mod q 2 +#pop-options (*** Proofs: parent of left/right node ***) diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst index 7607b12..8c89faf 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst @@ -114,7 +114,7 @@ val leaf_node_sign_pred: {|crypto_usages|} -> treekem_types bytes -> signwithlabel_crypto_pred let leaf_node_sign_pred #cu tkt = { - pred = (fun tr sk_usg ln_tbs_bytes -> + pred = (fun tr sk_usg vk ln_tbs_bytes -> match (parse (leaf_node_tbs_nt bytes tkt) ln_tbs_bytes) with | None -> False | Some ln_tbs -> ( @@ -137,7 +137,7 @@ let leaf_node_sign_pred #cu tkt = { ) ) ); - pred_later = (fun tr1 tr2 vk ln_tbs_bytes -> + pred_later = (fun tr1 tr2 sk_usg vk ln_tbs_bytes -> parse_wf_lemma (leaf_node_tbs_nt bytes tkt) (bytes_well_formed tr1) ln_tbs_bytes; introduce forall prin tr group_id (tl:tree_list bytes tkt). tree_list_has_event prin tr group_id tl <==> (forall x. List.Tot.memP x tl ==> tree_has_event prin tr group_id x) with ( @@ -329,7 +329,7 @@ let parent_hash_implies_event #ci #tkt #l #i tr group_id t ast = serialize_wf_lemma (leaf_node_tbs_nt bytes tkt) (bytes_invariant tr) ln_tbs; bytes_invariant_verify_with_label (leaf_node_sign_pred tkt) tr authentifier ln.data.signature_key "LeafNodeTBS" ln_tbs_bytes ln.signature; - introduce ((leaf_node_sign_pred tkt).pred tr (mk_mls_sigkey_usage authentifier) ln_tbs_bytes) ==> tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|) + introduce ((leaf_node_sign_pred tkt).pred tr (mk_mls_sigkey_usage authentifier) ln.data.signature_key ln_tbs_bytes) ==> tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|) with _. ( ( parse_serialize_inv_lemma #bytes (leaf_node_tbs_nt bytes tkt) ln_tbs;