From b3e4f94bba4a29fb0bb9640c42d25c7a9d2def55 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Wed, 24 Jul 2024 19:22:01 +0200 Subject: [PATCH] chore: update DY* --- Makefile | 2 +- flake.lock | 6 +++--- fstar/symbolic/MLS.Symbolic.fst | 4 ++-- .../MLS.TreeSync.Symbolic.API.Sessions.fst | 8 ++++---- .../symbolic/MLS.TreeSync.Symbolic.API.fst | 4 ++-- .../MLS.TreeSync.Symbolic.AuthServiceCache.fst | 2 +- .../symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst | 14 ++++++++------ .../MLS.TreeSync.Symbolic.LeafNodeSignature.fst | 8 ++++---- 8 files changed, 25 insertions(+), 23 deletions(-) diff --git a/Makefile b/Makefile index d56281a..ac3a8ba 100644 --- a/Makefile +++ b/Makefile @@ -11,7 +11,7 @@ INNER_SOURCE_DIRS = api bootstrap common/code common/proofs glue/code glue/proof HACL_SNAPSHOT_DIR = $(MLS_HOME)/hacl-star-snapshot SOURCE_DIRS = $(addprefix $(MLS_HOME)/fstar/, $(INNER_SOURCE_DIRS)) -DY_INCLUDE_DIRS = core lib lib/comparse lib/event lib/state lib/utils +DY_INCLUDE_DIRS = core lib lib/comparse lib/crypto lib/event lib/state lib/utils INCLUDE_DIRS = $(SOURCE_DIRS) $(HACL_SNAPSHOT_DIR)/lib $(HACL_SNAPSHOT_DIR)/specs $(COMPARSE_HOME)/src $(if $(USE_DY), $(addprefix $(DY_HOME)/src/, $(DY_INCLUDE_DIRS))) FSTAR_INCLUDE_DIRS = $(addprefix --include , $(INCLUDE_DIRS)) diff --git a/flake.lock b/flake.lock index ea39fd7..3a89133 100644 --- a/flake.lock +++ b/flake.lock @@ -36,11 +36,11 @@ ] }, "locked": { - "lastModified": 1721649266, - "narHash": "sha256-M5zka8Ig1K/XY4SxeiOL0G4jQrrOM7YQtuA6A329Vg8=", + "lastModified": 1721816292, + "narHash": "sha256-3J+AQxreaQ634uRwg0a8QplRxnkI0GsSHupMAtMtCfM=", "owner": "REPROSEC", "repo": "dolev-yao-star-extrinsic", - "rev": "ee46696a0c4ac9789c72d12e3234f429388303d3", + "rev": "b220103634a70e3a847d55f96ddc167cb4c6d474", "type": "github" }, "original": { diff --git a/fstar/symbolic/MLS.Symbolic.fst b/fstar/symbolic/MLS.Symbolic.fst index f319db4..7df814a 100644 --- a/fstar/symbolic/MLS.Symbolic.fst +++ b/fstar/symbolic/MLS.Symbolic.fst @@ -159,7 +159,7 @@ let split_sign_pred_params {|crypto_usages|}: split_function_parameters = { val has_sign_pred: crypto_invariants -> (valid_label & mls_sign_pred) -> prop let has_sign_pred ci (lab, spred) = - has_local_fun split_sign_pred_params (sign_pred #ci) (lab, spred) + has_local_fun split_sign_pred_params ((sign_pred #ci).pred) (lab, spred) #push-options "--z3rlimit 25" val bytes_invariant_sign_with_label: @@ -258,7 +258,7 @@ val mk_sign_pred_correct: ci:crypto_invariants -> lspred:list (valid_label & mls_sign_pred) -> Lemma (requires - sign_pred == mk_sign_pred lspred /\ + sign_pred.pred == mk_sign_pred lspred /\ List.Tot.no_repeats_p (List.Tot.map fst lspred) ) (ensures for_allP (has_sign_pred ci) lspred) diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst index c66626a..ea422fb 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst @@ -222,7 +222,7 @@ instance parseable_serializeable_treesync_private_state: parseable_serializeable val treesync_private_state_pred: {|crypto_invariants|} -> local_state_predicate treesync_private_state let treesync_private_state_pred #ci = { pred = (fun tr prin state_id st -> - is_signature_key "MLS.LeafSignKey" (principal_label prin) tr st.signature_key + is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key ); pred_later = (fun tr1 tr2 prin state_id st -> ()); pred_knowable = (fun tr prin state_id st -> ()); @@ -254,7 +254,7 @@ val new_private_treesync_state_proof: tr:trace -> Lemma (requires - is_signature_key "MLS.LeafSignKey" (principal_label prin) tr st.signature_key /\ + is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key /\ trace_invariant tr /\ has_treesync_private_state_invariant invs ) @@ -276,7 +276,7 @@ val set_private_treesync_state_proof: tr:trace -> Lemma (requires - is_signature_key "MLS.LeafSignKey" (principal_label prin) tr st.signature_key /\ + is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key /\ trace_invariant tr /\ has_treesync_private_state_invariant invs ) @@ -307,7 +307,7 @@ val get_private_treesync_state_proof: match opt_result with | None -> True | Some st -> - is_signature_key "MLS.LeafSignKey" (principal_label prin) tr st.signature_key + is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key ) )) let get_private_treesync_state_proof #invs prin state_id tr = () diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst index e960294..6040dd6 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst @@ -494,7 +494,7 @@ val create_signature_keypair: p:principal -> traceful (option (state_id & signature_public_key_nt dy_bytes)) let create_signature_keypair p = - let* signature_key = mk_rand (SigKey "MLS.LeafSignKey") (principal_label p) 32 in + let* signature_key = mk_rand (SigKey "MLS.LeafSignKey" empty) (principal_label p) 32 in let verification_key = vk signature_key in guard (length (signature_key <: dy_bytes) < pow2 30);*? guard (length (verification_key <: dy_bytes) < pow2 30);*? @@ -517,7 +517,7 @@ val create_signature_keypair_proof: match opt_res with | None -> True | Some (private_si, verification_key) -> - is_verification_key "MLS.LeafSignKey" (principal_label p) tr_out verification_key + is_verification_key (SigKey "MLS.LeafSignKey" empty) (principal_label p) tr_out verification_key ) )) let create_signature_keypair_proof #invs p tr = () diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst index 63d8b44..5de4842 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst @@ -43,7 +43,7 @@ let as_cache_pred #ci = { value.time <= DY.Core.Trace.Type.length tr /\ is_publishable (prefix tr value.time) key.verification_key /\ get_signkey_label key.verification_key == principal_label value.who /\ - get_signkey_usage key.verification_key == SigKey value.usg /\ + get_signkey_usage key.verification_key == SigKey value.usg empty /\ is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_publishable (prefix tr value.time)) key.credential ); pred_later = (fun tr1 tr2 prin state_id key value -> ()); diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst index b84a374..a839b40 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst @@ -27,10 +27,12 @@ let all_sign_preds tkt = [ val treesync_crypto_predicates: treekem_types dy_bytes -> crypto_predicates treesync_crypto_usages let treesync_crypto_predicates tkt = { default_crypto_predicates treesync_crypto_usages with - sign_pred = mk_sign_pred (all_sign_preds tkt); - sign_pred_later = (fun tr1 tr2 vk msg -> - mk_sign_pred_later (all_sign_preds tkt) tr1 tr2 vk msg - ); + sign_pred = { + pred = mk_sign_pred (all_sign_preds tkt); + pred_later = (fun tr1 tr2 vk msg -> + mk_sign_pred_later (all_sign_preds tkt) tr1 tr2 vk msg + ); + } } instance treesync_crypto_invariants (tkt:treekem_types dy_bytes): crypto_invariants = { @@ -49,7 +51,7 @@ let all_state_predicates tkt = [ val treesync_trace_invariants: tkt:treekem_types dy_bytes -> trace_invariants (treesync_crypto_invariants tkt) let treesync_trace_invariants tkt = { - state_pred = mk_state_predicate (treesync_crypto_invariants tkt) (all_state_predicates tkt); + state_pred = mk_state_pred (treesync_crypto_invariants tkt) (all_state_predicates tkt); event_pred = mk_event_pred []; } @@ -78,7 +80,7 @@ let treesync_global_usage_has_leaf_node_tbs_invariant tkt = val all_state_predicates_has_all_state_predicates: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate (treesync_protocol_invariants tkt)) (all_state_predicates tkt))) let all_state_predicates_has_all_state_predicates tkt = assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_state_predicates tkt))); - mk_global_local_bytes_state_predicate_correct (treesync_protocol_invariants tkt) (all_state_predicates tkt); + mk_state_pred_correct (treesync_protocol_invariants tkt) (all_state_predicates tkt); norm_spec [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate (treesync_protocol_invariants tkt)) (all_state_predicates tkt)) val treesync_protocol_invariants_has_as_cache_invariant: tkt:treekem_types dy_bytes -> Lemma diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst index 561ff36..fbba620 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst @@ -46,7 +46,7 @@ let dy_asp #ci tr = { credential_ok = (fun (vk, cred) token -> token.time <= (DY.Core.Trace.Type.length tr) /\ bytes_invariant (prefix tr token.time) vk /\ - get_signkey_usage vk == SigKey "MLS.LeafSignKey" /\ + get_signkey_usage vk == SigKey "MLS.LeafSignKey" empty /\ get_signkey_label vk == principal_label token.who ); valid_successor = (fun (vk_old, cred_old) (vk_new, cred_new) -> @@ -657,7 +657,7 @@ val is_msg_external_path_to_path: is_well_formed _ (is_knowable_by label tr) t /\ is_well_formed _ (is_knowable_by label tr) p /\ is_knowable_by label tr group_id /\ - bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" /\ + bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" empty /\ bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\ get_label sk == principal_label prin /\ get_label nonce == principal_label prin /\ @@ -713,7 +713,7 @@ val is_msg_sign_leaf_node_data_key_package: Success? (sign_leaf_node_data_key_package ln_data sk nonce) /\ leaf_node_has_event prin tr ({data = ln_data; group_id = (); leaf_index = ();}) /\ is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_knowable_by label tr) ln_data /\ - bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" /\ + bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" empty /\ bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\ get_label sk == principal_label prin /\ get_label nonce == principal_label prin /\ @@ -743,7 +743,7 @@ val is_msg_sign_leaf_node_data_update: tree_has_event prin tr group_id (|0, (leaf_index <: nat), TLeaf (Some ({data = ln_data; signature = empty #dy_bytes;} <: leaf_node_nt dy_bytes tkt))|) /\ is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_knowable_by label tr) ln_data /\ is_knowable_by label tr group_id /\ - bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" /\ + bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" empty /\ bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\ get_label sk == principal_label prin /\ get_label nonce == principal_label prin /\