diff --git a/fstar/symbolic/MLS.Symbolic.fst b/fstar/symbolic/MLS.Symbolic.fst index 2decdc6..f3d6ca5 100644 --- a/fstar/symbolic/MLS.Symbolic.fst +++ b/fstar/symbolic/MLS.Symbolic.fst @@ -9,12 +9,9 @@ open MLS.Result (*** Typeclass instantiation on DY* ***) -val dy_bytes: eqtype -let dy_bytes = DY.Core.bytes - #push-options "--ifuel 1" -val dy_bytes_has_crypto: available_ciphersuite -> crypto_bytes dy_bytes -let dy_bytes_has_crypto acs = { +val bytes_has_crypto_bytes: available_ciphersuite -> crypto_bytes bytes +let bytes_has_crypto_bytes acs = { base = DY.Lib.bytes_like_bytes; bytes_hasEq = (); @@ -82,7 +79,7 @@ let dy_bytes_has_crypto acs = { ); string_to_bytes = (fun s -> - (ps_whole_ascii_string.serialize s <: dy_bytes) + (ps_whole_ascii_string.serialize s <: bytes) ); unsafe_split = (fun buf i -> @@ -96,7 +93,7 @@ let dy_bytes_has_crypto acs = { } #pop-options -instance crypto_dy_bytes: crypto_bytes dy_bytes = dy_bytes_has_crypto AC_mls_128_dhkemx25519_chacha20poly1305_sha256_ed25519 +instance crypto_bytes_bytes: crypto_bytes bytes = bytes_has_crypto_bytes AC_mls_128_dhkemx25519_chacha20poly1305_sha256_ed25519 type mls_principal = { who: principal; diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst index 5c8ca8b..fbb001f 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst @@ -46,7 +46,7 @@ let extract_result #a x = | MLS.Result.ProtocolError s -> return None #pop-options -val has_treesync_invariants: treekem_types dy_bytes -> {|protocol_invariants|} -> prop +val has_treesync_invariants: treekem_types bytes -> {|protocol_invariants|} -> prop let has_treesync_invariants tkt #invs = has_treesync_public_state_invariant tkt /\ has_treesync_signature_key_state_invariant /\ @@ -57,7 +57,7 @@ let has_treesync_invariants tkt #invs = val get_token_for: p:principal -> as_session:state_id -> - inp:as_input dy_bytes -> + inp:as_input bytes -> traceful (option dy_as_token) let get_token_for p as_session (verification_key, credential) = let*? { token } = find_verified_credential p as_session ({ verification_key; credential; }) in @@ -66,7 +66,7 @@ let get_token_for p as_session (verification_key, credential) = val get_token_for_proof: {|protocol_invariants|} -> p:principal -> as_session:state_id -> - inp:as_input dy_bytes -> + inp:as_input bytes -> tr:trace -> Lemma (requires @@ -90,7 +90,7 @@ let get_token_for_proof #invs p as_session (verification_key, credential) tr = ( #push-options "--fuel 1 --ifuel 1" val get_tokens_for: p:principal -> as_session:state_id -> - inps:list (option (as_input dy_bytes)) -> + inps:list (option (as_input bytes)) -> traceful (option (l:list (option dy_as_token){List.Tot.length l == List.Tot.length inps})) let rec get_tokens_for p as_session inps = match inps with @@ -112,7 +112,7 @@ let rec get_tokens_for p as_session inps = val get_tokens_for_proof: {|protocol_invariants|} -> p:principal -> as_session:state_id -> - inps:list (option (as_input dy_bytes)) -> + inps:list (option (as_input bytes)) -> tr:trace -> Lemma (requires @@ -148,12 +148,12 @@ let rec get_tokens_for_proof #invs p as_session inps tr = (*** Process proposals ***) val create: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> as_session:state_id -> gmgr_session:state_id -> - group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> secret_session:state_id -> + group_id:mls_bytes bytes -> ln:leaf_node_nt bytes tkt -> secret_session:state_id -> traceful (option unit) let create #tkt p as_session gmgr_session group_id ln secret_session = - let*? create_pend = extract_result (prepare_create #dy_bytes #crypto_dy_bytes group_id ln) in + let*? create_pend = extract_result (prepare_create #bytes #crypto_bytes_bytes group_id ln) in let*? token = get_token_for p as_session (create_pend.as_input) in let st = finalize_create create_pend token in let* si_public = new_public_treesync_state p st in @@ -164,9 +164,9 @@ let create #tkt p as_session gmgr_session group_id ln secret_session = #push-options "--z3rlimit 25" val create_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> as_session:state_id -> gmgr_session:state_id -> - group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> secret_session:state_id -> + group_id:mls_bytes bytes -> ln:leaf_node_nt bytes tkt -> secret_session:state_id -> tr:trace -> Lemma (requires @@ -180,7 +180,7 @@ val create_proof: trace_invariant tr_out )) let create_proof #invs #tkt p as_session gmgr_session group_id ln secret_session tr = - let (opt_create_pend, tr) = extract_result (prepare_create #dy_bytes #crypto_dy_bytes group_id ln) tr in + let (opt_create_pend, tr) = extract_result (prepare_create #bytes #crypto_bytes_bytes group_id ln) tr in match opt_create_pend with | None -> () | Some create_pend -> ( @@ -195,13 +195,13 @@ let create_proof #invs #tkt p as_session gmgr_session group_id ln secret_session #pop-options val welcome: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> as_session:state_id -> gmgr_session:state_id -> kpmgr_session:state_id -> - my_key_package:key_package_nt dy_bytes tkt -> - group_id:mls_bytes dy_bytes -> l:nat -> t:treesync dy_bytes tkt l 0 -> + my_key_package:key_package_nt bytes tkt -> + group_id:mls_bytes bytes -> l:nat -> t:treesync bytes tkt l 0 -> traceful (option unit) let welcome #tkt p as_session gmgr_session kpmgr_session my_key_package group_id l t = - let*? welcome_pend = extract_result (prepare_welcome #dy_bytes #crypto_dy_bytes group_id t) in + let*? welcome_pend = extract_result (prepare_welcome #bytes #crypto_bytes_bytes group_id t) in welcome_pend.as_inputs_proof; let*? tokens = get_tokens_for p as_session welcome_pend.as_inputs in let st = finalize_welcome welcome_pend tokens in @@ -212,10 +212,10 @@ let welcome #tkt p as_session gmgr_session kpmgr_session my_key_package group_id val welcome_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> as_session:state_id -> gmgr_session:state_id -> kpmgr_session:state_id -> - my_key_package:key_package_nt dy_bytes tkt -> - group_id:mls_bytes dy_bytes -> l:nat -> t:treesync dy_bytes tkt l 0 -> + my_key_package:key_package_nt bytes tkt -> + group_id:mls_bytes bytes -> l:nat -> t:treesync bytes tkt l 0 -> tr:trace -> Lemma (requires @@ -229,7 +229,7 @@ val welcome_proof: trace_invariant tr_out )) let welcome_proof #invs #tkt p as_session gmgr_session kpmgr_session my_key_package group_id l t tr = - let (opt_welcome_pend, tr) = extract_result (prepare_welcome #dy_bytes #crypto_dy_bytes group_id t) tr in + let (opt_welcome_pend, tr) = extract_result (prepare_welcome #bytes #crypto_bytes_bytes group_id t) tr in match opt_welcome_pend with | None -> () | Some welcome_pend -> ( @@ -253,9 +253,9 @@ let welcome_proof #invs #tkt p as_session gmgr_session kpmgr_session my_key_pack ) val add: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> as_session:state_id -> gmgr_session:state_id -> - group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> + group_id:mls_bytes bytes -> ln:leaf_node_nt bytes tkt -> traceful (option nat) let add #tkt p as_session gmgr_session group_id ln = let*? group_session = find_group_sessions p gmgr_session { group_id } in @@ -268,9 +268,9 @@ let add #tkt p as_session gmgr_session group_id ln = val add_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> as_session:state_id -> gmgr_session:state_id -> - group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> + group_id:mls_bytes bytes -> ln:leaf_node_nt bytes tkt -> tr:trace -> Lemma (requires @@ -312,9 +312,9 @@ let add_proof #invs #tkt p as_session gmgr_session group_id ln tr = ) val update: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> as_session:state_id -> gmgr_session:state_id -> - group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> li:nat -> + group_id:mls_bytes bytes -> ln:leaf_node_nt bytes tkt -> li:nat -> traceful (option unit) let update #tkt p as_session gmgr_session group_id ln li = let*? group_session = find_group_sessions p gmgr_session { group_id } in @@ -328,9 +328,9 @@ let update #tkt p as_session gmgr_session group_id ln li = val update_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> as_session:state_id -> gmgr_session:state_id -> - group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> li:nat -> + group_id:mls_bytes bytes -> ln:leaf_node_nt bytes tkt -> li:nat -> tr:trace -> Lemma (requires @@ -370,9 +370,9 @@ let update_proof #invs #tkt p as_session gmgr_session group_id ln li tr = ) val remove: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> as_session:state_id -> gmgr_session:state_id -> - group_id:mls_bytes dy_bytes -> li:nat -> + group_id:mls_bytes bytes -> li:nat -> traceful (option unit) let remove #tkt p as_session gmgr_session group_id li = let*? group_session = find_group_sessions p gmgr_session { group_id } in @@ -385,9 +385,9 @@ let remove #tkt p as_session gmgr_session group_id li = val remove_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> as_session:state_id -> gmgr_session:state_id -> - group_id:mls_bytes dy_bytes -> li:nat -> + group_id:mls_bytes bytes -> li:nat -> tr:trace -> Lemma (requires @@ -421,9 +421,9 @@ let remove_proof #invs #tkt p as_session gmgr_session group_id li tr = ) val commit: - #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 -> + #tkt:treekem_types bytes -> #l:nat -> #li:leaf_index l 0 -> p:principal -> as_session:state_id -> gmgr_session:state_id -> - group_id:mls_bytes dy_bytes -> path:pathsync dy_bytes tkt l 0 li -> + group_id:mls_bytes bytes -> path:pathsync bytes tkt l 0 li -> traceful (option unit) let commit #tkt #l #li p as_session gmgr_session group_id path = let*? group_session = find_group_sessions p gmgr_session { group_id } in @@ -438,9 +438,9 @@ let commit #tkt #l #li p as_session gmgr_session group_id path = #push-options "--z3rlimit 100" val commit_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 -> + #tkt:treekem_types bytes -> #l:nat -> #li:leaf_index l 0 -> p:principal -> as_session:state_id -> gmgr_session:state_id -> - group_id:mls_bytes dy_bytes -> path:pathsync dy_bytes tkt l 0 li -> + group_id:mls_bytes bytes -> path:pathsync bytes tkt l 0 li -> tr:trace -> Lemma (requires @@ -495,12 +495,12 @@ let commit_proof #invs #tkt #l #li p as_session gmgr_session group_id path tr = val create_signature_keypair: p:principal -> - traceful (option (state_id & signature_public_key_nt dy_bytes)) + traceful (option (state_id & signature_public_key_nt bytes)) let create_signature_keypair p = let* private_si = mk_signature_key p in let*? verification_key = get_signature_key_vk p private_si in - guard (length (verification_key <: dy_bytes) < pow2 30);*? - return (Some (private_si, (verification_key <: signature_public_key_nt dy_bytes))) + guard (length (verification_key <: bytes) < pow2 30);*? + return (Some (private_si, (verification_key <: signature_public_key_nt bytes))) val create_signature_keypair_proof: {|protocol_invariants|} -> @@ -525,10 +525,10 @@ let create_signature_keypair_proof #invs p tr = () (*** Sign stuff ***) val external_path_has_event_later: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> #l:nat -> #li:leaf_index l 0 -> prin:principal -> tr1:trace -> tr2:trace -> - t:treesync dy_bytes tkt l 0 -> p:external_pathsync dy_bytes tkt l 0 li -> group_id:mls_bytes dy_bytes -> + t:treesync bytes tkt l 0 -> p:external_pathsync bytes tkt l 0 li -> group_id:mls_bytes bytes -> Lemma (requires external_path_has_event prin tr1 t p group_id /\ @@ -536,18 +536,18 @@ val external_path_has_event_later: ) (ensures external_path_has_event prin tr2 t p group_id) let external_path_has_event_later #tkt #l #li prin tr1 tr2 t p group_id = - let Success auth_p = external_path_to_path_nosig #dy_bytes #crypto_dy_bytes t p group_id in - path_is_parent_hash_valid_external_path_to_path_nosig #dy_bytes #crypto_dy_bytes t p group_id; - apply_path_aux_compute_leaf_parent_hash_from_path_both_succeed #dy_bytes #crypto_dy_bytes t auth_p (MLS.TreeSync.ParentHash.root_parent_hash #dy_bytes); - for_allP_eq (tree_has_event prin tr1 group_id) (path_to_tree_list #dy_bytes #crypto_dy_bytes t auth_p); - for_allP_eq (tree_has_event prin tr2 group_id) (path_to_tree_list #dy_bytes #crypto_dy_bytes t auth_p) + let Success auth_p = external_path_to_path_nosig #bytes #crypto_bytes_bytes t p group_id in + path_is_parent_hash_valid_external_path_to_path_nosig #bytes #crypto_bytes_bytes t p group_id; + apply_path_aux_compute_leaf_parent_hash_from_path_both_succeed #bytes #crypto_bytes_bytes t auth_p (MLS.TreeSync.ParentHash.root_parent_hash #bytes); + for_allP_eq (tree_has_event prin tr1 group_id) (path_to_tree_list #bytes #crypto_bytes_bytes t auth_p); + for_allP_eq (tree_has_event prin tr2 group_id) (path_to_tree_list #bytes #crypto_bytes_bytes t auth_p) #push-options "--z3rlimit 25" val authenticate_path: - #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 -> + #tkt:treekem_types bytes -> #l:nat -> #li:leaf_index l 0 -> p:principal -> gmgr_session:state_id -> - group_id:mls_bytes dy_bytes -> tree:treesync dy_bytes tkt l 0 -> path:external_pathsync dy_bytes tkt l 0 li{(get_path_leaf path).source == LNS_update} -> - traceful (option (pathsync dy_bytes tkt l 0 li)) + group_id:mls_bytes bytes -> tree:treesync bytes tkt l 0 -> path:external_pathsync bytes tkt l 0 li{(get_path_leaf path).source == LNS_update} -> + traceful (option (pathsync bytes tkt l 0 li)) let authenticate_path #tkt #l p gmgr_session group_id tree path = let* signature_nonce = mk_rand SigNonce secret 32 in let*? group_session = find_group_sessions p gmgr_session { group_id } in @@ -556,18 +556,18 @@ let authenticate_path #tkt #l p gmgr_session group_id tree path = guard (group_id = group_id');*? guard (l = st.levels);*? guard (tree = st.tree);*? - guard (length (signature_nonce <: dy_bytes) >= sign_sign_min_entropy_length #dy_bytes);*? - guard (path_is_filter_valid #dy_bytes #crypto_dy_bytes tree path);*? - let*? auth_path = extract_result (external_path_to_path #dy_bytes #crypto_dy_bytes tree path group_id signature_key signature_nonce) in + guard (length (signature_nonce <: bytes) >= sign_sign_min_entropy_length #bytes);*? + guard (path_is_filter_valid #bytes #crypto_bytes_bytes tree path);*? + let*? auth_path = extract_result (external_path_to_path #bytes #crypto_bytes_bytes tree path group_id signature_key signature_nonce) in return (Some auth_path) #pop-options #push-options "--z3rlimit 50" val authenticate_path_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 -> + #tkt:treekem_types bytes -> #l:nat -> #li:leaf_index l 0 -> p:principal -> gmgr_session:state_id -> - group_id:mls_bytes dy_bytes -> tree:treesync dy_bytes tkt l 0 -> path:external_pathsync dy_bytes tkt l 0 li -> + group_id:mls_bytes bytes -> tree:treesync bytes tkt l 0 -> path:external_pathsync bytes tkt l 0 li -> tr:trace -> Lemma (requires @@ -603,11 +603,11 @@ let authenticate_path_proof #invs #tkt #l p gmgr_session group_id tree path tr = if not (group_id = group_id') then () else if not (l = st.levels) then () else if not (tree = st.tree) then () - else if not (length (signature_nonce <: dy_bytes) >= sign_sign_min_entropy_length #dy_bytes) then () - else if not (path_is_filter_valid #dy_bytes #crypto_dy_bytes tree path) then () - else if not (length (signature_nonce <: dy_bytes) >= sign_sign_min_entropy_length #dy_bytes) then () + else if not (length (signature_nonce <: bytes) >= sign_sign_min_entropy_length #bytes) then () + else if not (path_is_filter_valid #bytes #crypto_bytes_bytes tree path) then () + else if not (length (signature_nonce <: bytes) >= sign_sign_min_entropy_length #bytes) then () else ( - let (opt_auth_path, tr) = extract_result (external_path_to_path #dy_bytes #crypto_dy_bytes tree path group_id signature_key signature_nonce) tr in + let (opt_auth_path, tr) = extract_result (external_path_to_path #bytes #crypto_bytes_bytes tree path group_id signature_key signature_nonce) tr in match opt_auth_path with | None -> () | Some auth_path -> ( @@ -623,24 +623,24 @@ let authenticate_path_proof #invs #tkt #l p gmgr_session group_id tree path tr = #pop-options val authenticate_leaf_node_data_from_key_package: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> si_private:state_id -> - ln_data:leaf_node_data_nt dy_bytes tkt{ln_data.source == LNS_key_package} -> - traceful (option (leaf_node_nt dy_bytes tkt)) + ln_data:leaf_node_data_nt bytes tkt{ln_data.source == LNS_key_package} -> + traceful (option (leaf_node_nt bytes tkt)) let authenticate_leaf_node_data_from_key_package #tkt p si_private ln_data = let* signature_nonce = mk_rand SigNonce secret 32 in let*? signature_key = get_signature_key_sk p si_private in - guard (length (signature_nonce <: dy_bytes) = sign_sign_min_entropy_length #dy_bytes);*? - extract_result (sign_leaf_node_data_key_package #dy_bytes #crypto_dy_bytes ln_data signature_key signature_nonce) + guard (length (signature_nonce <: bytes) = sign_sign_min_entropy_length #bytes);*? + extract_result (sign_leaf_node_data_key_package #bytes #crypto_bytes_bytes ln_data signature_key signature_nonce) #push-options "--z3rlimit 25" val authenticate_leaf_node_data_from_key_package_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> si_private:state_id -> - ln_data:leaf_node_data_nt dy_bytes tkt{ln_data.source == LNS_key_package} -> + ln_data:leaf_node_data_nt bytes tkt{ln_data.source == LNS_key_package} -> tr:trace -> Lemma (requires @@ -665,9 +665,9 @@ let authenticate_leaf_node_data_from_key_package_proof #invs #tkt p si_private match opt_signature_key with | None -> () | Some signature_key -> ( - if not (length (signature_nonce <: dy_bytes) = sign_sign_min_entropy_length #dy_bytes) then () + if not (length (signature_nonce <: bytes) = sign_sign_min_entropy_length #bytes) then () else ( - let (opt_res, tr) = extract_result (sign_leaf_node_data_key_package #dy_bytes #crypto_dy_bytes ln_data signature_key signature_nonce) tr in + let (opt_res, tr) = extract_result (sign_leaf_node_data_key_package #bytes #crypto_bytes_bytes ln_data signature_key signature_nonce) tr in match opt_res with | None -> () | Some res -> ( @@ -679,31 +679,31 @@ let authenticate_leaf_node_data_from_key_package_proof #invs #tkt p si_private #pop-options val authenticate_leaf_node_data_from_update: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> si_private:state_id -> - ln_data:leaf_node_data_nt dy_bytes tkt{ln_data.source == LNS_update} -> group_id:mls_bytes dy_bytes -> leaf_index:nat_lbytes 4 -> - traceful (option (leaf_node_nt dy_bytes tkt)) + ln_data:leaf_node_data_nt bytes tkt{ln_data.source == LNS_update} -> group_id:mls_bytes bytes -> leaf_index:nat_lbytes 4 -> + traceful (option (leaf_node_nt bytes tkt)) let authenticate_leaf_node_data_from_update #tkt p si_private ln_data group_id leaf_index = let* signature_nonce = mk_rand SigNonce secret 32 in let*? signature_key = get_signature_key_sk p si_private in - guard (length (signature_nonce <: dy_bytes) >= sign_sign_min_entropy_length #dy_bytes);*? - extract_result (sign_leaf_node_data_update #dy_bytes #crypto_dy_bytes ln_data group_id leaf_index signature_key signature_nonce) + guard (length (signature_nonce <: bytes) >= sign_sign_min_entropy_length #bytes);*? + extract_result (sign_leaf_node_data_update #bytes #crypto_bytes_bytes ln_data group_id leaf_index signature_key signature_nonce) #push-options "--z3rlimit 25" val authenticate_leaf_node_data_from_update_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> si_private:state_id -> - ln_data:leaf_node_data_nt dy_bytes tkt{ln_data.source == LNS_update} -> group_id:mls_bytes dy_bytes -> leaf_index:nat_lbytes 4 -> + ln_data:leaf_node_data_nt bytes tkt{ln_data.source == LNS_update} -> group_id:mls_bytes bytes -> leaf_index:nat_lbytes 4 -> tr:trace -> Lemma (requires is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_publishable tr) ln_data /\ is_publishable tr group_id /\ leaf_node_has_event p tr ({data = ln_data; group_id; leaf_index;}) /\ - tree_has_event p tr group_id (|0, leaf_index, TLeaf (Some ({data = ln_data; signature = empty #dy_bytes;} <: leaf_node_nt dy_bytes tkt))|) /\ + tree_has_event p tr group_id (|0, leaf_index, TLeaf (Some ({data = ln_data; signature = empty #bytes;} <: leaf_node_nt bytes tkt))|) /\ trace_invariant tr /\ has_treesync_invariants tkt ) @@ -723,9 +723,9 @@ let authenticate_leaf_node_data_from_update_proof #invs #tkt p si_private ln_dat match opt_signature_key with | None -> () | Some signature_key -> ( - if not (length (signature_nonce <: dy_bytes) >= sign_sign_min_entropy_length #dy_bytes) then () + if not (length (signature_nonce <: bytes) >= sign_sign_min_entropy_length #bytes) then () else ( - let (opt_res, tr) = extract_result (sign_leaf_node_data_update #dy_bytes #crypto_dy_bytes ln_data group_id leaf_index signature_key signature_nonce) tr in + let (opt_res, tr) = extract_result (sign_leaf_node_data_update #bytes #crypto_bytes_bytes ln_data group_id leaf_index signature_key signature_nonce) tr in match opt_res with | None -> () | Some res -> ( @@ -740,9 +740,9 @@ let authenticate_leaf_node_data_from_update_proof #invs #tkt p si_private ln_dat #push-options "--ifuel 1" val trigger_tree_list_event: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> - group_id:mls_bytes dy_bytes -> tl:tree_list dy_bytes tkt -> + group_id:mls_bytes bytes -> tl:tree_list bytes tkt -> traceful unit let rec trigger_tree_list_event #tkt p group_id tl = match tl with @@ -754,9 +754,9 @@ let rec trigger_tree_list_event #tkt p group_id tl = #pop-options val trigger_tree_list_event_lemma: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> tr:trace -> - group_id:mls_bytes dy_bytes -> h:(l:nat & i:tree_index l & treesync dy_bytes tkt l i) -> t:tree_list dy_bytes tkt -> + group_id:mls_bytes bytes -> h:(l:nat & i:tree_index l & treesync bytes tkt l i) -> t:tree_list bytes tkt -> Lemma(tree_list_has_event p tr group_id (h::t) <==> (tree_has_event p tr group_id h /\ tree_list_has_event p tr group_id t)) let trigger_tree_list_event_lemma #tkt p tr group_id h t = let open FStar.Tactics in @@ -771,10 +771,10 @@ let trigger_tree_list_event_lemma #tkt p tr group_id h t = #push-options "--ifuel 1 --fuel 1 --z3rlimit 10" val trigger_tree_list_event_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> - group_has_event_pred: event_predicate (group_has_tree_event dy_bytes tkt) -> + #tkt:treekem_types bytes -> + group_has_event_pred: event_predicate (group_has_tree_event bytes tkt) -> p:principal -> - group_id:mls_bytes dy_bytes -> tl:tree_list dy_bytes tkt -> + group_id:mls_bytes bytes -> tl:tree_list bytes tkt -> tr:trace -> Lemma (requires @@ -793,7 +793,7 @@ let rec trigger_tree_list_event_proof #invs #tkt group_has_event_pred p group_id | [] -> normalize_term_spec (tree_list_has_event p tr group_id tl) | tl_head::tl_tail -> ( // There is a problem in the SMT encoding, hence we need to bamboozle F* like this. - let lem (x:group_has_tree_event dy_bytes tkt): Lemma (tr <$ snd (trigger_event p x tr)) = () in + let lem (x:group_has_tree_event bytes tkt): Lemma (tr <$ snd (trigger_event p x tr)) = () in lem (mk_group_has_tree_event group_id tl_head); // Similarly, this lemma should be triggered by SMT patterns. // Looks like F* do not like `mk_group_has_tree_event group_id tl_head` @@ -806,19 +806,19 @@ let rec trigger_tree_list_event_proof #invs #tkt group_has_event_pred p group_id #pop-options val trigger_leaf_node_event: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> p:principal -> - ln_tbs:leaf_node_tbs_nt dy_bytes tkt -> + ln_tbs:leaf_node_tbs_nt bytes tkt -> traceful unit let trigger_leaf_node_event #tkt p ln_tbs = trigger_event p ln_tbs val trigger_leaf_node_event_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> - leaf_node_has_event_pred: event_predicate (leaf_node_tbs_nt dy_bytes tkt) -> + #tkt:treekem_types bytes -> + leaf_node_has_event_pred: event_predicate (leaf_node_tbs_nt bytes tkt) -> p:principal -> - ln_tbs:leaf_node_tbs_nt dy_bytes tkt -> + ln_tbs:leaf_node_tbs_nt bytes tkt -> tr:trace -> Lemma (requires diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst index 582a7cb..ef4de61 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst @@ -11,7 +11,7 @@ open MLS.Symbolic #set-options "--fuel 0 --ifuel 0" -[@@ with_bytes dy_bytes] +[@@ with_bytes bytes] type dy_as_token = { time: nat; } @@ -22,7 +22,7 @@ type dy_as_token = { /// Instantiation of the abstract "Authentication Service" for DY*. /// The token is a a timestamp, /// and the AS attests that the signature verification key belonged to that principal at that time. -val dy_asp: {|crypto_invariants|} -> trace -> as_parameters dy_bytes +val dy_asp: {|crypto_invariants|} -> trace -> as_parameters bytes let dy_asp #ci tr = { token_t = dy_as_token; credential_ok = (fun (vk, cred) token -> diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst index be5c37c..745e5f8 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst @@ -22,32 +22,32 @@ open MLS.TreeSync.Symbolic.API instance treesync_crypto_usages: crypto_usages = default_crypto_usages -val all_signwithlabel_preds: treekem_types dy_bytes -> list (valid_label & signwithlabel_crypto_pred) +val all_signwithlabel_preds: treekem_types bytes -> list (valid_label & signwithlabel_crypto_pred) let all_signwithlabel_preds tkt = [ leaf_node_tbs_tag_and_invariant tkt; ] -val mls_sign_pred: treekem_types dy_bytes -> sign_crypto_predicate +val mls_sign_pred: treekem_types bytes -> sign_crypto_predicate let mls_sign_pred tkt = mk_mls_sign_pred (all_signwithlabel_preds tkt) -val all_sign_preds: treekem_types dy_bytes -> list (string & sign_crypto_predicate) +val all_sign_preds: treekem_types bytes -> list (string & sign_crypto_predicate) let all_sign_preds tkt = [ ("MLS.LeafSignKey", mls_sign_pred tkt) ] -val treesync_crypto_predicates: treekem_types dy_bytes -> crypto_predicates +val treesync_crypto_predicates: treekem_types bytes -> crypto_predicates let treesync_crypto_predicates tkt = { default_crypto_predicates with sign_pred = mk_sign_predicate (all_sign_preds tkt); } -instance treesync_crypto_invariants (tkt:treekem_types dy_bytes): crypto_invariants = { +instance treesync_crypto_invariants (tkt:treekem_types bytes): crypto_invariants = { usages = treesync_crypto_usages; preds = treesync_crypto_predicates tkt; } -val all_state_predicates: tkt:treekem_types dy_bytes -> list (dtuple2 string local_bytes_state_predicate) +val all_state_predicates: tkt:treekem_types bytes -> list (dtuple2 string local_bytes_state_predicate) let all_state_predicates tkt = [ as_cache_tag_and_invariant; group_manager_tag_and_invariant; @@ -56,13 +56,13 @@ let all_state_predicates tkt = [ treesync_signature_key_state_tag_and_invariant ] -val treesync_trace_invariants: tkt:treekem_types dy_bytes -> trace_invariants +val treesync_trace_invariants: tkt:treekem_types bytes -> trace_invariants let treesync_trace_invariants tkt = { state_pred = mk_state_pred (all_state_predicates tkt); event_pred = mk_event_pred []; } -instance treesync_protocol_invariants (tkt:treekem_types dy_bytes): protocol_invariants = { +instance treesync_protocol_invariants (tkt:treekem_types bytes): protocol_invariants = { crypto_invs = treesync_crypto_invariants tkt; trace_invs = treesync_trace_invariants tkt; } @@ -70,7 +70,7 @@ instance treesync_protocol_invariants (tkt:treekem_types dy_bytes): protocol_inv (*** Proofs ***) #push-options "--ifuel 1 --fuel 1" -val all_signwithlabel_preds_has_all_signwithlabel_preds: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_signwithlabel_preds; `%for_allP]; iota; zeta] (for_allP (has_signwithlabel_pred (mls_sign_pred tkt)) (all_signwithlabel_preds tkt))) +val all_signwithlabel_preds_has_all_signwithlabel_preds: tkt:treekem_types bytes -> Lemma (norm [delta_only [`%all_signwithlabel_preds; `%for_allP]; iota; zeta] (for_allP (has_signwithlabel_pred (mls_sign_pred tkt)) (all_signwithlabel_preds tkt))) let all_signwithlabel_preds_has_all_signwithlabel_preds tkt = assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_signwithlabel_preds tkt))); mk_mls_sign_pred_correct (mls_sign_pred tkt) (all_signwithlabel_preds tkt); @@ -78,20 +78,20 @@ let all_signwithlabel_preds_has_all_signwithlabel_preds tkt = #pop-options #push-options "--ifuel 1 --fuel 1" -val all_sign_preds_has_all_sign_preds: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP has_sign_predicate (all_sign_preds tkt))) +val all_sign_preds_has_all_sign_preds: tkt:treekem_types bytes -> Lemma (norm [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP has_sign_predicate (all_sign_preds tkt))) let all_sign_preds_has_all_sign_preds tkt = assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_sign_preds tkt))); mk_sign_predicate_correct (all_sign_preds tkt); norm_spec [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP has_sign_predicate (all_sign_preds tkt)) #pop-options -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 (all_state_predicates tkt))) +val all_state_predicates_has_all_state_predicates: tkt:treekem_types bytes -> Lemma (norm [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP has_local_bytes_state_predicate (all_state_predicates tkt))) let all_state_predicates_has_all_state_predicates tkt = assert_norm(List.Tot.no_repeats_p (List.Tot.map dfst (all_state_predicates tkt))); mk_state_pred_correct (all_state_predicates tkt); norm_spec [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP has_local_bytes_state_predicate (all_state_predicates tkt)) -val treesync_protocol_invariants_has_has_treesync_invariants: tkt:treekem_types dy_bytes -> Lemma +val treesync_protocol_invariants_has_has_treesync_invariants: tkt:treekem_types bytes -> Lemma (has_treesync_invariants tkt) [SMTPat (has_treesync_invariants tkt)] let treesync_protocol_invariants_has_has_treesync_invariants tkt = diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst index 01a7b57..7607b12 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst @@ -32,12 +32,12 @@ open MLS.Result (*** Predicates ***) -instance event_leaf_node_event (tkt:treekem_types dy_bytes): event (leaf_node_tbs_nt dy_bytes tkt) = +instance event_leaf_node_event (tkt:treekem_types bytes): event (leaf_node_tbs_nt bytes tkt) = mk_event_instance "MLS.TreeSync.LeafNodeEvent" val leaf_node_has_event: - #tkt:treekem_types dy_bytes -> - principal -> trace -> leaf_node_tbs_nt dy_bytes tkt -> + #tkt:treekem_types bytes -> + principal -> trace -> leaf_node_tbs_nt bytes tkt -> prop let leaf_node_has_event #tkt prin tr ln_tbs = event_triggered tr prin ln_tbs @@ -69,13 +69,13 @@ let tree_has_event_arithmetic_lemma l i = ) #pop-options -instance event_group_has_tree_event (tkt:treekem_types dy_bytes): event (group_has_tree_event dy_bytes tkt) = +instance event_group_has_tree_event (tkt:treekem_types bytes): event (group_has_tree_event bytes tkt) = mk_event_instance "MLS.TreeSync.GroupHasTreeEvent" val mk_group_has_tree_event: - #tkt:treekem_types dy_bytes -> - mls_bytes dy_bytes -> (l:nat & i:tree_index l & treesync dy_bytes tkt l i) -> - group_has_tree_event dy_bytes tkt + #tkt:treekem_types bytes -> + mls_bytes bytes -> (l:nat & i:tree_index l & treesync bytes tkt l i) -> + group_has_tree_event bytes tkt let mk_group_has_tree_event #tkt group_id (|l, i, t|) = tree_has_event_arithmetic_lemma l i; { @@ -86,17 +86,17 @@ let mk_group_has_tree_event #tkt group_id (|l, i, t|) = } val tree_has_event: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> principal -> trace -> - mls_bytes dy_bytes -> (l:nat & i:tree_index l & treesync dy_bytes tkt l i) -> + mls_bytes bytes -> (l:nat & i:tree_index l & treesync bytes tkt l i) -> prop let tree_has_event #tkt prin tr group_id (|l, i, t|) = event_triggered tr prin (mk_group_has_tree_event group_id (|l, i, t|)) val tree_list_has_event: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> principal -> trace -> - mls_bytes dy_bytes -> tree_list dy_bytes tkt -> + mls_bytes bytes -> tree_list bytes tkt -> prop let tree_list_has_event #tkt prin tr group_id tl = for_allP (tree_has_event prin tr group_id) tl @@ -111,11 +111,11 @@ let leaf_node_label = "LeafNodeTBS" /// furthermore one event "GroupHasTreeEvent" was triggered for each of these trees. #push-options "--fuel 0 --z3rlimit 25" val leaf_node_sign_pred: - {|crypto_usages|} -> treekem_types dy_bytes -> + {|crypto_usages|} -> treekem_types bytes -> signwithlabel_crypto_pred let leaf_node_sign_pred #cu tkt = { pred = (fun tr sk_usg ln_tbs_bytes -> - match (parse (leaf_node_tbs_nt dy_bytes tkt) ln_tbs_bytes) with + match (parse (leaf_node_tbs_nt bytes tkt) ln_tbs_bytes) with | None -> False | Some ln_tbs -> ( exists prin. @@ -123,7 +123,7 @@ let leaf_node_sign_pred #cu tkt = { leaf_node_has_event prin tr ln_tbs /\ ( match ln_tbs.data.source with | LNS_commit -> ( - exists (tl: tree_list dy_bytes tkt). + exists (tl: tree_list bytes tkt). tree_list_starts_with_tbs tl ln_tbs_bytes /\ tree_list_is_parent_hash_linkedP tl /\ tree_list_ends_at_root tl /\ @@ -131,15 +131,15 @@ let leaf_node_sign_pred #cu tkt = { tree_list_has_event prin tr ln_tbs.group_id tl ) | LNS_update -> ( - tree_has_event prin tr ln_tbs.group_id (|0, ln_tbs.leaf_index, TLeaf (Some ({data = ln_tbs.data; signature = empty #dy_bytes;} <: leaf_node_nt dy_bytes tkt))|) + tree_has_event prin tr ln_tbs.group_id (|0, ln_tbs.leaf_index, TLeaf (Some ({data = ln_tbs.data; signature = empty #bytes;} <: leaf_node_nt bytes tkt))|) ) | LNS_key_package -> True ) ) ); pred_later = (fun tr1 tr2 vk ln_tbs_bytes -> - parse_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (bytes_well_formed tr1) ln_tbs_bytes; - introduce forall prin tr group_id (tl:tree_list dy_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) + 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 ( for_allP_eq (tree_has_event prin tr group_id) tl ) @@ -147,11 +147,11 @@ let leaf_node_sign_pred #cu tkt = { } #pop-options -val leaf_node_tbs_tag_and_invariant: {|crypto_usages|} -> treekem_types dy_bytes -> (valid_label & signwithlabel_crypto_pred) +val leaf_node_tbs_tag_and_invariant: {|crypto_usages|} -> treekem_types bytes -> (valid_label & signwithlabel_crypto_pred) let leaf_node_tbs_tag_and_invariant #cu tkt = (leaf_node_label, leaf_node_sign_pred tkt) val has_leaf_node_tbs_invariant: - treekem_types dy_bytes -> {|crypto_invariants|} -> + treekem_types bytes -> {|crypto_invariants|} -> prop let has_leaf_node_tbs_invariant tkt #ci = has_mls_signwithlabel_pred (leaf_node_tbs_tag_and_invariant tkt) @@ -216,9 +216,9 @@ let rec tree_list_head_subtree_tail #bytes #cb #tkt tl = ) val get_authentifier_index: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> #l:nat -> #i:tree_index l -> - t:treesync dy_bytes tkt l i -> + t:treesync bytes tkt l i -> Pure (leaf_index l i) (requires unmerged_leaves_ok t /\ @@ -283,10 +283,10 @@ let rec is_well_formed_leaf_at #bytes #bl #tkt #l #i pre t li = #push-options "--z3rlimit 100" val parent_hash_implies_event: {|crypto_invariants|} -> - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> #l:nat -> #i:tree_index l -> tr:trace -> - group_id:mls_bytes dy_bytes -> t:treesync dy_bytes tkt l i -> ast:as_tokens dy_bytes (dy_asp tr).token_t l i -> + group_id:mls_bytes bytes -> t:treesync bytes tkt l i -> ast:as_tokens bytes (dy_asp tr).token_t l i -> Lemma (requires has_leaf_node_tbs_invariant tkt /\ @@ -316,7 +316,7 @@ let parent_hash_implies_event #ci #tkt #l #i tr group_id t ast = leaf_at_subtree_leaf leaf t; leaf_at_valid_leaves group_id t leaf_i; let TLeaf (Some ln) = leaf in - let ln_tbs: leaf_node_tbs_nt dy_bytes tkt = { + let ln_tbs: leaf_node_tbs_nt bytes tkt = { data = ln.data; group_id = group_id; leaf_index = leaf_i; @@ -326,15 +326,15 @@ let parent_hash_implies_event #ci #tkt #l #i tr group_id t ast = let authentifier_li = leaf_i in let authentifier = (Some?.v (credential_to_principal (Some?.v (leaf_at t authentifier_li)).data.credential)) in let leaf_sk_label = principal_label authentifier in - serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (bytes_invariant tr) ln_tbs; + 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)|) with _. ( ( - parse_serialize_inv_lemma #dy_bytes (leaf_node_tbs_nt dy_bytes tkt) ln_tbs; + parse_serialize_inv_lemma #bytes (leaf_node_tbs_nt bytes tkt) ln_tbs; - eliminate exists (leaf_tl: tree_list dy_bytes tkt). + eliminate exists (leaf_tl: tree_list bytes tkt). tree_list_starts_with_tbs leaf_tl ln_tbs_bytes /\ tree_list_is_parent_hash_linkedP leaf_tl /\ tree_list_ends_at_root leaf_tl /\ @@ -418,9 +418,9 @@ let rec all_credentials_ok_subtree #bytes #cb #tkt #asp #lp #ld #ip #id d p ast_ /// This theorem is mostly a wrapper around `parent_hash_implies_event`. val state_implies_event: {|crypto_invariants|} -> - #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes -> #l:nat -> #i:tree_index l -> + #tkt:treekem_types bytes -> #group_id:mls_bytes bytes -> #l:nat -> #i:tree_index l -> tr:trace -> - st:treesync_state dy_bytes tkt dy_as_token group_id -> t:treesync dy_bytes tkt l i -> ast:as_tokens dy_bytes (dy_asp tr).token_t l i -> + st:treesync_state bytes tkt dy_as_token group_id -> t:treesync bytes tkt l i -> ast:as_tokens bytes (dy_asp tr).token_t l i -> Lemma (requires has_leaf_node_tbs_invariant tkt /\ @@ -594,10 +594,10 @@ let rec apply_path_aux_compute_leaf_parent_hash_from_path_both_succeed #bytes #c | _ -> () val external_path_has_event: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> #l:nat -> #li:leaf_index l 0 -> prin:principal -> tr:trace -> - t:treesync dy_bytes tkt l 0 -> p:external_pathsync dy_bytes tkt l 0 li -> group_id:mls_bytes dy_bytes -> + t:treesync bytes tkt l 0 -> p:external_pathsync bytes tkt l 0 li -> group_id:mls_bytes bytes -> prop let external_path_has_event #tkt #l #li prin tr t p group_id = (get_path_leaf p).source == LNS_update /\ @@ -607,8 +607,8 @@ let external_path_has_event #tkt #l #li prin tr t p group_id = path_is_parent_hash_valid_external_path_to_path_nosig t p group_id; let Success auth_p = external_path_to_path_nosig t p group_id in let auth_ln = get_path_leaf auth_p in - compute_leaf_parent_hash_from_path_set_path_leaf t p auth_ln (root_parent_hash #dy_bytes); - apply_path_aux_compute_leaf_parent_hash_from_path_both_succeed t auth_p (root_parent_hash #dy_bytes); + compute_leaf_parent_hash_from_path_set_path_leaf t p auth_ln (root_parent_hash #bytes); + apply_path_aux_compute_leaf_parent_hash_from_path_both_succeed t auth_p (root_parent_hash #bytes); leaf_node_has_event prin tr ({data = auth_ln.data; group_id; leaf_index = li;}) /\ tree_list_has_event prin tr group_id (path_to_tree_list t auth_p) ) @@ -623,11 +623,11 @@ let external_path_has_event #tkt #l #li prin tr t p group_id = #push-options "--z3rlimit 100" val is_msg_external_path_to_path: {|crypto_invariants|} -> - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> #l:nat -> #li:leaf_index l 0 -> prin:principal -> label:label -> tr:trace -> - t:treesync dy_bytes tkt l 0 -> p:external_pathsync dy_bytes tkt l 0 li -> group_id:mls_bytes dy_bytes -> - sk:dy_bytes -> nonce:sign_nonce dy_bytes -> + t:treesync bytes tkt l 0 -> p:external_pathsync bytes tkt l 0 li -> group_id:mls_bytes bytes -> + sk:bytes -> nonce:sign_nonce bytes -> Lemma (requires (get_path_leaf p).source == LNS_update /\ @@ -645,25 +645,25 @@ val is_msg_external_path_to_path: ) (ensures is_well_formed _ (is_knowable_by label tr) (Success?.v (external_path_to_path t p group_id sk nonce))) let is_msg_external_path_to_path #ci #tkt #l #li prin label tr t p group_id sk nonce = - let Success computed_parent_hash = compute_leaf_parent_hash_from_path t p (root_parent_hash #dy_bytes) in + let Success computed_parent_hash = compute_leaf_parent_hash_from_path t p (root_parent_hash #bytes) in let ln_data = get_path_leaf p in let new_ln_data = { ln_data with source = LNS_commit; parent_hash = computed_parent_hash; } in - let new_ln_tbs: leaf_node_tbs_nt dy_bytes tkt = ({data = new_ln_data; group_id; leaf_index = li;}) in - let new_ln_tbs_bytes: dy_bytes = serialize (leaf_node_tbs_nt dy_bytes tkt) new_ln_tbs in + let new_ln_tbs: leaf_node_tbs_nt bytes tkt = ({data = new_ln_data; group_id; leaf_index = li;}) in + let new_ln_tbs_bytes: bytes = serialize (leaf_node_tbs_nt bytes tkt) new_ln_tbs in let Success new_signature = sign_with_label sk "LeafNodeTBS" new_ln_tbs_bytes nonce in - let new_ln = ({ data = new_ln_data; signature = new_signature; } <: leaf_node_nt dy_bytes tkt) in - let new_unsigned_ln = ({ data = new_ln_data; signature = empty #dy_bytes; } <: leaf_node_nt dy_bytes tkt) in + let new_ln = ({ data = new_ln_data; signature = new_signature; } <: leaf_node_nt bytes tkt) in + let new_unsigned_ln = ({ data = new_ln_data; signature = empty #bytes; } <: leaf_node_nt bytes tkt) in let unsigned_path = set_path_leaf p new_unsigned_ln in - compute_leaf_parent_hash_from_path_set_path_leaf t p new_unsigned_ln (root_parent_hash #dy_bytes); - apply_path_aux_compute_leaf_parent_hash_from_path_both_succeed t unsigned_path (root_parent_hash #dy_bytes); + compute_leaf_parent_hash_from_path_set_path_leaf t p new_unsigned_ln (root_parent_hash #bytes); + apply_path_aux_compute_leaf_parent_hash_from_path_both_succeed t unsigned_path (root_parent_hash #bytes); path_is_parent_hash_valid_external_path_to_path_nosig t p group_id; path_is_filter_valid_external_path_to_path_nosig t p group_id; get_path_leaf_set_path_leaf p new_unsigned_ln; - pre_compute_leaf_parent_hash_from_path (is_knowable_by label tr) t p (root_parent_hash #dy_bytes); + pre_compute_leaf_parent_hash_from_path (is_knowable_by label tr) t p (root_parent_hash #bytes); is_well_formed_get_path_leaf (is_knowable_by label tr) p; - serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (is_knowable_by label tr) ({data = new_ln_data; group_id; leaf_index = li;}); + serialize_wf_lemma (leaf_node_tbs_nt bytes tkt) (is_knowable_by label tr) ({data = new_ln_data; group_id; leaf_index = li;}); path_to_tree_list_lemma t unsigned_path; - parse_serialize_inv_lemma #dy_bytes (leaf_node_tbs_nt dy_bytes tkt) new_ln_tbs; + parse_serialize_inv_lemma #bytes (leaf_node_tbs_nt bytes tkt) new_ln_tbs; bytes_invariant_sign_with_label (leaf_node_sign_pred tkt) tr prin sk "LeafNodeTBS" new_ln_tbs_bytes nonce; is_well_formed_set_path_leaf (is_knowable_by label tr) p new_ln #pop-options @@ -673,10 +673,10 @@ let is_msg_external_path_to_path #ci #tkt #l #li prin label tr t p group_id sk n #push-options "--z3rlimit 25" val is_msg_sign_leaf_node_data_key_package: {|crypto_invariants|} -> - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> prin:principal -> label:label -> tr:trace -> - ln_data:leaf_node_data_nt dy_bytes tkt -> - sk:dy_bytes -> nonce:sign_nonce dy_bytes -> + ln_data:leaf_node_data_nt bytes tkt -> + sk:bytes -> nonce:sign_nonce bytes -> Lemma (requires ln_data.source == LNS_key_package /\ @@ -690,26 +690,26 @@ val is_msg_sign_leaf_node_data_key_package: ) (ensures is_well_formed _ (is_knowable_by label tr) (Success?.v (sign_leaf_node_data_key_package ln_data sk nonce))) let is_msg_sign_leaf_node_data_key_package #ci #tkt prin label tr ln_data sk nonce = - let ln_tbs: leaf_node_tbs_nt dy_bytes tkt = ({data = ln_data; group_id = (); leaf_index = ();}) in - let ln_tbs_bytes: dy_bytes = serialize _ ln_tbs in - parse_serialize_inv_lemma #dy_bytes (leaf_node_tbs_nt dy_bytes tkt) ln_tbs; - serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (is_knowable_by label tr) ln_tbs; + let ln_tbs: leaf_node_tbs_nt bytes tkt = ({data = ln_data; group_id = (); leaf_index = ();}) in + let ln_tbs_bytes: bytes = serialize _ ln_tbs in + parse_serialize_inv_lemma #bytes (leaf_node_tbs_nt bytes tkt) ln_tbs; + serialize_wf_lemma (leaf_node_tbs_nt bytes tkt) (is_knowable_by label tr) ln_tbs; bytes_invariant_sign_with_label (leaf_node_sign_pred tkt) tr prin sk "LeafNodeTBS" ln_tbs_bytes nonce #pop-options #push-options "--z3rlimit 25" val is_msg_sign_leaf_node_data_update: {|crypto_invariants|} -> - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> prin:principal -> label:label -> tr:trace -> - ln_data:leaf_node_data_nt dy_bytes tkt -> group_id:mls_bytes dy_bytes -> leaf_index:nat_lbytes 4 -> - sk:dy_bytes -> nonce:sign_nonce dy_bytes -> + ln_data:leaf_node_data_nt bytes tkt -> group_id:mls_bytes bytes -> leaf_index:nat_lbytes 4 -> + sk:bytes -> nonce:sign_nonce bytes -> Lemma (requires ln_data.source == LNS_update /\ Success? (sign_leaf_node_data_update ln_data group_id leaf_index sk nonce) /\ leaf_node_has_event prin tr ({data = ln_data; group_id; leaf_index;}) /\ - 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))|) /\ + tree_has_event prin tr group_id (|0, (leaf_index <: nat), TLeaf (Some ({data = ln_data; signature = empty #bytes;} <: leaf_node_nt 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 /\ is_signature_key_sk tr prin sk /\ @@ -719,9 +719,9 @@ val is_msg_sign_leaf_node_data_update: ) (ensures is_well_formed _ (is_knowable_by label tr) (Success?.v (sign_leaf_node_data_update ln_data group_id leaf_index sk nonce))) let is_msg_sign_leaf_node_data_update #ci #tkt prin label tr ln_data group_id leaf_index sk nonce = - let ln_tbs: leaf_node_tbs_nt dy_bytes tkt = ({data = ln_data; group_id; leaf_index;}) in - let ln_tbs_bytes: dy_bytes = serialize _ ln_tbs in - parse_serialize_inv_lemma #dy_bytes (leaf_node_tbs_nt dy_bytes tkt) ln_tbs; - serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (is_knowable_by label tr) ln_tbs; + let ln_tbs: leaf_node_tbs_nt bytes tkt = ({data = ln_data; group_id; leaf_index;}) in + let ln_tbs_bytes: bytes = serialize _ ln_tbs in + parse_serialize_inv_lemma #bytes (leaf_node_tbs_nt bytes tkt) ln_tbs; + serialize_wf_lemma (leaf_node_tbs_nt bytes tkt) (is_knowable_by label tr) ln_tbs; bytes_invariant_sign_with_label (leaf_node_sign_pred tkt) tr prin sk "LeafNodeTBS" ln_tbs_bytes nonce #pop-options diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.AuthServiceCache.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.AuthServiceCache.fst index 7f7e861..b4fd0e8 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.AuthServiceCache.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.AuthServiceCache.fst @@ -12,7 +12,7 @@ open MLS.Symbolic (*** AS cache types & invariants ***) -[@@ with_bytes dy_bytes] +[@@ with_bytes bytes] type as_cache_key = { verification_key: signature_public_key_nt bytes; credential: credential_nt bytes; @@ -21,7 +21,7 @@ type as_cache_key = { %splice [ps_as_cache_key] (gen_parser (`as_cache_key)) %splice [ps_as_cache_key_is_well_formed] (gen_is_well_formed_lemma (`as_cache_key)) -[@@ with_bytes dy_bytes] +[@@ with_bytes bytes] type as_cache_value = { token: dy_as_token; } diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.GroupManager.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.GroupManager.fst index 83fdaae..f65e864 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.GroupManager.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.GroupManager.fst @@ -10,15 +10,15 @@ open MLS.Symbolic (*** Group manager types & invariants ***) -[@@ with_bytes dy_bytes] +[@@ with_bytes bytes] type group_manager_key = { - group_id: mls_bytes dy_bytes; + group_id: mls_bytes bytes; } %splice [ps_group_manager_key] (gen_parser (`group_manager_key)) %splice [ps_group_manager_key_is_well_formed] (gen_is_well_formed_lemma (`group_manager_key)) -[@@ with_bytes dy_bytes] +[@@ with_bytes bytes] type group_manager_value = { si_public: state_id; si_private: state_id; diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.KeyPackageManager.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.KeyPackageManager.fst index cd486de..f78acb1 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.KeyPackageManager.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.KeyPackageManager.fst @@ -10,7 +10,7 @@ open MLS.TreeSync.Symbolic.IsWellFormed (*** KeyPackage manager types & invariants ***) -[@@ with_bytes dy_bytes] +[@@ with_bytes bytes] type key_package_manager_value = { si_private: state_id; } @@ -18,13 +18,13 @@ type key_package_manager_value = { %splice [ps_key_package_manager_value] (gen_parser (`key_package_manager_value)) %splice [ps_key_package_manager_value_is_well_formed] (gen_is_well_formed_lemma (`key_package_manager_value)) -instance key_package_manager_types (tkt:treekem_types dy_bytes): map_types (key_package_nt dy_bytes tkt) key_package_manager_value = { +instance key_package_manager_types (tkt:treekem_types bytes): map_types (key_package_nt bytes tkt) key_package_manager_value = { tag = "MLS.TreeSync.KeyPackageManager"; ps_key_t = ps_key_package_nt tkt; ps_value_t = ps_key_package_manager_value; } -val key_package_manager_pred: {|crypto_invariants|} -> tkt:treekem_types dy_bytes -> map_predicate (key_package_nt dy_bytes tkt) key_package_manager_value #_ +val key_package_manager_pred: {|crypto_invariants|} -> tkt:treekem_types bytes -> map_predicate (key_package_nt bytes tkt) key_package_manager_value #_ let key_package_manager_pred #ci tkt = { pred = (fun tr prin state_id key_package value -> is_well_formed _ (is_publishable tr) key_package @@ -35,15 +35,15 @@ let key_package_manager_pred #ci tkt = { ); } -val has_key_package_manager_invariant: treekem_types dy_bytes -> {|protocol_invariants|} -> prop +val has_key_package_manager_invariant: treekem_types bytes -> {|protocol_invariants|} -> prop let has_key_package_manager_invariant tkt #invs = has_map_session_invariant (key_package_manager_pred tkt) -val key_package_manager_tag_and_invariant: {|crypto_invariants|} -> treekem_types dy_bytes -> dtuple2 string local_bytes_state_predicate +val key_package_manager_tag_and_invariant: {|crypto_invariants|} -> treekem_types bytes -> dtuple2 string local_bytes_state_predicate let key_package_manager_tag_and_invariant #ci tkt = (|(key_package_manager_types tkt).tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant (key_package_manager_pred tkt))|) (*** KeyPackage manager API ***) -let initialize_key_package_manager (tkt:treekem_types dy_bytes) = initialize_map (key_package_nt dy_bytes tkt) key_package_manager_value -let add_new_key_package_secret_session (tkt:treekem_types dy_bytes) = add_key_value #(key_package_nt dy_bytes tkt) #key_package_manager_value -let find_key_package_secret_session (tkt:treekem_types dy_bytes) = find_value #(key_package_nt dy_bytes tkt) #key_package_manager_value +let initialize_key_package_manager (tkt:treekem_types bytes) = initialize_map (key_package_nt bytes tkt) key_package_manager_value +let add_new_key_package_secret_session (tkt:treekem_types bytes) = add_key_value #(key_package_nt bytes tkt) #key_package_manager_value +let find_key_package_secret_session (tkt:treekem_types bytes) = find_value #(key_package_nt bytes tkt) #key_package_manager_value diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.Tree.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.Tree.fst index 866269a..08327b9 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.Tree.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.Tree.fst @@ -22,14 +22,14 @@ open MLS.TreeSync.Symbolic.LeafNodeSignature (*** Session predicate for public state ***) -val ps_dy_as_tokens: l:nat -> i:tree_index l -> parser_serializer dy_bytes (as_tokens dy_bytes dy_as_token l i) +val ps_dy_as_tokens: l:nat -> i:tree_index l -> parser_serializer bytes (as_tokens bytes dy_as_token l i) let ps_dy_as_tokens l i = ps_as_tokens ps_dy_as_token l i #push-options "--z3rlimit 25" val ps_dy_as_tokens_is_well_formed: #l:nat -> #i:tree_index l -> - pre:bytes_compatible_pre dy_bytes -> tokens:as_tokens dy_bytes dy_as_token l i -> + pre:bytes_compatible_pre bytes -> tokens:as_tokens bytes dy_as_token l i -> Lemma (is_well_formed_prefix (ps_dy_as_tokens l i) pre tokens) let rec ps_dy_as_tokens_is_well_formed #l #i pre tokens = @@ -60,16 +60,16 @@ type bare_treesync_state_ (bytes:Type0) {|bytes_like bytes|} (tkt:treekem_types %splice [ps_bare_treesync_state__is_well_formed] (gen_is_well_formed_lemma (`bare_treesync_state_)) #pop-options -type bare_treesync_state (tkt:treekem_types dy_bytes) = - bare_treesync_state_ dy_bytes tkt dy_as_token ps_dy_as_token +type bare_treesync_state (tkt:treekem_types bytes) = + bare_treesync_state_ bytes tkt dy_as_token ps_dy_as_token -instance parseable_serializeable_bare_treesync_state (tkt:treekem_types dy_bytes): parseable_serializeable dy_bytes (bare_treesync_state tkt) = mk_parseable_serializeable (ps_bare_treesync_state_ tkt dy_as_token ps_dy_as_token) +instance parseable_serializeable_bare_treesync_state (tkt:treekem_types bytes): parseable_serializeable bytes (bare_treesync_state tkt) = mk_parseable_serializeable (ps_bare_treesync_state_ tkt dy_as_token ps_dy_as_token) -instance local_state_bare_treesync_state (tkt:treekem_types dy_bytes): local_state (bare_treesync_state tkt) = +instance local_state_bare_treesync_state (tkt:treekem_types bytes): local_state (bare_treesync_state tkt) = mk_local_state_instance "MLS.TreeSync.PublicState" #push-options "--fuel 1 --ifuel 1 --z3rlimit 25" -val treesync_public_state_pred: {|crypto_invariants|} -> tkt:treekem_types dy_bytes -> local_state_predicate (bare_treesync_state tkt) +val treesync_public_state_pred: {|crypto_invariants|} -> tkt:treekem_types bytes -> local_state_predicate (bare_treesync_state tkt) let treesync_public_state_pred #ci tkt = { pred = (fun tr prin state_id st -> is_publishable tr st.group_id /\ @@ -77,7 +77,7 @@ let treesync_public_state_pred #ci tkt = { unmerged_leaves_ok st.tree /\ parent_hash_invariant st.tree /\ valid_leaves_invariant st.group_id st.tree /\ - all_credentials_ok st.tree ((st.tokens <: as_tokens dy_bytes dy_as_token st.levels 0) <: as_tokens dy_bytes (dy_asp tr).token_t st.levels 0) + all_credentials_ok st.tree ((st.tokens <: as_tokens bytes dy_as_token st.levels 0) <: as_tokens bytes (dy_asp tr).token_t st.levels 0) ); pred_later = (fun tr1 tr2 prin state_id st -> wf_weaken_lemma _ (is_publishable tr1) (is_publishable tr2) st.tree @@ -90,18 +90,18 @@ let treesync_public_state_pred #ci tkt = { } #pop-options -val has_treesync_public_state_invariant: treekem_types dy_bytes -> {|protocol_invariants|} -> prop +val has_treesync_public_state_invariant: treekem_types bytes -> {|protocol_invariants|} -> prop let has_treesync_public_state_invariant tkt #invs = has_local_state_predicate (treesync_public_state_pred tkt) -val treesync_public_state_tag_and_invariant: {|crypto_invariants|} -> treekem_types dy_bytes -> dtuple2 string local_bytes_state_predicate +val treesync_public_state_tag_and_invariant: {|crypto_invariants|} -> treekem_types bytes -> dtuple2 string local_bytes_state_predicate let treesync_public_state_tag_and_invariant #ci tkt = (|(local_state_bare_treesync_state tkt).tag, local_state_predicate_to_local_bytes_state_predicate (treesync_public_state_pred tkt)|) (*** Traceful API for public state ***) val treesync_state_to_bare_treesync_state: - #tkt:treekem_types dy_bytes -> - #group_id:mls_bytes dy_bytes -> st:treesync_state dy_bytes tkt dy_as_token group_id -> + #tkt:treekem_types bytes -> + #group_id:mls_bytes bytes -> st:treesync_state bytes tkt dy_as_token group_id -> bare_treesync_state tkt let treesync_state_to_bare_treesync_state #tkt #group_id st = { group_id = group_id; @@ -111,9 +111,9 @@ let treesync_state_to_bare_treesync_state #tkt #group_id st = { } val new_public_treesync_state: - #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes -> + #tkt:treekem_types bytes -> #group_id:mls_bytes bytes -> principal -> - st:treesync_state dy_bytes tkt dy_as_token group_id -> + st:treesync_state bytes tkt dy_as_token group_id -> traceful state_id let new_public_treesync_state #tkt #group_id prin st = let* state_id = new_session_id prin in @@ -122,9 +122,9 @@ let new_public_treesync_state #tkt #group_id prin st = val new_public_treesync_state_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes -> + #tkt:treekem_types bytes -> #group_id:mls_bytes bytes -> prin:principal -> - st:treesync_state dy_bytes tkt dy_as_token group_id -> + st:treesync_state bytes tkt dy_as_token group_id -> tr:trace -> Lemma (requires @@ -141,18 +141,18 @@ val new_public_treesync_state_proof: let new_public_treesync_state_proof #invs #tkt #group_id prin st tr = () val set_public_treesync_state: - #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes -> + #tkt:treekem_types bytes -> #group_id:mls_bytes bytes -> prin:principal -> state_id:state_id -> - st:treesync_state dy_bytes tkt dy_as_token group_id -> + st:treesync_state bytes tkt dy_as_token group_id -> traceful unit let set_public_treesync_state #tkt #group_id prin state_id st = set_state prin state_id (treesync_state_to_bare_treesync_state st) val set_public_treesync_state_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes -> + #tkt:treekem_types bytes -> #group_id:mls_bytes bytes -> prin:principal -> state_id:state_id -> - st:treesync_state dy_bytes tkt dy_as_token group_id -> + st:treesync_state bytes tkt dy_as_token group_id -> tr:trace -> Lemma (requires @@ -169,9 +169,9 @@ val set_public_treesync_state_proof: let set_public_treesync_state_proof #invs #tkt #group_id prin state_id st tr = () val get_public_treesync_state: - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> prin:principal -> state_id:state_id -> - traceful (option (dtuple2 (mls_bytes dy_bytes) (treesync_state dy_bytes tkt dy_as_token))) + traceful (option (dtuple2 (mls_bytes bytes) (treesync_state bytes tkt dy_as_token))) let get_public_treesync_state #tkt prin state_id = let*? bare_st: bare_treesync_state tkt = get_state prin state_id in // TODO: Dynamic could be removed with REPROSEC/dolev-yao-star-extrinsic#24 @@ -182,11 +182,11 @@ let get_public_treesync_state #tkt prin state_id = levels = bare_st.levels; tree = bare_st.tree; tokens = bare_st.tokens; - } <: treesync_state dy_bytes tkt dy_as_token bare_st.group_id)|)) + } <: treesync_state bytes tkt dy_as_token bare_st.group_id)|)) val get_public_treesync_state_proof: {|protocol_invariants|} -> - #tkt:treekem_types dy_bytes -> + #tkt:treekem_types bytes -> prin:principal -> state_id:state_id -> tr:trace -> Lemma @@ -201,7 +201,7 @@ val get_public_treesync_state_proof: | None -> True | Some (|group_id, st|) -> ( is_publishable tr_out group_id /\ - is_well_formed _ (is_publishable tr_out) (st.tree <: treesync dy_bytes tkt _ _) + is_well_formed _ (is_publishable tr_out) (st.tree <: treesync bytes tkt _ _) ) ) ))