From 283cd0460fe7b40a0500c8f4a066e9236a5b185a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Fri, 17 May 2024 18:17:54 +0200 Subject: [PATCH] refactor: move to DY*-extrinsic --- Makefile | 8 +- flake.lock | 30 +- flake.nix | 25 +- fstar/api/MLS.fst | 8 +- fstar/symbolic/MLS.Symbolic.MapSession.fst | 234 ----- fstar/symbolic/MLS.Symbolic.Session.fst | 246 ----- .../symbolic/MLS.Symbolic.SplitPredicate.fst | 155 --- fstar/symbolic/MLS.Symbolic.TypedSession.fst | 67 -- fstar/symbolic/MLS.Symbolic.fst | 444 +++----- .../treesync/code/MLS.TreeSync.API.Types.fst | 15 +- fstar/treesync/code/MLS.TreeSync.API.fst | 377 ++++--- .../MLS.TreeSync.Invariants.AuthService.fst | 24 +- ...MLS.TreeSync.Symbolic.API.GroupManager.fst | 66 +- ...ync.Symbolic.API.IsWellFormedInvariant.fst | 52 +- ...reeSync.Symbolic.API.KeyPackageManager.fst | 47 +- .../MLS.TreeSync.Symbolic.API.Sessions.fst | 342 +++--- .../symbolic/MLS.TreeSync.Symbolic.API.fst | 986 ++++++++++++------ ...MLS.TreeSync.Symbolic.AuthServiceCache.fst | 60 +- .../MLS.TreeSync.Symbolic.GlobalUsage.fst | 193 ++-- .../MLS.TreeSync.Symbolic.IsWellFormed.fst | 29 +- ...LS.TreeSync.Symbolic.LeafNodeSignature.fst | 319 +++--- 21 files changed, 1686 insertions(+), 2041 deletions(-) delete mode 100644 fstar/symbolic/MLS.Symbolic.MapSession.fst delete mode 100644 fstar/symbolic/MLS.Symbolic.Session.fst delete mode 100644 fstar/symbolic/MLS.Symbolic.SplitPredicate.fst delete mode 100644 fstar/symbolic/MLS.Symbolic.TypedSession.fst diff --git a/Makefile b/Makefile index fc5e657..d56281a 100644 --- a/Makefile +++ b/Makefile @@ -11,7 +11,8 @@ 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)) -INCLUDE_DIRS = $(SOURCE_DIRS) $(HACL_SNAPSHOT_DIR)/lib $(HACL_SNAPSHOT_DIR)/specs $(COMPARSE_HOME)/src $(if $(USE_DY), $(DY_HOME) $(DY_HOME)/symbolic) +DY_INCLUDE_DIRS = core lib lib/comparse 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)) ADMIT ?= @@ -20,8 +21,7 @@ MAYBE_ADMIT = $(if $(ADMIT),--admit_smt_queries true) FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe FSTAR = $(FSTAR_EXE) $(MAYBE_ADMIT) -DY_EXTRACT = +CryptoLib +SecrecyLabels +ComparseGlue +LabeledCryptoAPI +CryptoEffect +GlobalRuntimeLib +LabeledRuntimeAPI +Ord +AttackerAPI -FSTAR_EXTRACT = --extract '-* +MLS +Comparse -Comparse.Tactic $(if $(USE_DY), $(DY_EXTRACT))' +FSTAR_EXTRACT = --extract '-* +MLS +Comparse -Comparse.Tactic $(if $(USE_DY), +DY)' # Allowed warnings: # - (Warning 242) Definitions of inner let-rec ... and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types @@ -71,7 +71,7 @@ obj: cache/MLS.Test.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+272' # Allow more warning in dependencies cache/Lib.IntTypes.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+288+349' -cache/SecrecyLabels.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+337' +cache/DY.Core.Bytes.Type.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+290' %.checked: | hints obj $(FSTAR) $(FSTAR_FLAGS) $(FSTAR_RULE_FLAGS) $< && touch -c $@ diff --git a/flake.lock b/flake.lock index b4f524a..9cf917b 100644 --- a/flake.lock +++ b/flake.lock @@ -23,19 +23,29 @@ "type": "github" } }, - "dolev-yao-star-src": { - "flake": false, + "dolev-yao-star-flake": { + "inputs": { + "comparse-flake": [ + "comparse-flake" + ], + "fstar-flake": [ + "fstar-flake" + ], + "nixpkgs": [ + "nixpkgs" + ] + }, "locked": { - "lastModified": 1682502249, - "narHash": "sha256-Xf/tgpS4Xbweotc/XOr1M2tfjdkVMAU+A4Ce9CP7vCM=", - "owner": "Inria-Prosecco", - "repo": "treesync", - "rev": "7ea27ead0abc4e6bf47033f35a7eada233ac244e", + "lastModified": 1715956913, + "narHash": "sha256-qN9szzS81pPHOsx/dnjNqOtkKIEA9/iUTDcSf05gQ5E=", + "owner": "REPROSEC", + "repo": "dolev-yao-star-extrinsic", + "rev": "3b62a6ade537dc3f060064cb538ec75d4a2df020", "type": "github" }, "original": { - "owner": "Inria-Prosecco", - "repo": "treesync", + "owner": "REPROSEC", + "repo": "dolev-yao-star-extrinsic", "type": "github" } }, @@ -109,7 +119,7 @@ "root": { "inputs": { "comparse-flake": "comparse-flake", - "dolev-yao-star-src": "dolev-yao-star-src", + "dolev-yao-star-flake": "dolev-yao-star-flake", "fstar-flake": "fstar-flake", "hacl-packages-src": "hacl-packages-src", "nixpkgs": [ diff --git a/flake.nix b/flake.nix index 067d529..b7db2f3 100644 --- a/flake.nix +++ b/flake.nix @@ -9,9 +9,11 @@ inputs.fstar-flake.follows = "fstar-flake"; }; - dolev-yao-star-src = { - url = "github:Inria-Prosecco/treesync"; - flake = false; + dolev-yao-star-flake = { + url = "github:REPROSEC/dolev-yao-star-extrinsic"; + inputs.nixpkgs.follows = "nixpkgs"; + inputs.fstar-flake.follows = "fstar-flake"; + inputs.comparse-flake.follows = "comparse-flake"; }; hacl-packages-src = { @@ -20,7 +22,7 @@ }; }; - outputs = {self, nixpkgs, fstar-flake, comparse-flake, dolev-yao-star-src, hacl-packages-src}: + outputs = {self, nixpkgs, fstar-flake, comparse-flake, dolev-yao-star-flake, hacl-packages-src}: let system = "x86_64-linux"; pkgs = import nixpkgs { inherit system; }; @@ -28,20 +30,7 @@ fstar = fstar-flake.packages.${system}.fstar; fstar-dune = fstar-flake.packages.${system}.fstar-dune; comparse = comparse-flake.packages.${system}.comparse; - # The following is a hack, because nix is not able to fetch a subdirectory of a git repository - # (there is the "?dir=..." syntax, but it works only to point to the flake.nix!) - # There are two repositories where we may obtain dolev-yao-star - # - from the private dolev-yao-star repository - # - from the artifact of the TreeSync paper, that contains a recent public version of DY* in the dolev-yao-star subdirectory - # Hence, this little condition will check whether there exists a "dolev-yao-star" subdirectory - # (which only happens when dolev-yao-star-src points to the TreeSync artifact), - # and go into it when that is the case. - dolev-yao-star = - if (builtins.readDir dolev-yao-star-src)?"dolev-yao-star" then - "${dolev-yao-star-src}/dolev-yao-star" - else - dolev-yao-star-src - ; + dolev-yao-star = dolev-yao-star-flake.packages.${system}.dolev-yao-star; mls-star = pkgs.callPackage ./default.nix {inherit fstar fstar-dune z3 comparse dolev-yao-star hacl-packages-src; ocamlPackages = pkgs.ocaml-ng.ocamlPackages_4_14;}; in { packages.${system} = { diff --git a/fstar/api/MLS.fst b/fstar/api/MLS.fst index 1b9b60c..42c9a0e 100644 --- a/fstar/api/MLS.fst +++ b/fstar/api/MLS.fst @@ -37,16 +37,10 @@ let universal_sign_nonce = let group_id = bytes -let asp: as_parameters bytes = { - token_t = unit; - credential_ok = (fun _ _ -> True); - valid_successor = (fun _ _ -> True); -} - noeq type state = { group_id:mls_bytes bytes; leaf_index: nat; - treesync_state: MLS.TreeSync.API.Types.treesync_state bytes tkt asp group_id; + treesync_state: MLS.TreeSync.API.Types.treesync_state bytes tkt unit group_id; treekem_state: treekem_state bytes leaf_index; treedem_state: treedem_state bytes; epoch: nat; diff --git a/fstar/symbolic/MLS.Symbolic.MapSession.fst b/fstar/symbolic/MLS.Symbolic.MapSession.fst deleted file mode 100644 index 503454a..0000000 --- a/fstar/symbolic/MLS.Symbolic.MapSession.fst +++ /dev/null @@ -1,234 +0,0 @@ -module MLS.Symbolic.MapSession - -open Comparse -open ComparseGlue -open GlobalRuntimeLib -open LabeledRuntimeAPI -open MLS.Symbolic -open MLS.Symbolic.Session -open MLS.Symbolic.TypedSession - -#set-options "--fuel 0 --ifuel 0" - -(*** Map state & invariants ***) - -noeq type map_types (bytes:Type0) {|bytes_like bytes|} = { - key: eqtype; - ps_key: parser_serializer bytes key; - value: Type0; - ps_value: parser_serializer bytes value; -} - -noeq type map_predicate (mt:map_types dy_bytes) = { - pred: global_usage -> timestamp -> mt.key -> mt.value -> prop; - pred_later: gu:global_usage -> time0:timestamp -> time1:timestamp -> key:mt.key -> value:mt.value -> Lemma - (requires pred gu time0 key value /\ time0 <$ time1) - (ensures pred gu time1 key value) - ; - pred_is_msg: gu:global_usage -> time:timestamp -> key:mt.key -> value:mt.value -> Lemma - (requires pred gu time key value) - (ensures is_well_formed_prefix mt.ps_key (is_publishable gu time) key /\ is_well_formed_prefix mt.ps_value (is_publishable gu time) value) - ; -} - -noeq type map_elem_ (bytes:Type0) {|bytes_like bytes|} (mt:map_types bytes) = { - [@@@ with_parser #bytes mt.ps_key] - key: mt.key; - [@@@ with_parser #bytes mt.ps_value] - value: mt.value; -} - -%splice [ps_map_elem_] (gen_parser (`map_elem_)) -%splice [ps_map_elem__is_well_formed] (gen_is_well_formed_lemma (`map_elem_)) - -type map_elem = map_elem_ dy_bytes - -noeq type map_ (bytes:Type0) {|bytes_like bytes|} (mt:map_types bytes) = { - [@@@ with_parser #bytes (ps_list (ps_map_elem_ mt))] - key_values: list (map_elem_ bytes mt) -} - -%splice [ps_map_] (gen_parser (`map_)) -%splice [ps_map__is_well_formed] (gen_is_well_formed_lemma (`map_)) - -type map = map_ dy_bytes - -instance parseable_serializeable_map_ (bytes:Type0) {|bytes_like bytes|} (mt:map_types bytes) : parseable_serializeable bytes (map_ bytes mt) = mk_parseable_serializeable (ps_map_ mt) - -val map_elem_invariant: mt:map_types dy_bytes -> map_predicate mt -> global_usage -> timestamp -> map_elem mt -> prop -let map_elem_invariant mt mpred gu time x = - mpred.pred gu time x.key x.value - -val map_invariant: mt:map_types dy_bytes -> map_predicate mt -> global_usage -> timestamp -> map mt -> prop -let map_invariant mt mpred gu time st = - for_allP (map_elem_invariant mt mpred gu time) st.key_values - -val map_invariant_eq: mt:map_types dy_bytes -> mpred:map_predicate mt -> gu:global_usage -> time:timestamp -> st:map mt -> Lemma - (map_invariant mt mpred gu time st <==> (forall x. List.Tot.memP x st.key_values ==> map_elem_invariant mt mpred gu time x)) -let map_invariant_eq mt mpred gu time st = - for_allP_eq (map_elem_invariant mt mpred gu time) st.key_values - -val bare_map_session_invariant: mt:map_types dy_bytes -> mpred:map_predicate mt -> bare_typed_session_pred (map mt) -let bare_map_session_invariant mt mpred gu p time si vi st = - map_invariant mt mpred gu time st - -val map_session_invariant: mt:map_types dy_bytes -> mpred:map_predicate mt -> session_pred -let map_session_invariant mt mpred = - typed_session_pred_to_session_pred ( - mk_typed_session_pred (bare_map_session_invariant mt mpred) - (fun gu p time0 time1 si vi st -> - map_invariant_eq mt mpred gu time0 st; - map_invariant_eq mt mpred gu time1 st; - introduce forall x. map_elem_invariant mt mpred gu time0 x ==> map_elem_invariant mt mpred gu time1 x - with ( - introduce _ ==> _ with _. ( - mpred.pred_later gu time0 time1 x.key x.value - ) - ) - ) - (fun gu p time si vi st -> - let pre = is_msg gu (readers [psv_id p si vi]) time in - map_invariant_eq mt mpred gu time st; - for_allP_eq (is_well_formed_prefix (ps_map_elem_ mt) pre) st.key_values; - introduce forall x. map_elem_invariant mt mpred gu time x ==> is_well_formed_prefix (ps_map_elem_ mt) pre x - with ( - introduce _ ==> _ with _. ( - mpred.pred_is_msg gu time x.key x.value; - is_well_formed_prefix_weaken mt.ps_key (is_publishable gu time) pre x.key; - is_well_formed_prefix_weaken mt.ps_value (is_publishable gu time) pre x.value - ) - ) - ) - ) - -val has_map_session_invariant: mt:map_types dy_bytes -> mpred:map_predicate mt -> string -> preds -> prop -let has_map_session_invariant mt mpred label pr = - has_session_pred pr label (map_session_invariant mt mpred) - -(*** Map API ***) - -#push-options "--fuel 1" -val initialize_map: - mt:map_types dy_bytes -> mpred:map_predicate mt -> label:string -> - pr:preds -> p:principal -> LCrypto nat pr - (requires fun t0 -> has_map_session_invariant mt mpred label pr) - (ensures fun t0 r t1 -> trace_len t1 == trace_len t0 + 1) -let initialize_map mt mpred label pr p = - let time = global_timestamp () in - let si = new_session_number pr p in - let session = { key_values = [] } in - let session_bytes: dy_bytes = serialize (map mt) session in - parse_serialize_inv_lemma #dy_bytes (map mt) session; - new_session pr label (map_session_invariant mt mpred) p si 0 session_bytes; - si -#pop-options - -val set_map: - mt:map_types dy_bytes -> mpred:map_predicate mt -> label:string -> - pr:preds -> p:principal -> si:nat -> - st:map mt -> - LCrypto unit pr - (requires fun t0 -> map_invariant mt mpred pr.global_usage (trace_len t0) st /\ has_map_session_invariant mt mpred label pr) - (ensures fun t0 r t1 -> trace_len t1 == trace_len t0 + 1) -let set_map mt mpred label pr p si st = - let st_bytes: dy_bytes = serialize (map mt) st in - parse_serialize_inv_lemma #dy_bytes (map mt) st; - update_session pr label (map_session_invariant mt mpred) p si 0 st_bytes - -val get_map: - mt:map_types dy_bytes -> mpred:map_predicate mt -> label:string -> - pr:preds -> p:principal -> si:nat -> - LCrypto (map mt) pr - (requires fun t0 -> has_map_session_invariant mt mpred label pr) - (ensures fun t0 st t1 -> - map_invariant mt mpred pr.global_usage (trace_len t0) st /\ - t1 == t0 - ) -let get_map mt mpred label pr p si = - let (_, st_bytes) = get_session pr label (map_session_invariant mt mpred) p si in - Some?.v (parse (map mt) st_bytes) - -#push-options "--fuel 1" -val add_key_value: - mt:map_types dy_bytes -> mpred:map_predicate mt -> label:string -> - pr:preds -> p:principal -> si:nat -> - key:mt.key -> value:mt.value -> - LCrypto unit pr - (requires fun t0 -> - mpred.pred pr.global_usage (trace_len t0) key value /\ - has_map_session_invariant mt mpred label pr - ) - (ensures fun t0 () t1 -> trace_len t1 == trace_len t0 + 1) -let add_key_value mt mpred label pr p si key value = - let cached_elem = { - key; - value; - } in - let st = get_map mt mpred label pr p si in - let new_st = { key_values = cached_elem::st.key_values } in - set_map mt mpred label pr p si new_st -#pop-options - -#push-options "--fuel 1 --ifuel 1" -val find_value_aux: #mt:map_types dy_bytes -> key:mt.key -> l:list (map_elem mt) -> Pure (option mt.value) - (requires True) - (ensures fun res -> - match res with - | None -> True - | Some value -> List.Tot.memP ({key; value;}) l - ) -let rec find_value_aux #mt key l = - match l with - | [] -> None - | h::t -> - if h.key = key then - Some h.value - else - match find_value_aux key t with - | Some res -> Some res - | None -> None -#pop-options - -val try_find_value: - mt:map_types dy_bytes -> mpred:map_predicate mt -> label:string -> - pr:preds -> p:principal -> si:nat -> - key:mt.key -> - LCrypto (option mt.value) pr - (requires fun t0 -> - has_map_session_invariant mt mpred label pr - ) - (ensures fun t0 opt_value t1 -> - (match opt_value with - | None -> True - | Some value -> mpred.pred pr.global_usage (trace_len t0) key value - ) /\ - t1 == t0 - ) -let try_find_value mt mpred label pr p si key = - let st = get_map mt mpred label pr p si in - match find_value_aux key st.key_values with - | None -> None - | Some value -> ( - let now = global_timestamp () in - map_invariant_eq mt mpred pr.global_usage now st; - Some value - ) - -val find_value: - mt:map_types dy_bytes -> mpred:map_predicate mt -> label:string -> - pr:preds -> p:principal -> si:nat -> - key:mt.key -> - LCrypto mt.value pr - (requires fun t0 -> - has_map_session_invariant mt mpred label pr - ) - (ensures fun t0 value t1 -> - mpred.pred pr.global_usage (trace_len t0) key value /\ - t1 == t0 - ) -let find_value mt mpred label pr p si key = - match try_find_value mt mpred label pr p si key with - | None -> error "find_value: no such key found!" - | Some value -> ( - value - ) diff --git a/fstar/symbolic/MLS.Symbolic.Session.fst b/fstar/symbolic/MLS.Symbolic.Session.fst deleted file mode 100644 index 846a10f..0000000 --- a/fstar/symbolic/MLS.Symbolic.Session.fst +++ /dev/null @@ -1,246 +0,0 @@ -module MLS.Symbolic.Session - -open Comparse -open ComparseGlue -open MLS.Symbolic -open MLS.Symbolic.SplitPredicate - -open GlobalRuntimeLib -open LabeledRuntimeAPI - -#set-options "--fuel 1 --ifuel 1" - -(*** Session predicates ***) - -type labeled_session (bytes:Type0) {|bytes_like bytes|} = { - label: bytes; - content: bytes; -} - -%splice [ps_labeled_session] (gen_parser (`labeled_session)) -%splice [ps_labeled_session_is_well_formed] (gen_is_well_formed_lemma (`labeled_session)) - -instance parseable_serializeable_labeled_session (bytes:Type0) {|bytes_like bytes|}: parseable_serializeable bytes (labeled_session bytes) = mk_parseable_serializeable (ps_labeled_session) - -let split_session_pred_func: split_predicate_input_values = { - labeled_data_t = principal & timestamp & nat & nat & dy_bytes; - label_t = string; - encoded_label_t = dy_bytes; - raw_data_t = principal & timestamp & nat & nat & dy_bytes; - - decode_labeled_data = (fun (p, time, si, vi, session) -> ( - match parse (labeled_session dy_bytes) session with - | Some ({label; content}) -> Some (label, (p, time, si, vi, content)) - | None -> None - )); - - encode_label = CryptoLib.string_to_bytes; - encode_label_inj = (fun l1 l2 -> - CryptoLib.string_to_bytes_lemma l1; - CryptoLib.string_to_bytes_lemma l2 - ); -} - -type bare_session_pred = gu:global_usage -> p:principal -> time:timestamp -> si:nat -> vi:nat -> session:dy_bytes -> prop - -val bare_session_pred_later: bare_session_pred -> prop -let bare_session_pred_later spred = - forall gu p time0 time1 si vi session. - (spred gu p time0 si vi session /\ time0 <$ time1) - ==> - spred gu p time1 si vi session - -val bare_session_pred_is_msg: bare_session_pred -> prop -let bare_session_pred_is_msg spred = - forall gu p time si vi session. - spred gu p time si vi session - ==> - is_msg gu (readers [psv_id p si vi]) time session - -type session_pred = spred:bare_session_pred{bare_session_pred_later spred /\ bare_session_pred_is_msg spred} - -val mk_session_pred: - spred:bare_session_pred -> - (gu:global_usage -> p:principal -> time0:timestamp -> time1:timestamp -> si:nat -> vi:nat -> session:dy_bytes -> Lemma - (requires spred gu p time0 si vi session /\ time0 <$ time1) - (ensures spred gu p time1 si vi session) - ) -> - (gu:global_usage -> p:principal -> time:timestamp -> si:nat -> vi:nat -> session:dy_bytes -> Lemma - (requires spred gu p time si vi session) - (ensures is_msg gu (readers [psv_id p si vi]) time session) - ) -> - session_pred - -let mk_session_pred spred later_lemma is_msg_lemma = - introduce forall gu p time0 time1 si vi session. (spred gu p time0 si vi session /\ time0 <$ time1) ==> spred gu p time1 si vi session - with ( - introduce _ ==> _ with _. ( - later_lemma gu p time0 time1 si vi session - ) - ); - introduce forall gu p time si vi session. spred gu p time si vi session ==> is_msg gu (readers [psv_id p si vi]) time session - with ( - introduce _ ==> _ with _. ( - is_msg_lemma gu p time si vi session - ) - ); - spred - -val session_pred_to_local_pred: global_usage -> session_pred -> local_pred split_session_pred_func -let session_pred_to_local_pred gu spred (p, time, si, vi, session) = - spred gu p time si vi session - -val preds_to_global_pred: preds -> global_pred split_session_pred_func -let preds_to_global_pred pr (p, time, si, vi, session) = - pr.trace_preds.session_st_inv time p si vi session - -val has_session_pred: preds -> string -> session_pred -> prop -let has_session_pred pr lab spred = - has_local_pred split_session_pred_func (preds_to_global_pred pr) lab (session_pred_to_local_pred pr.global_usage spred) - -(*** Global session predicate builder ***) - -val label_session_pred_to_label_local_pred: global_usage -> string & session_pred -> string & local_pred split_session_pred_func -let label_session_pred_to_label_local_pred gu (label, spred) = - (label, session_pred_to_local_pred gu spred) - -val mk_global_session_pred: list (string & session_pred) -> global_usage -> timestamp -> principal -> nat -> nat -> dy_bytes -> prop -let mk_global_session_pred l gu time p si vi session = - mk_global_pred split_session_pred_func (List.Tot.map (label_session_pred_to_label_local_pred gu) l) (p, time, si, vi, session) - -val mk_global_session_pred_correct: - pr:preds -> lspred:list (string & session_pred) -> - lab:string -> spred:session_pred -> - Lemma - (requires - pr.trace_preds.session_st_inv == mk_global_session_pred lspred pr.global_usage /\ - List.Tot.no_repeats_p (List.Tot.map fst lspred) /\ - List.Tot.memP (lab, spred) lspred - ) - (ensures has_session_pred pr lab spred) -let mk_global_session_pred_correct pr lspred lab spred = - let open MLS.MiscLemmas in - assert_norm (forall session p time si vi. preds_to_global_pred pr (p, time, si, vi, session) <==> pr.trace_preds.session_st_inv time p si vi session); - memP_map (lab, spred) (label_session_pred_to_label_local_pred pr.global_usage) lspred; - FStar.Classical.forall_intro_2 (index_map (label_session_pred_to_label_local_pred pr.global_usage)); - FStar.Classical.forall_intro_2 (index_map (fst #string #session_pred)); - FStar.Classical.forall_intro_2 (index_map (fst #string #(local_pred split_session_pred_func))); - List.Tot.index_extensionality (List.Tot.map fst lspred) (List.Tot.map fst (List.Tot.map (label_session_pred_to_label_local_pred pr.global_usage) lspred)); - mk_global_pred_correct split_session_pred_func (List.Tot.map (label_session_pred_to_label_local_pred pr.global_usage) lspred) lab (session_pred_to_local_pred pr.global_usage spred) - -val mk_global_session_pred_is_msg: - lspred:list (string & session_pred) -> gu:global_usage -> - time:timestamp -> p:principal -> si:nat -> vi:nat -> st:dy_bytes -> - Lemma - (requires mk_global_session_pred lspred gu time p si vi st) - (ensures is_msg gu (readers [psv_id p si vi]) time st) -let rec mk_global_session_pred_is_msg lspred gu time p si vi st = - match lspred with - | [] -> () - | (current_label, current_spred)::tspred -> - FStar.Classical.move_requires (mk_global_session_pred_is_msg tspred gu time p si vi) st; - match parse (labeled_session dy_bytes) st with - | None -> () - | Some ({label; content}) -> ( - if label = CryptoLib.string_to_bytes current_label then ( - introduce current_spred gu p time si vi content ==> is_msg gu (readers [psv_id p si vi]) time st - with _. ( - // This is the first time I use this lemma from Comparse! - // All that proof effort wasn't for nothing!!! - serialize_parse_inv_lemma (labeled_session dy_bytes) st; - LabeledCryptoAPI.string_to_bytes_lemma #gu #time current_label; - serialize_wf_lemma (labeled_session dy_bytes) (is_msg gu (readers [psv_id p si vi]) time) ({label; content}) - ) - ) else () - ) - -val mk_global_session_pred_later: - lspred:list (string & session_pred) -> gu:global_usage -> - time0:timestamp -> time1:timestamp -> p:principal -> si:nat -> vi:nat -> st:dy_bytes -> - Lemma - (requires mk_global_session_pred lspred gu time0 p si vi st /\ time0 <$ time1) - (ensures mk_global_session_pred lspred gu time1 p si vi st) -let rec mk_global_session_pred_later lspred gu time0 time1 p si vi st = - match lspred with - | [] -> () - | (current_label, current_spred)::tspred -> ( - FStar.Classical.move_requires (mk_global_session_pred_later tspred gu time0 time1 p si vi) st; - match parse (labeled_session dy_bytes) st with - | None -> () - | Some ({label; content}) -> ( - if label = CryptoLib.string_to_bytes current_label then ( - assert(current_spred gu p time0 si vi content ==> mk_global_session_pred lspred gu time1 p si vi st) - ) else () - ) - ) - -(*** LCrypto API for labeled sessions ***) - -let global_timestamp = global_timestamp - -val new_session_number: - pr:preds -> p:principal -> LCrypto nat pr - (requires fun t0 -> True) - (ensures fun t0 r t1 -> t1 == t0) -let new_session_number pr p = new_session_number #pr p - -val new_session: - pr:preds -> label:string -> spred:session_pred -> - p:principal -> si:nat -> vi:nat -> st:dy_bytes -> - LCrypto unit pr - (requires fun t0 -> spred pr.global_usage p (trace_len t0) si vi st /\ has_session_pred pr label spred) - (ensures fun t0 r t1 -> trace_len t1 == trace_len t0 + 1) -let new_session pr label spred p si vi st = - assert_norm (forall session p time si vi. preds_to_global_pred pr (p, time, si, vi, session) <==> pr.trace_preds.session_st_inv time p si vi session); - let time = global_timestamp () in - let session = { - label = CryptoLib.string_to_bytes label; - content = st; - } in - let session_bytes = serialize (labeled_session dy_bytes) session in - parse_serialize_inv_lemma #dy_bytes (labeled_session dy_bytes) session; - new_session #pr #time p si vi session_bytes - -// Roughly a copy-paste of the above -val update_session: - pr:preds -> label:string -> spred:session_pred -> - p:principal -> si:nat -> vi:nat -> st:dy_bytes -> - LCrypto unit pr - (requires fun t0 -> spred pr.global_usage p (trace_len t0) si vi st /\ has_session_pred pr label spred) - (ensures fun t0 r t1 -> trace_len t1 == trace_len t0 + 1) -let update_session pr label spred p si vi st = - assert_norm (forall session p time si vi. preds_to_global_pred pr (p, time, si, vi, session) <==> pr.trace_preds.session_st_inv time p si vi session); - let time = global_timestamp () in - let session = { - label = CryptoLib.string_to_bytes label; - content = st; - } in - let session_bytes = serialize (labeled_session dy_bytes) session in - parse_serialize_inv_lemma #dy_bytes (labeled_session dy_bytes) session; - update_session #pr #time p si vi session_bytes - -val get_session: - pr:preds -> label:string -> spred:session_pred -> - p:principal -> si:nat -> - LCrypto (nat & dy_bytes) pr - (requires fun t0 -> has_session_pred pr label spred) - (ensures fun t0 (vi,st) t1 -> - t1 == t0 /\ - spred pr.global_usage p (trace_len t0) si vi st /\ - is_msg pr.global_usage (readers [psv_id p si vi]) (trace_len t0) st - ) -let get_session pr label spred p si = - assert_norm (forall session p time si vi. preds_to_global_pred pr (p, time, si, vi, session) <==> pr.trace_preds.session_st_inv time p si vi session); - let time = global_timestamp () in - let (|vi, session_bytes|) = get_session #pr #time p si in - // Why the typeclass instantiation?? - match parse (labeled_session dy_bytes) #(parseable_serializeable_labeled_session dy_bytes) (session_bytes <: dy_bytes) with - | Some session -> ( - if session.label = CryptoLib.string_to_bytes label then ( - (vi, session.content) - ) else ( - error "session has wrong label" - ) - ) - | None -> - error "session isn't properly labeled (however it should be forbidden by the session invariant)" diff --git a/fstar/symbolic/MLS.Symbolic.SplitPredicate.fst b/fstar/symbolic/MLS.Symbolic.SplitPredicate.fst deleted file mode 100644 index e116390..0000000 --- a/fstar/symbolic/MLS.Symbolic.SplitPredicate.fst +++ /dev/null @@ -1,155 +0,0 @@ -module MLS.Symbolic.SplitPredicate - -#set-options "--fuel 1 --ifuel 1" - -// Some kind of cheap module functor like ocaml but in F* -noeq type split_predicate_input_values = { - labeled_data_t: Type; - label_t: Type; - encoded_label_t: Type; - raw_data_t: Type; - - decode_labeled_data: labeled_data_t -> GTot (option (encoded_label_t & raw_data_t)); - - encode_label: label_t -> encoded_label_t; - encode_label_inj: l1:label_t -> l2:label_t -> Lemma - (requires encode_label l1 == encode_label l2) - (ensures l1 == l2) - ; -} - -// Can probably be generalized to handle kdf usage too? -type global_pred (func:split_predicate_input_values) = - func.labeled_data_t -> prop -type local_pred (func:split_predicate_input_values) = - func.raw_data_t -> prop - -val has_local_pred: func:split_predicate_input_values -> global_pred func -> func.label_t -> local_pred func -> prop -let has_local_pred func gpred the_label lpred = - forall labeled_data. - match func.decode_labeled_data labeled_data with - | Some (label, raw_data) -> - label == func.encode_label the_label ==> (gpred labeled_data <==> lpred raw_data) - | None -> True - -val mk_global_pred: func:split_predicate_input_values -> list (func.label_t & local_pred func) -> global_pred func -let rec mk_global_pred func l labeled_data = - match l with - | [] -> False - | (the_label, lpred)::t -> - let cur_prop = - match func.decode_labeled_data labeled_data with - | Some (label, raw_data) -> - label == func.encode_label the_label /\ lpred raw_data - | None -> False - in - cur_prop \/ mk_global_pred func t labeled_data - -val mk_global_pred_wrong_label: - func:split_predicate_input_values -> the_label:func.label_t -> - l:list (func.label_t & local_pred func) -> labeled_data:func.labeled_data_t -> - Lemma - (requires ~(List.Tot.memP the_label (List.Tot.map fst l))) - (ensures ( - match func.decode_labeled_data labeled_data with - | Some (label, raw_data) -> - label == func.encode_label the_label ==> ~(mk_global_pred func l labeled_data) - | None -> ~(mk_global_pred func l labeled_data) - )) -let rec mk_global_pred_wrong_label func the_label l labeled_data = - match l with - | [] -> () - | (label, _)::t -> ( - FStar.Classical.move_requires_2 func.encode_label_inj the_label label; - mk_global_pred_wrong_label func the_label t labeled_data - ) - -val disjointP: #a:Type -> list a -> list a -> prop -let rec disjointP #a l1 l2 = - match l1 with - | [] -> True - | h1::t1 -> - ~(List.Tot.memP h1 l2) /\ disjointP t1 l2 - -val disjointP_cons: - #a:Type -> - x:a -> l1:list a -> l2:list a -> - Lemma - (requires disjointP l1 l2 /\ ~(List.Tot.memP x l1)) - (ensures disjointP l1 (x::l2)) -let rec disjointP_cons #a x l1 l2 = - match l1 with - | [] -> () - | h1::t1 -> disjointP_cons x t1 l2 - -val memP_map: - #a:Type -> #b:Type -> - x:a -> f:(a -> b) -> l:list a -> - Lemma - (requires List.Tot.memP x l) - (ensures List.Tot.memP (f x) (List.Tot.map f l)) -let rec memP_map #a #b x f l = - match l with - | [] -> () - | h::t -> - introduce x =!= h ==> List.Tot.memP (f x) (List.Tot.map f t) - with _. memP_map x f t - -val mk_global_pred_correct_aux: - func:split_predicate_input_values -> gpred:global_pred func -> - lpreds1:list (func.label_t & local_pred func) -> lpreds2:list (func.label_t & local_pred func) -> - the_label:func.label_t -> lpred:local_pred func -> - Lemma - (requires - (forall labeled_data. (mk_global_pred func lpreds1 labeled_data \/ mk_global_pred func lpreds2 labeled_data) <==> gpred labeled_data) /\ - List.Tot.no_repeats_p (List.Tot.map fst lpreds1) /\ - disjointP (List.Tot.map fst lpreds1) (List.Tot.map fst lpreds2) /\ - List.Tot.memP (the_label, lpred) lpreds1 - ) - (ensures has_local_pred func gpred the_label lpred) -let rec mk_global_pred_correct_aux func gpred lpreds1 lpreds2 the_label lpred = - match lpreds1 with - | [] -> () - | (h_lab, h_spred)::t -> ( - eliminate h_lab == the_label \/ h_lab =!= the_label returns _ with _. ( - introduce forall labeled_data. ( - match func.decode_labeled_data labeled_data with - | Some (label, raw_data) -> - label == func.encode_label the_label ==> (gpred labeled_data <==> lpred raw_data) - | None -> True - ) with ( - match func.decode_labeled_data labeled_data with - | Some (label, raw_data) -> ( - eliminate label == func.encode_label the_label \/ label =!= func.encode_label the_label returns _ with _. ( - func.encode_label_inj the_label h_lab; - mk_global_pred_wrong_label func the_label t labeled_data; - mk_global_pred_wrong_label func the_label lpreds2 labeled_data; - FStar.Classical.move_requires_3 memP_map (the_label, lpred) fst t - ) and _. () - ) - | None -> () - ) - ) and _. ( - disjointP_cons h_lab (List.Tot.map fst t) (List.Tot.map fst lpreds2); - mk_global_pred_correct_aux func gpred t ((h_lab, h_spred)::lpreds2) the_label lpred - ) - ) - -val disjointP_nil: #a:Type -> l:list a -> Lemma (disjointP l []) -let rec disjointP_nil #a l = - match l with - | [] -> () - | _::t -> disjointP_nil t - -val mk_global_pred_correct: - func:split_predicate_input_values -> lpreds:list (func.label_t & local_pred func) -> - the_label:func.label_t -> lpred:local_pred func -> - Lemma - (requires - List.Tot.no_repeats_p (List.Tot.map fst lpreds) /\ - List.Tot.memP (the_label, lpred) lpreds - ) - (ensures has_local_pred func (mk_global_pred func lpreds) the_label lpred) -let mk_global_pred_correct func lpreds the_label lpred = - disjointP_nil (List.Tot.map fst lpreds); - mk_global_pred_correct_aux func (mk_global_pred func lpreds) lpreds [] the_label lpred diff --git a/fstar/symbolic/MLS.Symbolic.TypedSession.fst b/fstar/symbolic/MLS.Symbolic.TypedSession.fst deleted file mode 100644 index 2b36dde..0000000 --- a/fstar/symbolic/MLS.Symbolic.TypedSession.fst +++ /dev/null @@ -1,67 +0,0 @@ -module MLS.Symbolic.TypedSession - -open Comparse -open MLS.Symbolic -open MLS.Symbolic.Session -open LabeledRuntimeAPI - -type bare_typed_session_pred (a:Type) {|parseable_serializeable dy_bytes a|} = gu:global_usage -> p:principal -> time:timestamp -> si:nat -> vi:nat -> session:a -> prop - -val bare_typed_session_pred_later: #a:Type -> {|parseable_serializeable dy_bytes a|} -> bare_typed_session_pred a -> prop -let bare_typed_session_pred_later #a #ps_a spred = - forall gu p time0 time1 si vi session. - (spred gu p time0 si vi session /\ time0 <$ time1) - ==> - spred gu p time1 si vi session - -val bare_typed_session_pred_is_msg: #a:Type -> {|parseable_serializeable dy_bytes a|} -> bare_typed_session_pred a -> prop -let bare_typed_session_pred_is_msg #a #ps_a spred = - forall gu p time si vi session. - spred gu p time si vi session - ==> - is_well_formed _ (is_msg gu (readers [psv_id p si vi]) time) session - -type typed_session_pred (a:Type) {|parseable_serializeable dy_bytes a|} = spred:bare_typed_session_pred a{bare_typed_session_pred_later spred /\ bare_typed_session_pred_is_msg spred} - -val typed_session_pred_to_session_pred: #a:Type -> {|parseable_serializeable dy_bytes a|} -> typed_session_pred a -> session_pred -let typed_session_pred_to_session_pred #a #ps_a tspred = - let bare_spred gu p time si vi session: prop = - match parse a session with - | None -> False - | Some st -> tspred gu p time si vi st - in - mk_session_pred bare_spred - (fun gu p time0 time1 si vi session -> ()) - (fun gu p time si vi session -> - let st = Some?.v (parse a session) in - let pre = is_msg gu (readers [psv_id p si vi]) time in - serialize_parse_inv_lemma a session; - serialize_wf_lemma a pre st - ) - -val mk_typed_session_pred: - #a:Type -> {|parseable_serializeable dy_bytes a|} -> - tspred:bare_typed_session_pred a -> - (gu:global_usage -> p:principal -> time0:timestamp -> time1:timestamp -> si:nat -> vi:nat -> session:a -> Lemma - (requires tspred gu p time0 si vi session /\ time0 <$ time1) - (ensures tspred gu p time1 si vi session) - ) -> - (gu:global_usage -> p:principal -> time:timestamp -> si:nat -> vi:nat -> session:a -> Lemma - (requires tspred gu p time si vi session) - (ensures is_well_formed _ (is_msg gu (readers [psv_id p si vi]) time) session) - ) -> - typed_session_pred a -let mk_typed_session_pred #a #ps_a tspred later_lemma is_msg_lemma = - introduce forall gu p time0 time1 si vi session. (tspred gu p time0 si vi session /\ time0 <$ time1) ==> tspred gu p time1 si vi session - with ( - introduce _ ==> _ with _. ( - later_lemma gu p time0 time1 si vi session - ) - ); - introduce forall gu p time si vi session. tspred gu p time si vi session ==> is_well_formed _ (is_msg gu (readers [psv_id p si vi]) time) session - with ( - introduce _ ==> _ with _. ( - is_msg_lemma gu p time si vi session - ) - ); - tspred diff --git a/fstar/symbolic/MLS.Symbolic.fst b/fstar/symbolic/MLS.Symbolic.fst index 614a79b..89dce41 100644 --- a/fstar/symbolic/MLS.Symbolic.fst +++ b/fstar/symbolic/MLS.Symbolic.fst @@ -1,68 +1,41 @@ module MLS.Symbolic open Comparse +open DY.Core open MLS.Crypto -open ComparseGlue open MLS.NetworkTypes -open MLS.Symbolic.SplitPredicate +open DY.Lib.SplitPredicate open MLS.Result -#push-options "--fuel 1 --ifuel 1" +#push-options "--fuel 0 --ifuel 0" (*** Typeclass instantiation on DY* ***) val dy_bytes: eqtype -let dy_bytes = CryptoLib.bytes - -/// At this time, DY* doesn't expose lengths for cryptographic functions. Therefore we assume them here. -/// Assuming them is sound since no similar properties are exposed by DY*. -/// This will have to be cleaned up the day DY* exposes lengths for cryptographic functions. - -assume val dy_kdf_length: nat -assume val dy_kdf_length_lemma: - key:dy_bytes -> data:dy_bytes -> - Lemma - (length (CryptoLib.extract key data) == dy_kdf_length) - -assume val dy_sign_public_key_length: nat -assume val dy_sign_private_key_length: nat -assume val dy_sign_nonce_length: nat -assume val dy_sign_signature_length: n:nat{n < 256} - -assume val dy_aead_nonce_length: n:nat{4 <= n} -assume val dy_aead_key_length: nat - -assume val dy_hmac_length: n:nat{n < 256} -assume val dy_hmac_length_lemma: - key:dy_bytes -> data:dy_bytes -> - Lemma - (length (CryptoLib.mac key data) == dy_hmac_length) +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 = { - base = dy_bytes_like; + base = DY.Lib.bytes_like_bytes; bytes_hasEq = (); ciphersuite = acs; hash_hash = (fun buf -> - return (CryptoLib.hash buf) + return (DY.Core.hash buf) ); hash_max_input_length = pow2 256; //infinity! hash_hash_pre = (fun buf -> ()); - hash_output_length_bound = (fun buf -> assume(CryptoLib.hash buf <> empty)); + hash_output_length_bound = (fun buf -> assume(DY.Core.hash buf <> empty)); - kdf_length = dy_kdf_length; + kdf_length = magic(); kdf_extract = (fun key data -> - dy_kdf_length_lemma key data; - return (CryptoLib.extract key data) + admit() ); kdf_expand = (fun prk info len -> - // TODO: expose the length in DY* - // (used in TreeKEM, TreeDEM) - admit(); - return (CryptoLib.expand prk info) + admit() ); hpke_public_key_length = magic(); @@ -71,61 +44,47 @@ let dy_bytes_has_crypto acs = { hpke_private_key_length_bound = magic(); hpke_kem_output_length = magic(); hpke_gen_keypair = (fun ikm -> - // TODO: actually implement HPKE in DY* - // (used in TreeKEM) - admit(); - return (ikm, CryptoLib.pk ikm) + admit() ); hpke_encrypt = (fun pkR info ad plaintext rand -> - // TODO: actually implement HPKE in DY* - // (no info/ad nor kem output) - // (used in TreeKEM) - admit(); - return (CryptoLib.pke_enc pkR rand plaintext, CryptoLib.empty) + admit() ); hpke_decrypt = (fun enc skR info ad ciphertext -> - // TODO: actually implement HPKE in DY* - // (no info/ad nor kem output) - // (used in TreeKEM) - match CryptoLib.pke_dec skR ciphertext with - | SecrecyLabels.Success res -> return res - | SecrecyLabels.Error e -> error e + admit() ); - sign_gen_keypair_min_entropy_length = dy_sign_private_key_length; + sign_gen_keypair_min_entropy_length = magic(); sign_gen_keypair = (fun rand -> - return (CryptoLib.vk rand, rand) + return (DY.Core.vk rand, rand) ); - sign_sign_min_entropy_length = dy_sign_nonce_length; + sign_sign_min_entropy_length = magic(); sign_sign = (fun sk msg rand -> - return (CryptoLib.sign sk rand msg) + return (DY.Core.sign sk rand msg) ); sign_verify = (fun pk msg signature -> - CryptoLib.verify pk msg signature + DY.Core.verify pk msg signature ); - aead_nonce_length = dy_aead_nonce_length; - aead_nonce_length_bound = (); - aead_key_length = dy_aead_key_length; + aead_nonce_length = magic(); + aead_nonce_length_bound = magic(); + aead_key_length = magic(); aead_encrypt = (fun key nonce ad plaintext -> - return (CryptoLib.aead_enc key nonce plaintext ad) + return (DY.Core.aead_enc key nonce plaintext ad) ); aead_decrypt = (fun key nonce ad ciphertext -> - match CryptoLib.aead_dec key nonce ciphertext ad with - | SecrecyLabels.Success res -> return res - | SecrecyLabels.Error e -> error e + match DY.Core.aead_dec key nonce ciphertext ad with + | Some res -> return res + | None -> error "aead_decrypt: couldn't decrypt" ); - hmac_length = dy_hmac_length; - hmac_length_bound = (); + hmac_length = magic(); + hmac_length_bound = magic(); hmac_hmac = (fun key data -> - dy_hmac_length_lemma key data; - return (CryptoLib.mac key data) + admit() ); string_to_bytes = (fun s -> - CryptoLib.string_to_bytes_len s; - CryptoLib.string_to_bytes s + (ps_whole_ascii_string.serialize s <: dy_bytes) ); unsafe_split = (fun buf i -> @@ -137,151 +96,10 @@ let dy_bytes_has_crypto acs = { debug_bytes_to_string = (fun b -> ""); } +#pop-options instance crypto_dy_bytes: crypto_bytes dy_bytes = dy_bytes_has_crypto AC_mls_128_dhkemx25519_chacha20poly1305_sha256_ed25519 -(*** Abbreviations for DY* functions ***) - -val principal: Type0 -let principal = SecrecyLabels.principal - -val ps_principal: #bytes:Type0 -> {|bytes_like bytes|} -> parser_serializer bytes principal -let ps_principal #bytes #bl = ps_principal #bytes - -val timestamp: Type0 -let timestamp = SecrecyLabels.timestamp - -val ps_timestamp: #bytes:Type0 -> {|bytes_like bytes|} -> parser_serializer bytes timestamp -let ps_timestamp #bytes #bl = ps_nat #bytes - -val key_usages: Type0 -let key_usages = LabeledCryptoAPI.key_usages - -// In universe 1 because it contains predicates -val global_usage: Type u#1 -let global_usage = LabeledCryptoAPI.global_usage - -val preds: Type u#1 -let preds = LabeledRuntimeAPI.preds - -val label: Type0 -let label = SecrecyLabels.label - -val id: Type0 -let id = SecrecyLabels.id - -// Exposing the constructor directly would have been nice, but that's not possible -val p_id: principal -> id -let p_id p = SecrecyLabels.P p - -val ps_id: principal -> nat -> id -let ps_id p s = SecrecyLabels.S p s - -val psv_id: principal -> nat -> nat -> id -let psv_id p s v = SecrecyLabels.V p s v - -val public: label -let public = SecrecyLabels.public - -val readers: list id -> label -let readers l = SecrecyLabels.readers l - -val usage: Type0 -let usage = CryptoLib.usage - -val sig_usage: string -> usage -let sig_usage usg = CryptoLib.sig_usage usg - -val can_flow: ts:timestamp -> from:label -> to:label -> prop -let can_flow = LabeledCryptoAPI.can_flow - -// Why a dollar? Because time is money! -let (<$) (t1:timestamp) (t2:timestamp) = SecrecyLabels.later_than t2 t1 - -val get_usage: global_usage -> dy_bytes -> (option usage) -let get_usage p b = LabeledCryptoAPI.get_usage p.key_usages b - -val get_label: global_usage -> dy_bytes -> label -let get_label p b = LabeledCryptoAPI.get_label p.key_usages b - -val is_valid: p:global_usage -> i:timestamp -> bytes_compatible_pre dy_bytes -let is_valid p i = LabeledCryptoAPI.is_valid p i - -val is_labeled: global_usage -> label -> timestamp -> dy_bytes -> prop -let is_labeled p l i b = is_valid p i b /\ get_label p b == l - -val has_usage: global_usage -> usage -> timestamp -> dy_bytes -> prop -let has_usage p u i b = LabeledCryptoAPI.has_usage p i b u - -val is_secret: global_usage -> usage -> label -> timestamp -> dy_bytes -> prop -let is_secret p u l i b = LabeledCryptoAPI.is_secret p i b l u - -val is_msg: global_usage -> label -> timestamp -> bytes_compatible_pre dy_bytes -let is_msg p l i = ComparseGlue.is_msg p l i - -val is_publishable: global_usage -> timestamp -> bytes_compatible_pre dy_bytes -let is_publishable p i = is_msg p SecrecyLabels.public i - -val is_verification_key: global_usage -> string -> label -> timestamp -> dy_bytes -> prop -let is_verification_key gu usg sk_lab time vk = LabeledCryptoAPI.is_verification_key gu time vk sk_lab usg - -val is_signature_key: global_usage -> string -> label -> timestamp -> dy_bytes -> prop -let is_signature_key gu usg sk_lab time sk = LabeledCryptoAPI.is_signing_key gu time sk sk_lab usg - -val get_signkey_label: key_usages -> dy_bytes -> label -let get_signkey_label ku vk = LabeledCryptoAPI.get_signkey_label ku vk - -val is_verification_key_to_signkey_label: gu:global_usage -> usg:string -> sk_lab:label -> time:timestamp -> vk:dy_bytes -> Lemma - (requires is_verification_key gu usg sk_lab time vk) - (ensures get_signkey_label gu.key_usages vk == sk_lab) -let is_verification_key_to_signkey_label gu usg sk_lab time vk = - LabeledCryptoAPI.verification_key_label_lemma gu time vk sk_lab - -val event: Type0 -let event = CryptoEffect.event - -val did_event_occur_before: principal -> timestamp -> event -> prop -let did_event_occur_before prin time e = GlobalRuntimeLib.did_event_occur_before time prin e - -val event_pred_at: preds -> principal -> timestamp -> event -> prop -let event_pred_at pr prin time e = LabeledRuntimeAPI.event_pred_at pr time prin e - -val hash_hash_inj: - b1:dy_bytes -> b2:dy_bytes -> - Lemma ( - length b1 < hash_max_input_length #dy_bytes /\ - length b2 < hash_max_input_length #dy_bytes /\ - hash_hash b1 == hash_hash b2 ==> - b1 == b2 - ) -let hash_hash_inj b1 b2 = CryptoLib.hash_inj_lemma b1 b2 - -val is_corrupt: timestamp -> id -> prop -let is_corrupt time x = LabeledCryptoAPI.corrupt_id time x - -val can_flow_to_public_implies_corruption: - time:timestamp -> x:id -> - Lemma - (requires (can_flow time (readers [x]) public)) - (ensures is_corrupt time x) -let can_flow_to_public_implies_corruption time x = LabeledCryptoAPI.can_flow_to_public_implies_corruption time x - -val readers_is_injective: - x:principal -> y:principal -> - Lemma - (requires readers [p_id x] == readers [p_id y]) - (ensures x == y) -let readers_is_injective x y = - SecrecyLabels.readers_is_injective x - -val can_flow_transitive: - time:timestamp -> l1:label -> l2:label -> l3:label -> - Lemma - (requires can_flow time l1 l2 /\ can_flow time l2 l3) - (ensures can_flow time l1 l3) -let can_flow_transitive time l1 l2 l3 = - LabeledCryptoAPI.can_flow_transitive time l1 l2 l3 - (*** Labeled signature predicate ***) val get_mls_label_inj: @@ -292,116 +110,154 @@ val get_mls_label_inj: let get_mls_label_inj l1 l2 = String.concat_injective "MLS 1.0 " "MLS 1.0 " l1 l2 -let split_sign_pred_func: split_predicate_input_values = { - labeled_data_t = (string & timestamp & dy_bytes & dy_bytes); - label_t = valid_label; - encoded_label_t = mls_ascii_string; - raw_data_t = (string & timestamp & dy_bytes & dy_bytes); +type verif_key_t {|crypto_usages|} = vk:dy_bytes{SigKey? (get_signkey_usage vk)} + +noeq +type mls_sign_pred {|crypto_usages|} = { + pred: trace -> key:verif_key_t -> msg:dy_bytes -> prop; + pred_later: + tr1:trace -> tr2:trace -> + key:verif_key_t -> msg:dy_bytes -> + Lemma + (requires pred tr1 key msg /\ tr1 <$ tr2) + (ensures pred tr2 key msg) + ; +} - decode_labeled_data = (fun (usg, time, key, data) -> ( - match parse (sign_content_nt dy_bytes) data with - | Some ({label; content}) -> Some (label, (usg, time, key, content)) - | None -> None - )); +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; - encode_label = get_mls_label; - encode_label_inj = get_mls_label_inj; -} + raw_data_t = (trace & verif_key_t & dy_bytes); + tagged_data_t = (trace & verif_key_t & dy_bytes); -let sign_pred = usage:string -> timestamp -> key:dy_bytes -> msg:dy_bytes -> prop + 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 _ _ -> ()); -val sign_pred_to_local_pred: sign_pred -> local_pred split_sign_pred_func -let sign_pred_to_local_pred spred (usg, time, key, msg) = - spred usg time key msg + tag_t = valid_label; + encoded_tag_t = mls_ascii_string; -val global_usage_to_global_pred: global_usage -> global_pred split_sign_pred_func -let global_usage_to_global_pred gu (usg, time, key, msg) = - gu.usage_preds.can_sign time usg key msg + encode_tag = get_mls_label; + encode_tag_inj = get_mls_label_inj; + + 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 + )); +} -val has_sign_pred: global_usage -> valid_label -> sign_pred -> prop -let has_sign_pred gu lab spred = - has_local_pred split_sign_pred_func (global_usage_to_global_pred gu) lab (sign_pred_to_local_pred spred) +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) -// We can omit the `is_publishable` disjunction in the precondition, -// because it will never be used inside a protocol security proof. -// It can however be used to demonstrate attacks, but that is not our goal. #push-options "--z3rlimit 25" -val sign_with_label_valid: - gu:global_usage -> spred:sign_pred -> usg:string -> time:timestamp -> +val bytes_invariant_sign_with_label: + {|ci:crypto_invariants|} -> spred:mls_sign_pred -> tr:trace -> sk:dy_bytes -> lab:valid_label -> msg:mls_bytes dy_bytes -> nonce:sign_nonce dy_bytes -> Lemma (requires - is_valid gu time sk /\ ( (* is_publishable gu time sk \/ *) get_usage gu sk == Some (sig_usage usg)) /\ - is_valid gu time nonce /\ - get_label gu sk == get_label gu nonce /\ - is_valid gu time msg /\ - has_sign_pred gu lab spred /\ (exists time_sig. time_sig <$ time /\ spred usg time_sig (CryptoLib.vk sk) msg) + bytes_invariant tr sk /\ + bytes_invariant tr nonce /\ + bytes_invariant tr msg /\ + SigKey? (get_usage sk) /\ + SigNonce? (get_usage nonce) /\ + (get_label sk) `can_flow tr` (get_label nonce) /\ + has_sign_pred ci (lab, spred) /\ + spred.pred tr (vk sk) msg ) (ensures - is_valid gu time (Success?.v (sign_with_label sk lab msg nonce)) /\ - can_flow time (get_label gu (Success?.v (sign_with_label sk lab msg nonce))) (get_label gu msg) + bytes_invariant tr (Success?.v (sign_with_label sk lab msg nonce)) /\ + (get_label (Success?.v (sign_with_label sk lab msg nonce))) `can_flow tr` (get_label msg) ) -let sign_with_label_valid gu spred usg time sk lab msg nonce = - assert_norm (forall msg usg time key. global_usage_to_global_pred gu (usg, time, key, msg) <==> gu.usage_preds.can_sign time usg key msg); //??? +let bytes_invariant_sign_with_label #ci spred tr sk lab msg nonce = let sign_content: sign_content_nt dy_bytes = { label = get_mls_label lab; content = msg; } in - serialize_wf_lemma (sign_content_nt dy_bytes) (is_valid gu time) sign_content; - serialize_wf_lemma (sign_content_nt dy_bytes) (is_msg gu (get_label gu msg) time) sign_content; - parse_serialize_inv_lemma #dy_bytes (sign_content_nt dy_bytes) sign_content; - let sign_content_bytes: dy_bytes = serialize (sign_content_nt dy_bytes) sign_content in - LabeledCryptoAPI.sign_lemma #gu #time #(get_label gu sk) #(get_label gu sign_content_bytes) sk nonce sign_content_bytes; - can_flow_transitive time (get_label gu (CryptoLib.sign sk nonce sign_content_bytes)) (get_label gu sign_content_bytes) (get_label gu msg) + 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))) #pop-options -val verify_with_label_is_valid: - gu:global_usage -> spred:sign_pred -> usg:string -> sk_label:label -> time:timestamp -> +val bytes_invariant_verify_with_label: + {|ci:crypto_invariants|} -> spred:mls_sign_pred -> tr:trace -> vk:dy_bytes -> lab:valid_label -> content:mls_bytes dy_bytes -> signature:dy_bytes -> Lemma (requires - has_sign_pred gu lab spred /\ - is_verification_key gu usg sk_label time vk /\ - is_valid gu time content /\ - is_valid gu time signature /\ + has_sign_pred ci (lab, spred) /\ + bytes_invariant tr vk /\ + bytes_invariant tr content /\ + bytes_invariant tr signature /\ verify_with_label vk lab content signature ) - (ensures can_flow time sk_label public \/ (exists time_sig. time_sig <$ time /\ spred usg time_sig vk content)) -let verify_with_label_is_valid gu spred usg sk_label time vk lab content signature = - assert_norm (forall msg usg time key. global_usage_to_global_pred gu (usg, time, key, msg) <==> gu.usage_preds.can_sign time usg key msg); //??? + (ensures + ( + SigKey? (get_signkey_usage vk) ==> + spred.pred tr vk content + ) \/ ( + (get_signkey_label vk) `can_flow tr` public + ) + ) +let bytes_invariant_verify_with_label #ci spred tr vk lab content signature = let sign_content: sign_content_nt dy_bytes = { label = get_mls_label lab; content = content; } in - serialize_wf_lemma (sign_content_nt dy_bytes) (is_valid gu time) sign_content; - parse_serialize_inv_lemma #dy_bytes (sign_content_nt dy_bytes) sign_content; - let sign_content_bytes: dy_bytes = serialize (sign_content_nt dy_bytes) sign_content in - LabeledCryptoAPI.verify_lemma #gu #time #SecrecyLabels.private_label #SecrecyLabels.private_label vk sign_content_bytes signature - -val label_sign_pred_to_label_local_pred: valid_label & sign_pred -> valid_label & local_pred split_sign_pred_func -let label_sign_pred_to_label_local_pred (label, spred) = - (label, sign_pred_to_local_pred spred) - -val mk_can_sign: list (valid_label & sign_pred) -> timestamp -> string -> dy_bytes -> dy_bytes -> prop -let mk_can_sign l time usg key msg = - mk_global_pred split_sign_pred_func (List.Tot.map label_sign_pred_to_label_local_pred l) (usg, time, key, msg) - -val mk_can_sign_correct: - gu:global_usage -> lspred:list (valid_label & sign_pred) -> - lab:valid_label -> spred:sign_pred -> + 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))) + else () + +val mk_sign_pred: + {|crypto_usages|} -> + list (valid_label & mls_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 + +#push-options "--ifuel 1" +val mk_sign_pred_later: + {|crypto_usages|} -> + lspred:list (valid_label & mls_sign_pred) -> + tr1:trace -> tr2:trace -> + vk:verif_key_t -> msg:dy_bytes -> Lemma (requires - gu.usage_preds.can_sign == mk_can_sign lspred /\ - List.Tot.no_repeats_p (List.Tot.map fst lspred) /\ - List.Tot.memP (lab, spred) lspred + mk_sign_pred lspred tr1 vk msg /\ + tr1 <$ tr2 + ) + (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)) ) - (ensures has_sign_pred gu lab spred) -let mk_can_sign_correct gu lspred lab spred = - let open MLS.MiscLemmas in - assert_norm (forall msg usg time key. global_usage_to_global_pred gu (usg, time, key, msg) <==> gu.usage_preds.can_sign time usg key msg); //??? - memP_map (lab, spred) label_sign_pred_to_label_local_pred lspred; - FStar.Classical.forall_intro_2 (index_map label_sign_pred_to_label_local_pred); - FStar.Classical.forall_intro_2 (index_map (fst #valid_label #sign_pred)); - FStar.Classical.forall_intro_2 (index_map (fst #valid_label #(local_pred split_sign_pred_func))); - List.Tot.index_extensionality (List.Tot.map fst lspred) (List.Tot.map fst (List.Tot.map label_sign_pred_to_label_local_pred lspred)); - mk_global_pred_correct split_sign_pred_func (List.Tot.map label_sign_pred_to_label_local_pred lspred) lab (sign_pred_to_local_pred spred) +#pop-options + +#push-options "--ifuel 1" +val mk_sign_pred_correct: + ci:crypto_invariants -> lspred:list (valid_label & mls_sign_pred) -> + Lemma + (requires + sign_pred == mk_sign_pred lspred /\ + List.Tot.no_repeats_p (List.Tot.map fst lspred) + ) + (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)) +#pop-options diff --git a/fstar/treesync/code/MLS.TreeSync.API.Types.fst b/fstar/treesync/code/MLS.TreeSync.API.Types.fst index c748347..9dc5197 100644 --- a/fstar/treesync/code/MLS.TreeSync.API.Types.fst +++ b/fstar/treesync/code/MLS.TreeSync.API.Types.fst @@ -9,10 +9,19 @@ open MLS.TreeSync.Invariants.AuthService (** TreeSync state and accessors *) noeq -type treesync_state (bytes:Type0) {|crypto_bytes bytes|} (tkt:treekem_types bytes) (asp:as_parameters bytes) (group_id:mls_bytes bytes) = { +type treesync_state (bytes:Type0) {|crypto_bytes bytes|} (tkt:treekem_types bytes) (token_t:Type0) (group_id:mls_bytes bytes) = { levels: nat; tree: treesync_valid bytes tkt levels 0 group_id; - tokens: tokens:as_tokens bytes asp.token_t levels 0{all_credentials_ok tree tokens}; + tokens: as_tokens bytes token_t levels 0; } -type treesync_index (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#asp:as_parameters bytes) (#group_id:mls_bytes bytes) (st:treesync_state bytes tkt asp group_id) = i:nat{i < pow2 st.levels} +val treesync_state_valid: + #bytes:Type0 -> {|crypto_bytes bytes|} -> + #tkt:treekem_types bytes -> asp:as_parameters bytes -> + #group_id:mls_bytes bytes -> + treesync_state bytes tkt asp.token_t group_id -> + prop +let treesync_state_valid #bytes #cb #tkt asp #group_id st = + all_credentials_ok st.tree st.tokens + +type treesync_index (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#token_t:Type0) (#group_id:mls_bytes bytes) (st:treesync_state bytes tkt token_t group_id) = i:nat{i < pow2 st.levels} diff --git a/fstar/treesync/code/MLS.TreeSync.API.fst b/fstar/treesync/code/MLS.TreeSync.API.fst index 9611617..a0e96ec 100644 --- a/fstar/treesync/code/MLS.TreeSync.API.fst +++ b/fstar/treesync/code/MLS.TreeSync.API.fst @@ -35,18 +35,18 @@ let as_token_for token:asp.token_t{ asp.credential_ok inp token } val state_leaf_at: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - st:treesync_state bytes tkt asp group_id -> li:treesync_index st{Some? (leaf_at st.tree li)} -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + st:treesync_state bytes tkt token_t group_id -> li:treesync_index st{Some? (leaf_at st.tree li)} -> leaf_node_nt bytes tkt -let state_leaf_at #bytes #cb #tkt #asp #group_id st li = +let state_leaf_at #bytes #cb #tkt #token_t #group_id st li = Some?.v (leaf_at st.tree li) val state_update_tree: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> #l:nat -> - st:treesync_state bytes tkt asp group_id -> new_tree:treesync_valid bytes tkt l 0 group_id -> new_tokens:as_tokens bytes asp.token_t l 0{all_credentials_ok new_tree new_tokens} -> - treesync_state bytes tkt asp group_id -let state_update_tree #bytes #cb #tkt #asp #group_id #l st new_tree new_tokens = + st:treesync_state bytes tkt token_t group_id -> new_tree:treesync_valid bytes tkt l 0 group_id -> new_tokens:as_tokens bytes token_t l 0 -> + treesync_state bytes tkt token_t group_id +let state_update_tree #bytes #cb #tkt #token_t #group_id #l st new_tree new_tokens = ({ levels = l; tree = new_tree; @@ -70,12 +70,6 @@ type pending_create as_input: as_input_for ln; } -type token_for_create - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) - (#group_id:mls_bytes bytes) (#ln:leaf_node_nt bytes tkt) - (asp:as_parameters bytes) (pend:pending_create group_id ln) = - as_token_for asp pend.as_input - val prepare_create: #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> group_id:mls_bytes bytes -> ln:leaf_node_nt bytes tkt -> @@ -91,19 +85,28 @@ let prepare_create #bytes #cb #tkt group_id ln = ) val finalize_create: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> #ln:leaf_node_nt bytes tkt -> - pend:pending_create group_id ln -> token:token_for_create asp pend -> - treesync_state bytes tkt asp group_id + pend:pending_create group_id ln -> token:token_t -> + treesync_state bytes tkt token_t group_id let finalize_create #bytes #cb #tkt #asp #group_id #ln pend token = pend.can_create_proof; - all_credentials_ok_tree_create ln token; ({ levels = 0; tree = tree_create ln; tokens = MLS.TreeCommon.tree_create (Some token); }) +val finalize_create_valid: + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> + #group_id:mls_bytes bytes -> #ln:leaf_node_nt bytes tkt -> + pend:pending_create group_id ln -> token:asp.token_t -> + Lemma + (requires asp.credential_ok pend.as_input token) + (ensures treesync_state_valid asp (finalize_create pend token)) +let finalize_create_valid #bytes #cb #tkt #asp #group_id #ln pend token = + all_credentials_ok_tree_create ln token + (*** Welcome ***) let pending_welcome_proof @@ -130,19 +133,6 @@ type pending_welcome } #pop-options -type tokens_for_welcome - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#l:nat) - (#group_id:mls_bytes bytes) (#t:treesync bytes tkt l 0) - (asp:as_parameters bytes) (pend:pending_welcome group_id t) = - tokens:list (option asp.token_t){ - List.Tot.length tokens == pow2 l /\ ( - forall li. match List.Tot.index pend.as_inputs li, List.Tot.index tokens li with - | Some as_inp, Some token -> asp.credential_ok as_inp token - | None, None -> True - | _, _ -> False - ) - } - val prepare_welcome: #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #l:nat -> @@ -171,62 +161,77 @@ let prepare_welcome #bytes #cb #tkt #l group_id t = #push-options "--fuel 2 --ifuel 2" val tokens_from_list: - #bytes:Type0 -> {|bytes_like bytes|} -> - asp:as_parameters bytes -> l:nat -> i:tree_index l -> tokens:list (option asp.token_t){List.Tot.length tokens == pow2 l} -> - as_tokens bytes asp.token_t l i -let rec tokens_from_list #bytes #bl asp l i tokens = + #bytes:Type0 -> {|bytes_like bytes|} -> #token_t:Type0 -> + l:nat -> i:tree_index l -> tokens:list (option token_t){List.Tot.length tokens == pow2 l} -> + as_tokens bytes token_t l i +let rec tokens_from_list #bytes #bl #token_t l i tokens = if l = 0 then ( let [token] = tokens in TLeaf token ) else ( let tokens_left, tokens_right = List.Tot.splitAt (pow2 (l-1)) tokens in List.Pure.splitAt_length (pow2 (l-1)) tokens; - TNode () (tokens_from_list asp _ _ tokens_left) (tokens_from_list asp _ _ tokens_right) + TNode () (tokens_from_list #bytes _ _ tokens_left) (tokens_from_list #bytes _ _ tokens_right) ) #pop-options +val finalize_welcome: + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> + #l:nat -> #group_id:mls_bytes bytes -> #t:treesync bytes tkt l 0 -> + pend:pending_welcome group_id t -> tokens:list (option token_t){List.Tot.length tokens == pow2 l} -> + treesync_state bytes tkt token_t group_id +let finalize_welcome #bytes #cb #tkt #token_t #l #group_id #t pend tokens = + pend.can_welcome_proof; + let tokens_tree = tokens_from_list l 0 tokens in + ({ + levels = l; + tree = t; + tokens = tokens_tree; + }) + #push-options "--fuel 1" val leaf_at_token_from_list: - #bytes:Type0 -> {|bytes_like bytes|} -> - asp:as_parameters bytes -> l:nat -> i:tree_index l -> tokens:list (option asp.token_t){List.Tot.length tokens == pow2 l} -> li:leaf_index l i -> + #bytes:Type0 -> {|bytes_like bytes|} -> #token_t:Type0 -> + l:nat -> i:tree_index l -> tokens:list (option token_t){List.Tot.length tokens == pow2 l} -> li:leaf_index l i -> Lemma - (leaf_at (tokens_from_list asp l i tokens) li == List.Tot.index tokens (li-i)) -let rec leaf_at_token_from_list #bytes #bl asp l i tokens li = + (leaf_at (tokens_from_list #bytes l i tokens) li == List.Tot.index tokens (li-i)) +let rec leaf_at_token_from_list #bytes #bl #token_t l i tokens li = if l = 0 then () else ( let tokens_left, tokens_right = List.Tot.splitAt (pow2 (l-1)) tokens in List.Pure.lemma_splitAt tokens tokens_left tokens_right (pow2 (l-1)); index_append tokens_left tokens_right (li-i); if is_left_leaf li then - leaf_at_token_from_list asp (l-1) (left_index i) tokens_left li + leaf_at_token_from_list #bytes (l-1) (left_index i) tokens_left li else - leaf_at_token_from_list asp (l-1) (right_index i) tokens_right li + leaf_at_token_from_list #bytes (l-1) (right_index i) tokens_right li ) #pop-options -val finalize_welcome: +val finalize_welcome_valid: #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #l:nat -> #group_id:mls_bytes bytes -> #t:treesync bytes tkt l 0 -> - pend:pending_welcome group_id t -> tokens:tokens_for_welcome asp pend -> - treesync_state bytes tkt asp group_id -let finalize_welcome #bytes #cb #tkt #asp #l #group_id #t pend tokens = - pend.can_welcome_proof; - let tokens_tree = tokens_from_list asp l 0 tokens in + pend:pending_welcome group_id t -> tokens:list (option asp.token_t){List.Tot.length tokens == pow2 l} -> + Lemma + (requires + forall li. match List.Tot.index pend.as_inputs li, List.Tot.index tokens li with + | Some as_inp, Some token -> asp.credential_ok as_inp token + | None, None -> True + | _, _ -> False + ) + (ensures treesync_state_valid asp (finalize_welcome pend tokens)) +let finalize_welcome_valid #bytes #cb #tkt #asp #l #group_id #t pend tokens = + let tokens_tree = tokens_from_list l 0 tokens in intro_all_credentials_ok t tokens_tree (fun li -> pend.as_inputs_proof; - leaf_at_token_from_list asp l 0 tokens li - ); - ({ - levels = l; - tree = t; - tokens = tokens_tree; - }) + leaf_at_token_from_list #bytes l 0 tokens li + ) (*** Add ***) let pending_add_proof - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#asp:as_parameters bytes) (#group_id:mls_bytes bytes) - (st:treesync_state bytes tkt asp group_id) (ln:leaf_node_nt bytes tkt) = + (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#token_t:Type0) (#group_id:mls_bytes bytes) + (st:treesync_state bytes tkt token_t group_id) (ln:leaf_node_nt bytes tkt) = squash ( ln.data.source == LNS_key_package /\ ( //TODO: check key package signature // TODO this match is a bit useless: @@ -244,24 +249,18 @@ let pending_add_proof ) type pending_add - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#asp:as_parameters bytes) (#group_id:mls_bytes bytes) - (st:treesync_state bytes tkt asp group_id) (ln:leaf_node_nt bytes tkt) = + (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#token_t:Type0) (#group_id:mls_bytes bytes) + (st:treesync_state bytes tkt token_t group_id) (ln:leaf_node_nt bytes tkt) = { can_add_proof: pending_add_proof st ln; as_input: as_input_for ln; } -type token_for_add - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#asp:as_parameters bytes) (#group_id:mls_bytes bytes) - (#st:treesync_state bytes tkt asp group_id) (#ln:leaf_node_nt bytes tkt) - (pend:pending_add st ln) = - as_token_for asp pend.as_input - val prepare_add: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - st:treesync_state bytes tkt asp group_id -> ln:leaf_node_nt bytes tkt -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + st:treesync_state bytes tkt token_t group_id -> ln:leaf_node_nt bytes tkt -> result (pending_add st ln) -let prepare_add #bytes #cb #tkt #asp #group_id st ln = +let prepare_add #bytes #cb #tkt #token_t #group_id st ln = if not (ln.data.source = LNS_key_package) then error "prepare_add: source is not key_package" else ( @@ -290,16 +289,15 @@ let prepare_add #bytes #cb #tkt #asp #group_id st ln = ) val finalize_add: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - #st:treesync_state bytes tkt asp group_id -> #ln:leaf_node_nt bytes tkt -> - pend:pending_add st ln -> token:token_for_add pend -> - result (treesync_state bytes tkt asp group_id & nat) -let finalize_add #bytes #cb #tkt #asp #group_id #st #ln pend token = + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + #st:treesync_state bytes tkt token_t group_id -> #ln:leaf_node_nt bytes tkt -> + pend:pending_add st ln -> token:token_t -> + result (treesync_state bytes tkt token_t group_id & nat) +let finalize_add #bytes #cb #tkt #token_t #group_id #st #ln pend token = pend.can_add_proof; match find_empty_leaf st.tree with | Some li -> ( let? new_tree = tree_add st.tree li ln in - all_credentials_ok_tree_add st.tree st.tokens li ln token; return (state_update_tree st new_tree (as_add_update st.tokens li token), (li <: nat)) ) | None -> ( @@ -308,16 +306,49 @@ let finalize_add #bytes #cb #tkt #asp #group_id #st #ln pend token = let extended_tokens = as_extend st.tokens in let li = Some?.v (find_empty_leaf extended_tree) in let? new_tree = tree_add extended_tree li ln in - all_credentials_ok_tree_extend st.tree st.tokens; - all_credentials_ok_tree_add extended_tree extended_tokens li ln token; return (state_update_tree st new_tree (as_add_update extended_tokens li token), (li <: nat)) ) +#push-options "--ifuel 1" +val finalize_add_valid: + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> + #st:treesync_state bytes tkt asp.token_t group_id -> #ln:leaf_node_nt bytes tkt -> + pend:pending_add st ln -> token:asp.token_t -> + Lemma + (requires + asp.credential_ok pend.as_input token /\ + treesync_state_valid asp st + ) + (ensures ( + match finalize_add pend token with + | Success (res, _) -> treesync_state_valid asp res + | _ -> True + )) +let finalize_add_valid #bytes #cb #tkt #asp #group_id #st #ln pend token = + pend.can_add_proof; + match finalize_add pend token with + | Success _ -> ( + match find_empty_leaf st.tree with + | Some li -> ( + all_credentials_ok_tree_add st.tree st.tokens li ln token + ) + | None -> ( + find_empty_leaf_tree_extend st.tree; + let extended_tree = tree_extend st.tree in + let extended_tokens = as_extend st.tokens in + let li = Some?.v (find_empty_leaf extended_tree) in + all_credentials_ok_tree_extend st.tree st.tokens; + all_credentials_ok_tree_add extended_tree extended_tokens li ln token + ) + ) + | _ -> () +#pop-options + (*** Update ***) let pending_update_proof - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#asp:as_parameters bytes) (#group_id:mls_bytes bytes) - (st:treesync_state bytes tkt asp group_id) (ln:leaf_node_nt bytes tkt) (li:treesync_index st) = + (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#token_t:Type0) (#group_id:mls_bytes bytes) + (st:treesync_state bytes tkt token_t group_id) (ln:leaf_node_nt bytes tkt) (li:treesync_index st) = squash ( ln.data.source == LNS_update /\ leaf_is_valid ln group_id li /\ @@ -325,25 +356,19 @@ let pending_update_proof ) type pending_update - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#asp:as_parameters bytes) (#group_id:mls_bytes bytes) - (st:treesync_state bytes tkt asp group_id) (ln:leaf_node_nt bytes tkt) (li:treesync_index st) = + (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#token_t:Type0) (#group_id:mls_bytes bytes) + (st:treesync_state bytes tkt token_t group_id) (ln:leaf_node_nt bytes tkt) (li:treesync_index st) = { can_update_proof: pending_update_proof st ln li; as_input_before: (can_update_proof; as_input_for (state_leaf_at st li)); as_input: as_input_for ln; } -type token_for_update - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#asp:as_parameters bytes) (#group_id:mls_bytes bytes) - (#st:treesync_state bytes tkt asp group_id) (#ln:leaf_node_nt bytes tkt) (#li:treesync_index st) - (pend:pending_update st ln li) = - token:as_token_for asp pend.as_input{asp.valid_successor pend.as_input_before pend.as_input} - val prepare_update: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - st:treesync_state bytes tkt asp group_id -> ln:leaf_node_nt bytes tkt -> li:treesync_index st -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + st:treesync_state bytes tkt token_t group_id -> ln:leaf_node_nt bytes tkt -> li:treesync_index st -> result (pending_update st ln li) -let prepare_update #bytes #cb #tkt #asp #group_id st ln li = +let prepare_update #bytes #cb #tkt #token_t #group_id st ln li = if not (ln.data.source = LNS_update) then error "prepare_update: leaf node has invalid source" else if not (leaf_is_valid ln group_id li) then @@ -359,36 +384,48 @@ let prepare_update #bytes #cb #tkt #asp #group_id st ln li = ) val finalize_update: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - #st:treesync_state bytes tkt asp group_id -> #ln:leaf_node_nt bytes tkt -> #li:treesync_index st -> - pend:pending_update st ln li -> token:token_for_update pend -> - treesync_state bytes tkt asp group_id -let finalize_update #bytes #cb #tkt #asp #group_id #st #ln #li pend token = + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + #st:treesync_state bytes tkt token_t group_id -> #ln:leaf_node_nt bytes tkt -> #li:treesync_index st -> + pend:pending_update st ln li -> token:token_t -> + treesync_state bytes tkt token_t group_id +let finalize_update #bytes #cb #tkt #token_t #group_id #st #ln #li pend token = pend.can_update_proof; - all_credentials_ok_tree_update st.tree st.tokens li ln token; (state_update_tree st (tree_update st.tree li ln) (as_add_update st.tokens li token)) +val finalize_update_valid: + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> + #st:treesync_state bytes tkt asp.token_t group_id -> #ln:leaf_node_nt bytes tkt -> #li:treesync_index st -> + pend:pending_update st ln li -> token:asp.token_t -> + Lemma + (requires + asp.credential_ok pend.as_input token /\ + treesync_state_valid asp st + ) + (ensures treesync_state_valid asp (finalize_update pend token)) +let finalize_update_valid #bytes #cb #tkt #asp #group_id #st #ln #li pend token = + all_credentials_ok_tree_update st.tree st.tokens li ln token + (*** Remove ***) let pending_remove_proof - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#asp:as_parameters bytes) (#group_id:mls_bytes bytes) - (st:treesync_state bytes tkt asp group_id) (li:treesync_index st) = + (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#token_t:Type0) (#group_id:mls_bytes bytes) + (st:treesync_state bytes tkt token_t group_id) (li:treesync_index st) = squash ( Some? (leaf_at st.tree li) ) type pending_remove - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#asp:as_parameters bytes) (#group_id:mls_bytes bytes) - (st:treesync_state bytes tkt asp group_id) (li:treesync_index st) = + (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#token_t:Type0) (#group_id:mls_bytes bytes) + (st:treesync_state bytes tkt token_t group_id) (li:treesync_index st) = { can_remove_proof: pending_remove_proof st li; } val prepare_remove: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - st:treesync_state bytes tkt asp group_id -> li:treesync_index st -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + st:treesync_state bytes tkt token_t group_id -> li:treesync_index st -> result (pending_remove st li) -let prepare_remove #bytes #cb #tkt #asp #group_id st li = +let prepare_remove #bytes #cb #tkt #token_t #group_id st li = if not (Some? (leaf_at st.tree li)) then error "prepare_remove: removed leaf is already blank" else ( @@ -399,13 +436,12 @@ let prepare_remove #bytes #cb #tkt #asp #group_id st li = #push-options "--fuel 0 --ifuel 1" val fully_truncate_state: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - st:treesync_state bytes tkt asp group_id -> - Tot (treesync_state bytes tkt asp group_id) + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + st:treesync_state bytes tkt token_t group_id -> + Tot (treesync_state bytes tkt token_t group_id) (decreases st.levels) -let rec fully_truncate_state #bytes #cb #tkt #asp #group_id st = +let rec fully_truncate_state #bytes #cb #tkt #token_t #group_id st = if 1 <= st.levels && is_tree_empty (TNode?.right st.tree) then ( - all_credentials_ok_tree_truncate st.tree st.tokens; fully_truncate_state { levels = st.levels-1; tree = tree_truncate st.tree; @@ -417,21 +453,52 @@ let rec fully_truncate_state #bytes #cb #tkt #asp #group_id st = #pop-options val finalize_remove: + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + #st:treesync_state bytes tkt token_t group_id -> #li:treesync_index st -> + pend:pending_remove st li -> + treesync_state bytes tkt token_t group_id +let finalize_remove #bytes #cb #tkt #token_t #group_id #st #li pend = + let blanked_tree = tree_remove st.tree li in + let blanked_tokens = as_remove st.tokens li in + fully_truncate_state (state_update_tree st blanked_tree blanked_tokens) + +#push-options "--fuel 1 --ifuel 1" +val fully_truncate_state_valid: + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> + st:treesync_state bytes tkt asp.token_t group_id -> + Lemma + (requires treesync_state_valid asp st) + (ensures treesync_state_valid asp (fully_truncate_state st)) + (decreases st.levels) +let rec fully_truncate_state_valid #bytes #cb #tkt #asp #group_id st = + if 1 <= st.levels && is_tree_empty (TNode?.right st.tree) then ( + all_credentials_ok_tree_truncate st.tree st.tokens; + fully_truncate_state_valid { + levels = st.levels-1; + tree = tree_truncate st.tree; + tokens = as_truncate st.tokens; + } + ) else () +#pop-options + +val finalize_remove_valid: #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - #st:treesync_state bytes tkt asp group_id -> #li:treesync_index st -> + #st:treesync_state bytes tkt asp.token_t group_id -> #li:treesync_index st -> pend:pending_remove st li -> - treesync_state bytes tkt asp group_id -let finalize_remove #bytes #cb #tkt #asp #group_id #st #li pend = + Lemma + (requires treesync_state_valid asp st) + (ensures treesync_state_valid asp (finalize_remove pend)) +let finalize_remove_valid #bytes #cb #tkt #asp #group_id #st #li pend = let blanked_tree = tree_remove st.tree li in let blanked_tokens = as_remove st.tokens li in all_credentials_ok_tree_remove st.tree st.tokens li; - fully_truncate_state (state_update_tree st blanked_tree blanked_tokens) + fully_truncate_state_valid (state_update_tree st blanked_tree blanked_tokens) (*** Commit ***) let pending_commit_proof - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#asp:as_parameters bytes) (#group_id:mls_bytes bytes) - (st:treesync_state bytes tkt asp group_id) (#li:treesync_index st) (p:pathsync bytes tkt st.levels 0 li) = + (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#token_t:Type0) (#group_id:mls_bytes bytes) + (st:treesync_state bytes tkt token_t group_id) (#li:treesync_index st) (p:pathsync bytes tkt st.levels 0 li) = squash ( path_is_valid group_id st.tree p /\ Some? (leaf_at st.tree li) @@ -439,8 +506,8 @@ let pending_commit_proof #push-options "--fuel 0 --ifuel 1 --z3rlimit 25" type pending_commit - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#asp:as_parameters bytes) (#group_id:mls_bytes bytes) - (st:treesync_state bytes tkt asp group_id) (#li:treesync_index st) (p:pathsync bytes tkt st.levels 0 li) = + (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#token_t:Type0) (#group_id:mls_bytes bytes) + (st:treesync_state bytes tkt token_t group_id) (#li:treesync_index st) (p:pathsync bytes tkt st.levels 0 li) = { can_commit_proof: pending_commit_proof st p; as_input_before: (can_commit_proof; as_input_for (state_leaf_at st li)); @@ -448,17 +515,11 @@ type pending_commit } #pop-options -type token_for_commit - (#bytes:Type0) {|crypto_bytes bytes|} (#tkt:treekem_types bytes) (#asp:as_parameters bytes) (#group_id:mls_bytes bytes) - (#st:treesync_state bytes tkt asp group_id) (#li:treesync_index st) (#p:pathsync bytes tkt st.levels 0 li) - (pend:pending_commit st p) = - token:as_token_for asp pend.as_input{asp.valid_successor pend.as_input_before pend.as_input} - val prepare_commit: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - st:treesync_state bytes tkt asp group_id -> #li:treesync_index st -> p:pathsync bytes tkt st.levels 0 li -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + st:treesync_state bytes tkt token_t group_id -> #li:treesync_index st -> p:pathsync bytes tkt st.levels 0 li -> result (pending_commit st p) -let prepare_commit #bytes #cb #tkt #asp #group_id st #li p = +let prepare_commit #bytes #cb #tkt #token_t #group_id st #li p = if not (path_is_valid group_id st.tree p) then error "prepare_commit: invalid path" else if not (Some? (leaf_at st.tree li)) then @@ -473,56 +534,82 @@ let prepare_commit #bytes #cb #tkt #asp #group_id st #li p = #push-options "--fuel 0 --ifuel 1" val finalize_commit: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - #st:treesync_state bytes tkt asp group_id -> #li:treesync_index st -> #p:pathsync bytes tkt st.levels 0 li -> - pend:pending_commit st p -> token:token_for_commit pend -> - result (treesync_state bytes tkt asp group_id) -let finalize_commit #bytes #cb #tkt #asp #group_id #st #li #p pend token = + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + #st:treesync_state bytes tkt token_t group_id -> #li:treesync_index st -> #p:pathsync bytes tkt st.levels 0 li -> + pend:pending_commit st p -> token:token_t -> + result (treesync_state bytes tkt token_t group_id) +let finalize_commit #bytes #cb #tkt #token_t #group_id #st #li #p pend token = pend.can_commit_proof; let? new_tree = apply_path st.tree p in - all_credentials_ok_apply_path st.tree st.tokens p token; return (state_update_tree st new_tree (as_add_update st.tokens li token)) #pop-options +#push-options "--fuel 0 --ifuel 1" +val finalize_commit_valid: + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> + #st:treesync_state bytes tkt asp.token_t group_id -> #li:treesync_index st -> #p:pathsync bytes tkt st.levels 0 li -> + pend:pending_commit st p -> token:asp.token_t -> + Lemma + (requires + asp.credential_ok pend.as_input token /\ + treesync_state_valid asp st + ) + (ensures ( + match finalize_commit pend token with + | Success res -> treesync_state_valid asp res + | _ -> True + )) +let finalize_commit_valid #bytes #cb #tkt #asp #group_id #st #li #p pend token = + match finalize_commit pend token with + | Success _ -> + all_credentials_ok_apply_path st.tree st.tokens p token + | _ -> () +#pop-options + (*** Weaken ***) +#push-options "--fuel 1 --ifuel 1" val weaken_asp: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - asp_weak:as_parameters bytes{as_parameters_weaker asp asp_weak} -> treesync_state bytes tkt asp group_id -> - treesync_state bytes tkt asp_weak group_id -let weaken_asp #bytes #cb #tkt #asp #group_id asp_weak st = - { st with - tokens = all_credentials_ok_weaken asp_weak st.tree st.tokens; - } + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + asp_strong:as_parameters bytes -> asp_weak:as_parameters bytes -> st:treesync_state bytes tkt token_t group_id -> + Lemma + (requires + asp_strong.token_t == token_t /\ + as_parameters_weaker asp_strong asp_weak /\ + treesync_state_valid asp_strong st + ) + (ensures treesync_state_valid asp_weak st) +let weaken_asp #bytes #cb #tkt #token_t #group_id asp_strong asp_weak st = () +#pop-options (*** Authenticate external path ***) #push-options "--fuel 0 --ifuel 1" val authenticate_external_path: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - st:treesync_state bytes tkt asp group_id -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + st:treesync_state bytes tkt token_t group_id -> #li:treesync_index st -> p:external_pathsync bytes tkt st.levels 0 li{(get_path_leaf p).source == LNS_update} -> sign_key:bytes -> sign_nonce bytes -> result (pathsync bytes tkt st.levels 0 li) -let authenticate_external_path #bytes #cb #tkt #asp #group_id st #li p sign_private_key sign_nonce = +let authenticate_external_path #bytes #cb #tkt #token_t #group_id st #li p sign_private_key sign_nonce = external_path_to_path st.tree p group_id sign_private_key sign_nonce #pop-options (*** Compute tree hashes ***) val compute_tree_hash: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - treesync_state bytes tkt asp group_id -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + treesync_state bytes tkt token_t group_id -> result bytes -let compute_tree_hash #bytes #cb #tkt #asp #group_id st = +let compute_tree_hash #bytes #cb #tkt #token_t #group_id st = tree_hash st.tree val compute_provisional_tree_hash: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - st:treesync_state bytes tkt asp group_id -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + st:treesync_state bytes tkt token_t group_id -> #li:treesync_index st -> pathsync bytes tkt st.levels 0 li -> result bytes -let compute_provisional_tree_hash #bytes #cb #tkt #asp #group_id st #li p = +let compute_provisional_tree_hash #bytes #cb #tkt #token_t #group_id st #li p = let? provisional_tree = MLS.TreeSync.Operations.apply_path st.tree p in tree_hash provisional_tree diff --git a/fstar/treesync/code/MLS.TreeSync.Invariants.AuthService.fst b/fstar/treesync/code/MLS.TreeSync.Invariants.AuthService.fst index 29443f0..e871adf 100644 --- a/fstar/treesync/code/MLS.TreeSync.Invariants.AuthService.fst +++ b/fstar/treesync/code/MLS.TreeSync.Invariants.AuthService.fst @@ -42,35 +42,35 @@ noeq type as_parameters (bytes:Type0) {|bytes_like bytes|} = { let as_tokens (bytes:Type0) {|bytes_like bytes|} (token_t:Type0) = tree (option token_t) unit val as_add_update: - #bytes:Type0 -> {|bytes_like bytes|} -> #asp:as_parameters bytes -> + #bytes:Type0 -> {|bytes_like bytes|} -> #token_t:Type0 -> #l:nat -> #i:tree_index l -> - as_tokens bytes asp.token_t l i -> leaf_index l i -> asp.token_t -> - as_tokens bytes asp.token_t l i + as_tokens bytes token_t l i -> leaf_index l i -> token_t -> + as_tokens bytes token_t l i let as_add_update #bytes #bl #asp #l #i t li token = tree_change_path t li (Some token) () val as_remove: - #bytes:Type0 -> {|bytes_like bytes|} -> #asp:as_parameters bytes -> + #bytes:Type0 -> {|bytes_like bytes|} -> #token_t:Type0 -> #l:nat -> #i:tree_index l -> - as_tokens bytes asp.token_t l i -> leaf_index l i -> - as_tokens bytes asp.token_t l i + as_tokens bytes token_t l i -> leaf_index l i -> + as_tokens bytes token_t l i let as_remove #bytes #bl #asp #l #i t li = tree_change_path t li None () val as_truncate: - #bytes:Type0 -> {|bytes_like bytes|} -> #asp:as_parameters bytes -> + #bytes:Type0 -> {|bytes_like bytes|} -> #token_t:Type0 -> #l:pos -> - as_tokens bytes asp.token_t l 0 -> - as_tokens bytes asp.token_t (l-1) 0 + as_tokens bytes token_t l 0 -> + as_tokens bytes token_t (l-1) 0 let as_truncate #bytes #bl #asp #l t = let TNode _ left _ = t in left val as_extend: - #bytes:Type0 -> {|bytes_like bytes|} -> #asp:as_parameters bytes -> + #bytes:Type0 -> {|bytes_like bytes|} -> #token_t:Type0 -> #l:nat -> - as_tokens bytes asp.token_t l 0 -> - as_tokens bytes asp.token_t (l+1) 0 + as_tokens bytes token_t l 0 -> + as_tokens bytes token_t (l+1) 0 let as_extend #bytes #bl #asp #l t = TNode () t (mk_blank_tree_general _ _ None ()) diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst index 5c8a4cf..e461ec2 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst @@ -1,62 +1,56 @@ module MLS.TreeSync.Symbolic.API.GroupManager open Comparse +open DY.Core +open DY.Lib open MLS.NetworkTypes -open ComparseGlue -open GlobalRuntimeLib -open LabeledRuntimeAPI open MLS.Symbolic -open MLS.Symbolic.MapSession (*** Group manager types & invariants ***) -type group_manager_value (bytes:Type0) {|bytes_like bytes|} = { +[@@ with_bytes dy_bytes] +type group_manager_key = { + group_id: mls_bytes dy_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] +type group_manager_value = { [@@@ with_parser #bytes ps_nat] si_public: nat; [@@@ with_parser #bytes ps_nat] si_private: nat; } -// When upgrading F* from commit 7ae4850a7e24f011a572ab4097fe1045babab48c to commit eb911fc41d5ba730c15f2ac296ffc5ebf7b46560, -// We get a failure in the `gen_parser` tactic: -// Goal: (bytes: Type0), (_: Comparse.Bytes.Typeclass.bytes_like bytes), (x: Prims.nat) |- _ : Prims.squash (forall (y: Prims.nat). (| x, y |) == (| x, y |)) -// Comparse.Tactic.GenerateParser.fst(293,8-293,85): (Error 228) user tactic failed: `apply_lemma: Cannot instantiate lemma FStar.Tactics.Logic.fa_intro_lem (with postcondition: Prims.squash (forall (x: Prims.nat). (| (*?u383*) _, (*?u379*) _ |) == (*?u371*) _)) to match goal (Prims.squash (forall (y: Prims.nat). (| x, y |) == (| x, y |)))` (see also FStar.Tactics.Logic.fst(50,4-50,31)) -// It does not happen in interactive mode, only when compiling using `make`. -// Very difficult to minimize, modifying functions *after* the tactic call would make the error dissappear. -// I noticed that adding a dummy function before is fixing the problem. -// Another option would have been to spend hours minimizing, filing an issue in F* and hope it would be fixed, but I don't have that time right now. -// This is why there is this horrible hack. -private let __do_not_remove_me__ (bytes:Type0) = () - %splice [ps_group_manager_value] (gen_parser (`group_manager_value)) %splice [ps_group_manager_value_is_well_formed] (gen_is_well_formed_lemma (`group_manager_value)) -val group_manager_types: map_types dy_bytes -let group_manager_types = { - key = mls_bytes dy_bytes; - ps_key = ps_mls_bytes; - value = group_manager_value dy_bytes; - ps_value = ps_group_manager_value; +instance group_manager_types: map_types group_manager_key group_manager_value = { + tag = "MLS.TreeSync.GroupManager"; + ps_key_t = ps_group_manager_key; + ps_value_t = ps_group_manager_value; } -val group_manager_pred: map_predicate group_manager_types -let group_manager_pred = { - pred = (fun gu time (group_id:group_manager_types.key) value -> - is_publishable gu time group_id +val group_manager_pred: {|crypto_invariants|} -> map_predicate group_manager_key group_manager_value #_ +let group_manager_pred #ci = { + pred = (fun tr prin state_id key value -> + is_publishable tr key.group_id ); - pred_later = (fun gu time0 time1 key value -> ()); - pred_is_msg = (fun gu time key value -> ()); + pred_later = (fun tr1 tr2 prin state_id key value -> ()); + pred_knowable = (fun tr prin state_id key value -> ()); } -val group_manager_label: string -let group_manager_label = "MLS.TreeSync.GroupManager" +val has_group_manager_invariant: protocol_invariants -> prop +let has_group_manager_invariant invs = + has_map_session_invariant invs group_manager_pred -val has_group_manager_invariant: preds -> prop -let has_group_manager_invariant pr = - has_map_session_invariant group_manager_types group_manager_pred group_manager_label pr +val group_manager_tag_and_invariant: {|crypto_invariants|} -> string & local_bytes_state_predicate +let group_manager_tag_and_invariant #ci = (group_manager_types.tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant group_manager_pred)) (*** Group manager API ***) -let initialize_group_manager = initialize_map group_manager_types group_manager_pred group_manager_label -let add_new_group_sessions = add_key_value group_manager_types group_manager_pred group_manager_label -let find_group_sessions = find_value group_manager_types group_manager_pred group_manager_label +let initialize_group_manager = initialize_map group_manager_key group_manager_value +let add_new_group_sessions = add_key_value #group_manager_key #group_manager_value +let find_group_sessions = find_value #group_manager_key #group_manager_value diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.IsWellFormedInvariant.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.IsWellFormedInvariant.fst index 9176639..05808d3 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.IsWellFormedInvariant.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.IsWellFormedInvariant.fst @@ -18,38 +18,38 @@ open MLS.Result #set-options "--fuel 1 --ifuel 1" val is_well_formed_finalize_create: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> #ln:leaf_node_nt bytes tkt -> pre:bytes_compatible_pre bytes -> - pend:pending_create group_id ln -> token:token_for_create asp pend -> + pend:pending_create group_id ln -> token:token_t -> Lemma (requires is_well_formed _ pre ln) (ensures ( let new_state = finalize_create pend token in is_well_formed _ pre (new_state.tree <: treesync _ _ _ _) )) -let is_well_formed_finalize_create #bytes #cb #tkt #asp #group_id #ln pre pend token = +let is_well_formed_finalize_create #bytes #cb #tkt #token_t #group_id #ln pre pend token = () val is_well_formed_finalize_welcome: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #l:nat -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #l:nat -> #group_id:mls_bytes bytes -> #t:treesync bytes tkt l 0 -> pre:bytes_compatible_pre bytes -> - pend:pending_welcome group_id t -> tokens:tokens_for_welcome asp pend -> + pend:pending_welcome group_id t -> tokens:list (option token_t){List.Tot.length tokens == pow2 l} -> Lemma (requires is_well_formed _ pre t) (ensures ( let new_state = finalize_welcome pend tokens in is_well_formed _ pre (new_state.tree <: treesync _ _ _ _) )) -let is_well_formed_finalize_welcome #bytes #cb #tkt #asp #l #group_id #t pre pend tokens = +let is_well_formed_finalize_welcome #bytes #cb #tkt #token_t #l #group_id #t pre pend tokens = () val is_well_formed_finalize_add: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - #st:treesync_state bytes tkt asp group_id -> #ln:leaf_node_nt bytes tkt -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + #st:treesync_state bytes tkt token_t group_id -> #ln:leaf_node_nt bytes tkt -> pre:bytes_compatible_pre bytes -> - pend:pending_add st ln -> token:token_for_add pend -> + pend:pending_add st ln -> token:token_t -> Lemma (requires is_well_formed _ pre (st.tree <: treesync _ _ _ _) /\ @@ -60,7 +60,7 @@ val is_well_formed_finalize_add: let Success (new_state, _) = finalize_add pend token in is_well_formed _ pre (new_state.tree <: treesync _ _ _ _) )) -let is_well_formed_finalize_add #bytes #cb #tkt #asp #group_id #st #ln pre pend token = +let is_well_formed_finalize_add #bytes #cb #tkt #token_t #group_id #st #ln pre pend token = match find_empty_leaf st.tree with | Some li -> ( is_well_formed_tree_add pre st.tree li ln @@ -74,22 +74,22 @@ let is_well_formed_finalize_add #bytes #cb #tkt #asp #group_id #st #ln pre pend ) val is_well_formed_finalize_update: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - #st:treesync_state bytes tkt asp group_id -> #ln:leaf_node_nt bytes tkt -> #li:treesync_index st -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + #st:treesync_state bytes tkt token_t group_id -> #ln:leaf_node_nt bytes tkt -> #li:treesync_index st -> pre:bytes_compatible_pre bytes -> - pend:pending_update st ln li -> token:token_for_update pend -> + pend:pending_update st ln li -> token:token_t -> Lemma (requires is_well_formed _ pre (st.tree <: treesync _ _ _ _) /\ is_well_formed _ pre ln) (ensures ( let new_state = finalize_update pend token in is_well_formed _ pre (new_state.tree <: treesync _ _ _ _) )) -let is_well_formed_finalize_update #bytes #cb #tkt #asp #group_id #st #ln #li pre pend token = +let is_well_formed_finalize_update #bytes #cb #tkt #token_t #group_id #st #ln #li pre pend token = is_well_formed_tree_update pre st.tree li ln val is_well_formed_fully_truncate_state: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - st:treesync_state bytes tkt asp group_id -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + st:treesync_state bytes tkt token_t group_id -> pre:bytes_compatible_pre bytes -> Lemma (requires is_well_formed _ pre (st.tree <: treesync _ _ _ _)) @@ -98,19 +98,18 @@ val is_well_formed_fully_truncate_state: is_well_formed _ pre (new_state.tree <: treesync _ _ _ _) )) (decreases st.levels) -let rec is_well_formed_fully_truncate_state #bytes #cb #tkt #asp #group_id st pre = +let rec is_well_formed_fully_truncate_state #bytes #cb #tkt #token_t #group_id st pre = if 1 <= st.levels && is_tree_empty (TNode?.right st.tree) then ( - MLS.TreeSync.Invariants.AuthService.Proofs.all_credentials_ok_tree_truncate st.tree st.tokens; is_well_formed_fully_truncate_state ({ levels = st.levels-1; tree = tree_truncate st.tree; tokens = as_truncate st.tokens; - } <: treesync_state bytes tkt asp group_id) pre + } <: treesync_state bytes tkt token_t group_id) pre ) else () val is_well_formed_finalize_remove: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - #st:treesync_state bytes tkt asp group_id -> #li:treesync_index st -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + #st:treesync_state bytes tkt token_t group_id -> #li:treesync_index st -> pre:bytes_compatible_pre bytes -> pend:pending_remove st li -> Lemma @@ -119,16 +118,15 @@ val is_well_formed_finalize_remove: let new_state = finalize_remove pend in is_well_formed _ pre (new_state.tree <: treesync _ _ _ _) )) -let is_well_formed_finalize_remove #bytes #cb #tkt #asp #group_id #st #li pre pend = - MLS.TreeSync.Invariants.AuthService.Proofs.all_credentials_ok_tree_remove st.tree st.tokens li; +let is_well_formed_finalize_remove #bytes #cb #tkt #token_t #group_id #st #li pre pend = is_well_formed_tree_remove pre st.tree li; is_well_formed_fully_truncate_state (state_update_tree st (tree_remove st.tree li) (as_remove st.tokens li)) pre val is_well_formed_finalize_commit: - #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #asp:as_parameters bytes -> #group_id:mls_bytes bytes -> - #st:treesync_state bytes tkt asp group_id -> #li:treesync_index st -> #p:pathsync bytes tkt st.levels 0 li -> + #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> #token_t:Type0 -> #group_id:mls_bytes bytes -> + #st:treesync_state bytes tkt token_t group_id -> #li:treesync_index st -> #p:pathsync bytes tkt st.levels 0 li -> pre:bytes_compatible_pre bytes{pre_is_hash_compatible pre} -> - pend:pending_commit st p -> token:token_for_commit pend -> + pend:pending_commit st p -> token:token_t -> Lemma (requires is_well_formed _ pre (st.tree <: treesync _ _ _ _) /\ @@ -139,5 +137,5 @@ val is_well_formed_finalize_commit: let Success new_state = finalize_commit pend token in is_well_formed _ pre (new_state.tree <: treesync _ _ _ _) )) -let is_well_formed_finalize_commit #bytes #cb #tkt #asp #group_id #st #li #p pre pend token = +let is_well_formed_finalize_commit #bytes #cb #tkt #token_t #group_id #st #li #p pre pend token = is_well_formed_apply_path pre st.tree p diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst index 9713f53..3292c85 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst @@ -1,16 +1,17 @@ module MLS.TreeSync.Symbolic.API.KeyPackageManager open Comparse +open DY.Core +open DY.Lib open MLS.TreeSync.NetworkTypes open MLS.Bootstrap.NetworkTypes -open LabeledRuntimeAPI open MLS.Symbolic -open MLS.Symbolic.MapSession open MLS.TreeSync.Symbolic.IsWellFormed (*** KeyPackage manager types & invariants ***) -type key_package_manager_value (bytes:Type0) {|bytes_like bytes|} = { +[@@ with_bytes dy_bytes] +type key_package_manager_value = { [@@@ with_parser #bytes ps_nat] si_private: nat; } @@ -18,32 +19,32 @@ type key_package_manager_value (bytes:Type0) {|bytes_like bytes|} = { %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)) -val key_package_manager_types: treekem_types dy_bytes -> map_types dy_bytes -let key_package_manager_types tkt = { - key = key_package_nt dy_bytes tkt; - ps_key = ps_key_package_nt tkt; - value = key_package_manager_value dy_bytes; - ps_value = ps_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 = { + 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: tkt:treekem_types dy_bytes -> map_predicate (key_package_manager_types tkt) -let key_package_manager_pred tkt = { - pred = (fun gu time (key_package:(key_package_manager_types tkt).key) value -> - is_well_formed _ (is_publishable gu time) key_package +val key_package_manager_pred: {|crypto_invariants|} -> tkt:treekem_types dy_bytes -> map_predicate (key_package_nt dy_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 + ); + pred_later = (fun tr1 tr2 prin state_id key_package value -> ()); + pred_knowable = (fun tr prin state_id key_package value -> + assert(is_well_formed _ (is_knowable_by (principal_state_label prin state_id) tr) key_package) ); - pred_later = (fun gu time0 time1 key_package value -> ()); - pred_is_msg = (fun gu time key_package value -> ()); } -val key_package_manager_label: string -let key_package_manager_label = "MLS.TreeSync.KeyPackageManager" +val has_key_package_manager_invariant: treekem_types dy_bytes -> protocol_invariants -> prop +let has_key_package_manager_invariant tkt invs = + has_map_session_invariant invs (key_package_manager_pred tkt) -val has_key_package_manager_invariant: treekem_types dy_bytes -> preds -> prop -let has_key_package_manager_invariant tkt pr = - has_map_session_invariant (key_package_manager_types tkt) (key_package_manager_pred tkt) key_package_manager_label pr +val key_package_manager_tag_and_invariant: {|crypto_invariants|} -> treekem_types dy_bytes -> 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_manager_types tkt) (key_package_manager_pred tkt) key_package_manager_label -let add_new_key_package_secret_session (tkt:treekem_types dy_bytes) = add_key_value (key_package_manager_types tkt) (key_package_manager_pred tkt) key_package_manager_label -let find_key_package_secret_session (tkt:treekem_types dy_bytes) = find_value (key_package_manager_types tkt) (key_package_manager_pred tkt) key_package_manager_label +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 diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst index 1fdceea..7813530 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst @@ -1,8 +1,8 @@ module MLS.TreeSync.Symbolic.API.Sessions open Comparse -open GlobalRuntimeLib -open LabeledRuntimeAPI +open DY.Core +open DY.Lib open MLS.Tree open MLS.NetworkTypes open MLS.TreeSync.NetworkTypes @@ -13,8 +13,6 @@ open MLS.TreeSync.Invariants.ValidLeaves open MLS.TreeSync.Invariants.AuthService open MLS.TreeSync.API.Types open MLS.Symbolic -open MLS.Symbolic.Session -open MLS.Symbolic.TypedSession open MLS.TreeSync.Symbolic.Parsers open MLS.TreeSync.Symbolic.IsWellFormed open MLS.TreeSync.Symbolic.LeafNodeSignature @@ -66,118 +64,147 @@ type bare_treesync_state (tkt:treekem_types dy_bytes) = 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) -val treesync_public_state_label: string -let treesync_public_state_label = "MLS.TreeSync.PublicState" - -// The `fun` is a workaround for FStarLang/FStar#2694 -val bare_treesync_public_state_pred: tkt:treekem_types dy_bytes -> bare_typed_session_pred (bare_treesync_state tkt) -let bare_treesync_public_state_pred tkt = fun gu p time si vi st -> - is_publishable gu time st.group_id /\ - is_well_formed _ (is_publishable gu time) st.tree /\ - 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_asp gu time).token_t st.levels 0) - -#push-options "--fuel 0 --ifuel 0" -val treesync_public_state_pred: treekem_types dy_bytes -> session_pred -let treesync_public_state_pred tkt = - typed_session_pred_to_session_pred ( - mk_typed_session_pred (bare_treesync_public_state_pred tkt) - (fun gu p time0 time1 si vi st -> - // Prove publishability of treesync in the future - wf_weaken_lemma _ (is_publishable gu time0) (is_publishable gu time1) st.tree - ) - (fun gu p time si vi st -> - let pre = is_msg gu (readers [psv_id p si vi]) time in - wf_weaken_lemma _ (is_publishable gu time) pre st.tree; - ps_dy_as_tokens_is_well_formed pre st.tokens - ) - ) +#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) +let treesync_public_state_pred #ci tkt = { + pred = (fun tr prin state_id st -> + is_publishable tr st.group_id /\ + is_well_formed _ (is_publishable tr) st.tree /\ + 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) + ); + pred_later = (fun tr1 tr2 prin state_id st -> + wf_weaken_lemma _ (is_publishable tr1) (is_publishable tr2) st.tree + ); + pred_knowable = (fun tr prin state_id st -> + let pre = is_knowable_by (principal_state_label prin state_id) tr in + wf_weaken_lemma _ (is_publishable tr) pre st.tree; + ps_dy_as_tokens_is_well_formed pre st.tokens + ); +} #pop-options -val has_treesync_public_state_invariant: treekem_types dy_bytes -> preds -> prop -let has_treesync_public_state_invariant tkt pr = - has_session_pred pr treesync_public_state_label (treesync_public_state_pred tkt) +instance local_state_bare_treesync_state (tkt:treekem_types dy_bytes): local_state (bare_treesync_state tkt) = + mk_local_state_instance "MLS.TreeSync.PublicState" + +val has_treesync_public_state_invariant: treekem_types dy_bytes -> protocol_invariants -> prop +let has_treesync_public_state_invariant tkt invs = + has_local_state_predicate invs (treesync_public_state_pred tkt) + +val treesync_public_state_tag_and_invariant: {|crypto_invariants|} -> treekem_types dy_bytes -> 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)) (*** LCrypto API for public state ***) -val treesync_state_to_session_bytes: +val treesync_state_to_bare_treesync_state: #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> time:timestamp -> si:nat -> vi:nat -> - group_id:mls_bytes dy_bytes -> st:treesync_state dy_bytes tkt (dy_asp pr.global_usage time) group_id -> - Pure dy_bytes - (requires - is_publishable pr.global_usage time group_id /\ - is_well_formed _ (is_publishable pr.global_usage time) (st.tree <: treesync _ _ _ _) /\ - has_treesync_public_state_invariant tkt pr - ) - (ensures fun res -> treesync_public_state_pred tkt pr.global_usage p time si vi res) -let treesync_state_to_session_bytes #tkt pr p time si vi group_id st = - let bare_st: bare_treesync_state tkt = { + #group_id:mls_bytes dy_bytes -> st:treesync_state dy_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; levels = st.levels; tree = st.tree; tokens = st.tokens; - } in - parse_serialize_inv_lemma #dy_bytes (bare_treesync_state tkt) bare_st; - serialize (bare_treesync_state tkt) bare_st + } val new_public_treesync_state: - #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> time:timestamp -> - group_id:mls_bytes dy_bytes -> st:treesync_state dy_bytes tkt (dy_asp pr.global_usage time) group_id -> - LCrypto nat pr - (requires fun t0 -> - time == trace_len t0 /\ - is_publishable pr.global_usage time group_id /\ - is_well_formed _ (is_publishable pr.global_usage time) (st.tree <: treesync _ _ _ _) /\ - has_treesync_public_state_invariant tkt pr + #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes -> + principal -> + st:treesync_state dy_bytes tkt dy_as_token group_id -> + crypto nat +let new_public_treesync_state #tkt #group_id prin st = + let* state_id = new_session_id prin in + set_state prin state_id (treesync_state_to_bare_treesync_state st);* + return state_id + +val new_public_treesync_state_proof: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes -> + prin:principal -> + st:treesync_state dy_bytes tkt dy_as_token group_id -> + tr:trace -> + Lemma + (requires + is_publishable tr group_id /\ + is_well_formed _ (is_publishable tr) (st.tree <: treesync _ _ _ _) /\ + treesync_state_valid (dy_asp tr) st /\ + trace_invariant tr /\ + has_treesync_public_state_invariant tkt invs ) - (ensures fun t0 si t1 -> trace_len t1 == trace_len t0 + 1) -let new_public_treesync_state #tkt pr p time group_id st = - let si = new_session_number pr p in - let bare_st_bytes = treesync_state_to_session_bytes pr p time si 0 group_id st in - new_session pr treesync_public_state_label (treesync_public_state_pred tkt) p si 0 bare_st_bytes; - si + (ensures ( + let (_, tr_out) = new_public_treesync_state prin st tr in + trace_invariant tr_out + )) +let new_public_treesync_state_proof #invs #tkt #group_id prin st tr = () val set_public_treesync_state: - #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> si:nat -> time:timestamp -> - group_id:mls_bytes dy_bytes -> st:treesync_state dy_bytes tkt (dy_asp pr.global_usage time) group_id -> - LCrypto unit pr - (requires fun t0 -> - time == trace_len t0 /\ - is_publishable pr.global_usage time group_id /\ - is_well_formed _ (is_publishable pr.global_usage time) (st.tree <: treesync _ _ _ _) /\ - has_treesync_public_state_invariant tkt pr + #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes -> + prin:principal -> state_id:nat -> + st:treesync_state dy_bytes tkt dy_as_token group_id -> + crypto 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: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes -> + prin:principal -> state_id:nat -> + st:treesync_state dy_bytes tkt dy_as_token group_id -> + tr:trace -> + Lemma + (requires + is_publishable tr group_id /\ + is_well_formed _ (is_publishable tr) (st.tree <: treesync _ _ _ _) /\ + treesync_state_valid (dy_asp tr) st /\ + trace_invariant tr /\ + has_treesync_public_state_invariant tkt invs ) - (ensures fun t0 r t1 -> trace_len t1 == trace_len t0 + 1) -let set_public_treesync_state #tkt pr p si time group_id st = - let bare_st_bytes = treesync_state_to_session_bytes pr p time si 0 group_id st in - update_session pr treesync_public_state_label (treesync_public_state_pred tkt) p si 0 bare_st_bytes + (ensures ( + let ((), tr_out) = set_public_treesync_state prin state_id st tr in + trace_invariant tr_out + )) +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 -> - pr:preds -> p:principal -> si:nat -> time:timestamp -> - LCrypto (group_id:mls_bytes dy_bytes & treesync_state dy_bytes tkt (dy_asp pr.global_usage time) group_id) pr - (requires fun t0 -> - time == trace_len t0 /\ - has_treesync_public_state_invariant tkt pr - ) - (ensures fun t0 (|group_id, st|) t1 -> - is_publishable pr.global_usage time group_id /\ - is_well_formed _ (is_publishable pr.global_usage time) (st.tree <: treesync _ _ _ _) /\ - t1 == t0 + prin:principal -> state_id:nat -> + crypto (option (dtuple2 (mls_bytes dy_bytes) (treesync_state dy_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 + if not (unmerged_leaves_ok bare_st.tree && parent_hash_invariant bare_st.tree && valid_leaves_invariant bare_st.group_id bare_st.tree) then + return None + else + return (Some (|bare_st.group_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)|)) + +val get_public_treesync_state_proof: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> + prin:principal -> state_id:nat -> + tr:trace -> + Lemma + (requires + trace_invariant tr /\ + has_treesync_public_state_invariant tkt invs ) -let get_public_treesync_state #tkt pr p si time = - let (_, st_bytes) = get_session pr treesync_public_state_label (treesync_public_state_pred tkt) p si in - let st = Some?.v (parse (bare_treesync_state tkt) st_bytes) in - (|st.group_id, ({ - levels = st.levels; - tree = st.tree; - tokens = st.tokens; - } <: treesync_state dy_bytes tkt (dy_asp pr.global_usage time) st.group_id)|) + (ensures ( + let (opt_result, tr_out) = get_public_treesync_state prin state_id tr in + tr_out == tr /\ ( + match opt_result with + | 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 _ _) + ) + ) + )) +let get_public_treesync_state_proof #invs #tkt prin state_id tr = () (*** Session predicate for private state ***) @@ -192,62 +219,95 @@ type treesync_private_state = treesync_private_state_ dy_bytes instance parseable_serializeable_treesync_private_state: parseable_serializeable dy_bytes treesync_private_state = mk_parseable_serializeable ps_treesync_private_state_ -val treesync_private_state_label: string -let treesync_private_state_label = "MLS.TreeSync.PrivateState" +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 + ); + pred_later = (fun tr1 tr2 prin state_id st -> ()); + pred_knowable = (fun tr prin state_id st -> ()); +} -val bare_treesync_private_state_pred: bare_typed_session_pred treesync_private_state -let bare_treesync_private_state_pred gu p time si vi st = - is_signature_key gu "MLS.LeafSignKey" (readers [p_id p]) time st.signature_key +instance local_state_treesync_private_state: local_state treesync_private_state = + mk_local_state_instance "MLS.TreeSync.PrivateState" -val treesync_private_state_pred: session_pred -let treesync_private_state_pred = - typed_session_pred_to_session_pred bare_treesync_private_state_pred +val has_treesync_private_state_invariant: protocol_invariants -> prop +let has_treesync_private_state_invariant invs = + has_local_state_predicate invs treesync_private_state_pred -val has_treesync_private_state_invariant: preds -> prop -let has_treesync_private_state_invariant pr = - has_session_pred pr treesync_private_state_label treesync_private_state_pred +val treesync_private_state_tag_and_invariant: {|crypto_invariants|} -> string & local_bytes_state_predicate +let treesync_private_state_tag_and_invariant #ci = (local_state_treesync_private_state.tag, local_state_predicate_to_local_bytes_state_predicate treesync_private_state_pred) (*** LCrypto API for private state ***) val new_private_treesync_state: - pr:preds -> p:principal -> - st:treesync_private_state -> - LCrypto nat pr - (requires fun t0 -> - is_signature_key pr.global_usage "MLS.LeafSignKey" (readers [p_id p]) (trace_len t0) st.signature_key /\ - has_treesync_private_state_invariant pr + principal -> treesync_private_state -> + crypto nat +let new_private_treesync_state prin st = + let* state_id = new_session_id prin in + set_state prin state_id st;* + return state_id + +val new_private_treesync_state_proof: + {|invs:protocol_invariants|} -> + prin:principal -> st:treesync_private_state -> + tr:trace -> + Lemma + (requires + is_signature_key "MLS.LeafSignKey" (principal_label prin) tr st.signature_key /\ + trace_invariant tr /\ + has_treesync_private_state_invariant invs ) - (ensures fun t0 si t1 -> trace_len t1 == trace_len t0 + 1) -let new_private_treesync_state pr p st = - let si = new_session_number pr p in - let st_bytes = serialize treesync_private_state st in - parse_serialize_inv_lemma #dy_bytes treesync_private_state st; - new_session pr treesync_private_state_label treesync_private_state_pred p si 0 st_bytes; - si + (ensures ( + let (_, tr_out) = new_private_treesync_state prin st tr in + trace_invariant tr_out + )) +let new_private_treesync_state_proof #invs prin st tr = () val set_private_treesync_state: - pr:preds -> p:principal -> si:nat -> - st:treesync_private_state -> - LCrypto unit pr - (requires fun t0 -> - is_signature_key pr.global_usage "MLS.LeafSignKey" (readers [p_id p]) (trace_len t0) st.signature_key /\ - has_treesync_private_state_invariant pr + principal -> nat -> treesync_private_state -> + crypto unit +let set_private_treesync_state prin state_id st = + set_state prin state_id st + +val set_private_treesync_state_proof: + {|invs:protocol_invariants|} -> + prin:principal -> state_id:nat -> st:treesync_private_state -> + tr:trace -> + Lemma + (requires + is_signature_key "MLS.LeafSignKey" (principal_label prin) tr st.signature_key /\ + trace_invariant tr /\ + has_treesync_private_state_invariant invs ) - (ensures fun t0 r t1 -> trace_len t1 == trace_len t0 + 1) -let set_private_treesync_state pr p si st = - let st_bytes = serialize treesync_private_state st in - parse_serialize_inv_lemma #dy_bytes treesync_private_state st; - new_session pr treesync_private_state_label treesync_private_state_pred p si 0 st_bytes + (ensures ( + let ((), tr_out) = set_private_treesync_state prin state_id st tr in + trace_invariant tr_out + )) +let set_private_treesync_state_proof #invs prin state_id st tr = () val get_private_treesync_state: - pr:preds -> p:principal -> si:nat -> - LCrypto treesync_private_state pr - (requires fun t0 -> has_treesync_private_state_invariant pr) - (ensures fun t0 st t1 -> - is_signature_key pr.global_usage "MLS.LeafSignKey" (readers [p_id p]) (trace_len t0) st.signature_key /\ - t1 == t0 + principal -> nat -> + crypto (option treesync_private_state) +let get_private_treesync_state prin state_id = + get_state prin state_id + +val get_private_treesync_state_proof: + {|invs:protocol_invariants|} -> + prin:principal -> state_id:nat -> + tr:trace -> + Lemma + (requires + trace_invariant tr /\ + has_treesync_private_state_invariant invs ) -let get_private_treesync_state pr p si = - let (_, st_bytes) = get_session pr treesync_private_state_label treesync_private_state_pred p si in - let st = Some?.v (parse treesync_private_state st_bytes) in - st + (ensures ( + let (opt_result, tr_out) = get_private_treesync_state prin state_id tr in + tr_out == tr /\ ( + match opt_result with + | None -> True + | Some st -> + is_signature_key "MLS.LeafSignKey" (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 83d39af..a6277d0 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst @@ -3,8 +3,6 @@ module MLS.TreeSync.Symbolic.API open Comparse open MLS.Result open MLS.Crypto -open GlobalRuntimeLib -open LabeledRuntimeAPI open MLS.Tree open MLS.NetworkTypes open MLS.Bootstrap.NetworkTypes @@ -23,427 +21,811 @@ open MLS.TreeSync.Symbolic.API.IsWellFormedInvariant open MLS.TreeSync.Symbolic.LeafNodeSignature open MLS.TreeSync.Symbolic.AuthServiceCache open MLS.TreeSync.Symbolic.IsWellFormed +open DY.Core +open DY.Lib -#set-options "--fuel 0 --ifuel 0" +#set-options "--fuel 0 --ifuel 0 --z3cliopt 'smt.qi.eager_threshold=100'" (*** Utility functions ***) -val guard: pr:preds -> b:bool -> LCrypto unit pr - (requires fun t0 -> True) - (ensures fun t0 _ t1 -> t1 == t0 /\ b) -let guard pr b = - if b then () - else error "guard failed" +val guard: b:bool -> crypto (option (squash b)) +let guard b = + if b then + return (Some ()) + else + return None #push-options "--ifuel 1" -val extract_result: #a:Type -> pr:preds -> x:MLS.Result.result a -> LCrypto a pr - (requires fun t0 -> True) - (ensures fun t0 res t1 -> t1 == t0 /\ x == Success res) -let extract_result #a pr x = +val extract_result: #a:Type -> x:MLS.Result.result a -> crypto (option a) +let extract_result #a x = match x with - | MLS.Result.Success y -> y - | MLS.Result.InternalError s -> error "extract_result: internal error '" ^ s ^ "'" - | MLS.Result.ProtocolError s -> error "extract_result: protocol error '" ^ s ^ "'" + | MLS.Result.Success y -> return (Some y) + | MLS.Result.InternalError s -> return None + | MLS.Result.ProtocolError s -> return None #pop-options -val has_treesync_invariants: treekem_types dy_bytes -> preds -> prop -let has_treesync_invariants tkt pr = - has_treesync_public_state_invariant tkt pr /\ - has_treesync_private_state_invariant pr /\ - has_group_manager_invariant pr /\ - has_key_package_manager_invariant tkt pr /\ - has_as_cache_invariant pr /\ - has_leaf_node_tbs_invariant tkt pr.global_usage +val has_treesync_invariants: treekem_types dy_bytes -> protocol_invariants -> prop +let has_treesync_invariants tkt invs = + has_treesync_public_state_invariant tkt invs /\ + has_treesync_private_state_invariant invs /\ + has_group_manager_invariant invs /\ + has_key_package_manager_invariant tkt invs /\ + has_as_cache_invariant invs /\ + has_leaf_node_tbs_invariant tkt invs.crypto_invs val get_token_for: - pr:preds -> p:principal -> as_session:nat -> + p:principal -> as_session:nat -> inp:as_input dy_bytes -> - LCrypto dy_as_token pr - (requires fun t0 -> has_as_cache_invariant pr) - (ensures fun t0 token t1 -> - (dy_asp pr.global_usage (trace_len t0)).credential_ok inp token /\ - t1 == t0 + crypto (option dy_as_token) +let get_token_for p as_session (verification_key, credential) = + let*? { who; usg; time; } = find_verified_credential p as_session ({ verification_key; credential; }) in + guard (usg = "MLS.LeafSignKey");*? + return (Some ({ who; time; } <: dy_as_token)) + +val get_token_for_proof: + {|invs:protocol_invariants|} -> + p:principal -> as_session:nat -> + inp:as_input dy_bytes -> + tr:trace -> + Lemma + (requires + trace_invariant tr /\ + has_as_cache_invariant invs ) -let get_token_for pr p as_session (verification_key, credential) = - let now = global_timestamp () in - let { who; usg; time; } = find_verified_credential pr p as_session ({ verification_key; credential; }) in - guard pr (usg = "MLS.LeafSignKey"); - { who; time; } + (ensures ( + let (opt_token, tr_out) = get_token_for p as_session inp tr in + tr_out == tr /\ ( + match opt_token with + | None -> True + | Some token -> ( + (dy_asp tr_out).credential_ok inp token + ) + ) + )) + [SMTPat (get_token_for p as_session inp tr); + SMTPat (has_as_cache_invariant invs)] +let get_token_for_proof #invs p as_session (verification_key, credential) tr = () #push-options "--fuel 1 --ifuel 1" val get_tokens_for: - pr:preds -> p:principal -> as_session:nat -> + p:principal -> as_session:nat -> inps:list (option (as_input dy_bytes)) -> - LCrypto (list (option dy_as_token)) pr - (requires fun t0 -> has_as_cache_invariant pr) - (ensures fun t0 tokens t1 -> - List.Tot.length tokens == List.Tot.length inps /\ - (forall i. - match (List.Tot.index inps i), (List.Tot.index tokens i) with - | None, None -> True - | Some inp, Some token -> (dy_asp pr.global_usage (trace_len t0)).credential_ok inp token - | _, _ -> False - ) /\ - t1 == t0 - ) -let rec get_tokens_for pr p as_session inps = - let now = global_timestamp () in + crypto (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 - | [] -> [] + | [] -> return (Some []) | inp_head::inps_tail -> - let token_head = + let*? token_head = match inp_head with - | Some inp -> Some (get_token_for pr p as_session inp) - | None -> None + | Some inp -> + let*? token = get_token_for p as_session inp in + return (Some (Some token)) + | None -> return (Some None) in - let tokens_tail = get_tokens_for pr p as_session inps_tail in + let*? tokens_tail = get_tokens_for p as_session inps_tail in let tokens = token_head::tokens_tail in - // An assert is needed to trigger the `forall` - assert(forall i. i <> 0 ==> List.Tot.index inps i == List.Tot.index inps_tail (i-1)); - tokens + return (Some (tokens <: l:list (option dy_as_token){List.Tot.length l == List.Tot.length inps})) +#pop-options + +#push-options "--fuel 1 --ifuel 1" +val get_tokens_for_proof: + {|invs:protocol_invariants|} -> + p:principal -> as_session:nat -> + inps:list (option (as_input dy_bytes)) -> + tr:trace -> + Lemma + (requires + trace_invariant tr /\ + has_as_cache_invariant invs + ) + (ensures ( + let (opt_tokens, tr_out) = get_tokens_for p as_session inps tr in + tr_out == tr /\ ( + match opt_tokens with + | None -> True + | Some tokens -> ( + List.Tot.length tokens == List.Tot.length inps /\ + (forall i. + match (List.Tot.index inps i), (List.Tot.index tokens i) with + | None, None -> True + | Some inp, Some token -> (dy_asp tr_out).credential_ok inp token + | _, _ -> False + ) + ) + ) + )) + [SMTPat (get_tokens_for p as_session inps tr); + SMTPat (has_as_cache_invariant invs)] +let rec get_tokens_for_proof #invs p as_session inps tr = + match inps with + | [] -> () + | inp_head::inps_tail -> + get_tokens_for_proof p as_session inps_tail tr; + assert(forall i. i <> 0 ==> List.Tot.index inps i == List.Tot.index inps_tail (i-1)) #pop-options (*** Process proposals ***) val create: #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> as_session:nat -> gmgr_session:nat -> + p:principal -> as_session:nat -> gmgr_session:nat -> group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> secret_session:nat -> - LCrypto unit pr - (requires fun t0 -> - is_publishable pr.global_usage (trace_len t0) group_id /\ - is_well_formed _ (is_publishable pr.global_usage (trace_len t0)) ln /\ - has_treesync_invariants tkt pr - ) - (ensures fun t0 () t1 -> trace_len t1 == trace_len t0 + 2) -let create #tkt pr p as_session gmgr_session group_id ln secret_session = - let now = global_timestamp () in - let create_pend = extract_result pr (prepare_create #dy_bytes #crypto_dy_bytes group_id ln) in - let token = get_token_for pr p as_session create_pend.as_input in - let token: as_token_for (dy_asp pr.global_usage now) create_pend.as_input = token in + crypto (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*? token = get_token_for p as_session (create_pend.as_input) in let st = finalize_create create_pend token in - is_well_formed_finalize_create (is_publishable pr.global_usage now) create_pend token; - let si_public = new_public_treesync_state pr p now _ st in + let* si_public = new_public_treesync_state p st in let group_sessions = { si_public; si_private = secret_session; } in - add_new_group_sessions pr p gmgr_session group_id group_sessions + add_new_group_sessions p gmgr_session { group_id } group_sessions;*? + return (Some ()) + +val create_proof: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> + p:principal -> as_session:nat -> gmgr_session:nat -> + group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> secret_session:nat -> + tr:trace -> + Lemma + (requires + is_publishable tr group_id /\ + is_well_formed _ (is_publishable tr) ln /\ + trace_invariant tr /\ + has_treesync_invariants tkt invs + ) + (ensures ( + let (_, tr_out) = create p as_session gmgr_session group_id ln secret_session tr in + 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 + match opt_create_pend with + | None -> () + | Some create_pend -> ( + let (opt_token, tr) = get_token_for p as_session create_pend.as_input tr in + match opt_token with + | None -> () + | Some token -> ( + is_well_formed_finalize_create (is_publishable tr) create_pend token; + finalize_create_valid #_ #_ #_ #(dy_asp tr) create_pend token + ) + ) val welcome: #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> as_session:nat -> gmgr_session:nat -> kpmgr_session:nat -> + p:principal -> as_session:nat -> gmgr_session:nat -> kpmgr_session:nat -> my_key_package:key_package_nt dy_bytes tkt -> group_id:mls_bytes dy_bytes -> l:nat -> t:treesync dy_bytes tkt l 0 -> - LCrypto unit pr - (requires fun t0 -> - is_publishable pr.global_usage (trace_len t0) group_id /\ - is_well_formed _ (is_publishable pr.global_usage (trace_len t0)) t /\ - has_treesync_invariants tkt pr - ) - (ensures fun t0 () t1 -> trace_len t1 == trace_len t0 + 2) -let welcome #tkt pr p as_session gmgr_session kpmgr_session my_key_package group_id l t = - let now = global_timestamp () in - let welcome_pend = extract_result pr (prepare_welcome #dy_bytes #crypto_dy_bytes group_id t) in + crypto (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 welcome_pend.as_inputs_proof; - let tokens = get_tokens_for pr p as_session welcome_pend.as_inputs in - let tokens: tokens_for_welcome (dy_asp pr.global_usage now) welcome_pend = tokens in + let*? tokens = get_tokens_for p as_session welcome_pend.as_inputs in let st = finalize_welcome welcome_pend tokens in - is_well_formed_finalize_welcome (is_publishable pr.global_usage now) welcome_pend tokens; - let si_public = new_public_treesync_state pr p now _ st in - let si_private = (find_key_package_secret_session tkt pr p kpmgr_session my_key_package).si_private in + let* si_public = new_public_treesync_state p st in + let*? { si_private } = find_key_package_secret_session tkt p kpmgr_session my_key_package in let group_sessions = { si_public; si_private; } in - add_new_group_sessions pr p gmgr_session group_id group_sessions + add_new_group_sessions p gmgr_session { group_id } group_sessions + +val welcome_proof: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> + p:principal -> as_session:nat -> gmgr_session:nat -> kpmgr_session:nat -> + my_key_package:key_package_nt dy_bytes tkt -> + group_id:mls_bytes dy_bytes -> l:nat -> t:treesync dy_bytes tkt l 0 -> + tr:trace -> + Lemma + (requires + is_publishable tr group_id /\ + is_well_formed _ (is_publishable tr) t /\ + trace_invariant tr /\ + has_treesync_invariants tkt invs + ) + (ensures ( + let (_, tr_out) = welcome p as_session gmgr_session kpmgr_session my_key_package group_id l t tr in + 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 + match opt_welcome_pend with + | None -> () + | Some welcome_pend -> ( + welcome_pend.as_inputs_proof; + get_tokens_for_proof p as_session welcome_pend.as_inputs tr; + let (opt_tokens, tr) = get_tokens_for p as_session welcome_pend.as_inputs tr in + match opt_tokens with + | None -> () + | Some tokens -> ( + is_well_formed_finalize_welcome (is_publishable tr) welcome_pend tokens; + finalize_welcome_valid #_ #_ #_ #(dy_asp tr) welcome_pend tokens; + // not sure why F* needs the following lines + // similar to FStarLang/FStar#3093 ? + let st = finalize_welcome welcome_pend tokens in + let (si_public, tr) = new_public_treesync_state p st tr in + let (opt_si_private, tr) = find_key_package_secret_session tkt p kpmgr_session my_key_package tr in + match opt_si_private with + | None -> () + | Some { si_private } -> () + ) + ) val add: #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> as_session:nat -> gmgr_session:nat -> + p:principal -> as_session:nat -> gmgr_session:nat -> group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> - LCrypto nat pr - (requires fun t0 -> - is_well_formed _ (is_publishable pr.global_usage (trace_len t0)) ln /\ - has_treesync_invariants tkt pr + crypto (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 + let*? (|group_id, st|) = get_public_treesync_state #tkt p group_session.si_public in + let*? add_pend = extract_result (prepare_add st ln) in + let*? token = get_token_for p as_session add_pend.as_input in + let*? (new_st, new_leaf_index) = extract_result (finalize_add add_pend token) in + set_public_treesync_state p group_session.si_public new_st;* + return (Some new_leaf_index) + +val add_proof: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> + p:principal -> as_session:nat -> gmgr_session:nat -> + group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> + tr:trace -> + Lemma + (requires + is_well_formed _ (is_publishable tr) ln /\ + trace_invariant tr /\ + has_treesync_invariants tkt invs + ) + (ensures ( + let (_, tr_out) = add p as_session gmgr_session group_id ln tr in + trace_invariant tr_out + )) +let add_proof #invs #tkt p as_session gmgr_session group_id ln tr = + let (opt_group_session, tr) = find_group_sessions p gmgr_session { group_id } tr in + match opt_group_session with + | None -> () + | Some group_session -> ( + let (opt_st, tr) = get_public_treesync_state #tkt p group_session.si_public tr in + match opt_st with + | None -> () + | Some (|group_id, st|) -> ( + let (opt_add_pend, tr) = extract_result (prepare_add st ln) tr in + match opt_add_pend with + | None -> () + | Some add_pend -> ( + let (opt_token, tr) = get_token_for p as_session add_pend.as_input tr in + match opt_token with + | None -> () + | Some token -> ( + let (opt_new_st, tr) = extract_result (finalize_add add_pend token) tr in + match opt_new_st with + | None -> () + | Some (new_st, _) -> ( + is_well_formed_finalize_add (is_publishable tr) add_pend token; + finalize_add_valid #_ #_ #_ #(dy_asp tr) add_pend token + ) + ) + ) + ) ) - (ensures fun t0 _ t1 -> trace_len t1 == trace_len t0 + 1) -let add #tkt pr p as_session gmgr_session group_id ln = - let now = global_timestamp () in - let group_session = find_group_sessions pr p gmgr_session group_id in - let (|group_id, st|) = get_public_treesync_state #tkt pr p group_session.si_public now in - - let add_pend = extract_result pr (prepare_add st ln) in - let token = get_token_for pr p as_session add_pend.as_input in - let (new_st, new_leaf_index) = extract_result pr (finalize_add add_pend token) in - is_well_formed_finalize_add (is_publishable pr.global_usage now) add_pend token; - set_public_treesync_state pr p group_session.si_public now _ new_st; - new_leaf_index val update: #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> as_session:nat -> gmgr_session:nat -> + p:principal -> as_session:nat -> gmgr_session:nat -> group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> li:nat -> - LCrypto unit pr - (requires fun t0 -> - is_well_formed _ (is_publishable pr.global_usage (trace_len t0)) ln /\ - has_treesync_invariants tkt pr - ) - (ensures fun t0 () t1 -> trace_len t1 == trace_len t0 + 1) -let update #tkt pr p as_session gmgr_session group_id ln li = - let now = global_timestamp () in - let group_session = find_group_sessions pr p gmgr_session group_id in - let (|group_id, st|) = get_public_treesync_state #tkt pr p group_session.si_public now in - guard pr (li < pow2 st.levels); - let update_pend = extract_result pr (prepare_update st ln li) in - let token = get_token_for pr p as_session update_pend.as_input in + crypto (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 + let*? (|group_id, st|) = get_public_treesync_state #tkt p group_session.si_public in + guard (li < pow2 st.levels);*? + let*? update_pend = extract_result (prepare_update st ln li) in + let*? token = get_token_for p as_session update_pend.as_input in let new_st = finalize_update update_pend token in - is_well_formed_finalize_update (is_publishable pr.global_usage now) update_pend token; - set_public_treesync_state pr p group_session.si_public now _ new_st + set_public_treesync_state p group_session.si_public new_st;* + return (Some ()) + +val update_proof: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> + p:principal -> as_session:nat -> gmgr_session:nat -> + group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> li:nat -> + tr:trace -> + Lemma + (requires + is_well_formed _ (is_publishable tr) ln /\ + trace_invariant tr /\ + has_treesync_invariants tkt invs + ) + (ensures ( + let (_, tr_out) = update p as_session gmgr_session group_id ln li tr in + trace_invariant tr_out + )) +let update_proof #invs #tkt p as_session gmgr_session group_id ln li tr = + let (opt_group_session, tr) = find_group_sessions p gmgr_session { group_id } tr in + match opt_group_session with + | None -> () + | Some group_session -> ( + let (opt_st, tr) = get_public_treesync_state #tkt p group_session.si_public tr in + match opt_st with + | None -> () + | Some (|group_id, st|) -> ( + if not (li < pow2 st.levels) then () + else ( + let (opt_update_pend, tr) = extract_result (prepare_update st ln li) tr in + match opt_update_pend with + | None -> () + | Some update_pend -> ( + let (opt_token, tr) = get_token_for p as_session update_pend.as_input tr in + match opt_token with + | None -> () + | Some token -> ( + is_well_formed_finalize_update (is_publishable tr) update_pend token; + finalize_update_valid #_ #_ #_ #(dy_asp tr) update_pend token + ) + ) + ) + ) + ) val remove: #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> as_session:nat -> gmgr_session:nat -> + p:principal -> as_session:nat -> gmgr_session:nat -> group_id:mls_bytes dy_bytes -> li:nat -> - LCrypto unit pr - (requires fun t0 -> - has_treesync_invariants tkt pr - ) - (ensures fun t0 () t1 -> trace_len t1 == trace_len t0 + 1) -let remove #tkt pr p as_session gmgr_session group_id li = - let now = global_timestamp () in - let group_session = find_group_sessions pr p gmgr_session group_id in - let (|group_id, st|) = get_public_treesync_state #tkt pr p group_session.si_public now in - guard pr (li < pow2 st.levels); - let remove_pend = extract_result pr (prepare_remove st li) in + crypto (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 + let*? (|group_id, st|) = get_public_treesync_state #tkt p group_session.si_public in + guard (li < pow2 st.levels);*? + let*? remove_pend = extract_result (prepare_remove st li) in let new_st = finalize_remove remove_pend in - is_well_formed_finalize_remove (is_publishable pr.global_usage now) remove_pend; - set_public_treesync_state pr p group_session.si_public now _ new_st + set_public_treesync_state p group_session.si_public new_st;* + return (Some ()) + +val remove_proof: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> + p:principal -> as_session:nat -> gmgr_session:nat -> + group_id:mls_bytes dy_bytes -> li:nat -> + tr:trace -> + Lemma + (requires + trace_invariant tr /\ + has_treesync_invariants tkt invs + ) + (ensures ( + let (_, tr_out) = remove #tkt p as_session gmgr_session group_id li tr in + trace_invariant tr_out + )) +let remove_proof #invs #tkt p as_session gmgr_session group_id li tr = + let (opt_group_session, tr) = find_group_sessions p gmgr_session { group_id } tr in + match opt_group_session with + | None -> () + | Some group_session -> ( + let (opt_st, tr) = get_public_treesync_state #tkt p group_session.si_public tr in + match opt_st with + | None -> () + | Some (|group_id, st|) -> ( + if not (li < pow2 st.levels) then () + else ( + let (opt_remove_pend, tr) = extract_result (prepare_remove st li) tr in + match opt_remove_pend with + | None -> () + | Some remove_pend -> ( + is_well_formed_finalize_remove (is_publishable tr) remove_pend; + finalize_remove_valid #_ #_ #_ #(dy_asp tr) remove_pend + ) + ) + ) + ) -#push-options "--z3rlimit 25" val commit: #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 -> - pr:preds -> p:principal -> as_session:nat -> gmgr_session:nat -> + p:principal -> as_session:nat -> gmgr_session:nat -> + group_id:mls_bytes dy_bytes -> path:pathsync dy_bytes tkt l 0 li -> + crypto (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 + let*? (|group_id, st|) = get_public_treesync_state #tkt p group_session.si_public in + guard (l = st.levels);*? + let*? commit_pend = extract_result (prepare_commit st path) in + let*? token = get_token_for p as_session commit_pend.as_input in + let*? new_st = extract_result (finalize_commit commit_pend token) in + set_public_treesync_state p group_session.si_public new_st;* + return (Some ()) + +#push-options "--z3rlimit 50" +val commit_proof: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 -> + p:principal -> as_session:nat -> gmgr_session:nat -> group_id:mls_bytes dy_bytes -> path:pathsync dy_bytes tkt l 0 li -> - LCrypto unit pr - (requires fun t0 -> - is_well_formed _ (is_publishable pr.global_usage (trace_len t0)) path /\ - has_treesync_invariants tkt pr + tr:trace -> + Lemma + (requires + is_well_formed _ (is_publishable tr) path /\ + trace_invariant tr /\ + has_treesync_invariants tkt invs + ) + (ensures ( + let (_, tr_out) = commit p as_session gmgr_session group_id path tr in + trace_invariant tr_out + )) +#restart-solver +let commit_proof #invs #tkt #l #li p as_session gmgr_session group_id path tr = + let (opt_group_session, tr) = find_group_sessions p gmgr_session { group_id } tr in + match opt_group_session with + | None -> () + | Some group_session -> ( + let (opt_st, tr) = get_public_treesync_state #tkt p group_session.si_public tr in + match opt_st with + | None -> () + | Some (|group_id, st|) -> ( + if not (l = st.levels) then () + else ( + let (opt_commit_pend, tr) = extract_result (prepare_commit st path) tr in + match opt_commit_pend with + | None -> () + | Some commit_pend -> ( + let (opt_token, tr) = get_token_for p as_session commit_pend.as_input tr in + match opt_token with + | None -> () + | Some token -> ( + let (opt_new_st, tr) = extract_result (finalize_commit commit_pend token) tr in + assert((dy_asp tr).credential_ok commit_pend.as_input token); + match opt_new_st with + | None -> () + | Some new_st -> ( + FStar.Pure.BreakVC.break_vc (); + is_well_formed_finalize_commit (is_publishable tr) commit_pend token; + finalize_commit_valid #_ #_ #_ #(dy_asp tr) commit_pend token; + set_public_treesync_state_proof p group_session.si_public new_st tr; + let (_, tr) = set_public_treesync_state p group_session.si_public new_st tr in + () + ) + ) + ) + ) + ) ) - (ensures fun t0 () t1 -> trace_len t1 == trace_len t0 + 1) -let commit #tkt #l #li pr p as_session gmgr_session group_id path = - let now = global_timestamp () in - let group_session = find_group_sessions pr p gmgr_session group_id in - let (|group_id, st|) = get_public_treesync_state #tkt pr p group_session.si_public now in - guard pr (l = st.levels); - let commit_pend = extract_result pr (prepare_commit st path) in - let token = get_token_for pr p as_session commit_pend.as_input in - let new_st = extract_result pr (finalize_commit commit_pend token) in - is_well_formed_finalize_commit (is_publishable pr.global_usage now) commit_pend token; - set_public_treesync_state pr p group_session.si_public now _ new_st #pop-options (*** Create signature keypair ***) val create_signature_keypair: - pr:preds -> p:principal -> - LCrypto (nat & signature_public_key_nt dy_bytes) pr - (requires fun t0 -> - has_treesync_private_state_invariant pr - ) - (ensures fun t0 (private_si, verification_key) t1 -> - is_verification_key pr.global_usage "MLS.LeafSignKey" (readers [p_id p]) (trace_len t0) verification_key /\ - trace_len t1 == trace_len t0 + 2 - ) -let create_signature_keypair pr p = - let (|now, signature_key|) = rand_gen #pr (readers [p_id p]) (sig_usage "MLS.LeafSignKey") in - let verification_key = LabeledCryptoAPI.vk #pr.global_usage #now #(readers [p_id p]) signature_key in - guard pr (length (signature_key <: dy_bytes) < pow2 30); - guard pr (length (verification_key <: dy_bytes) < pow2 30); + p:principal -> + crypto (option (nat & 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 verification_key = vk signature_key in + guard (length (signature_key <: dy_bytes) < pow2 30);*? + guard (length (verification_key <: dy_bytes) < pow2 30);*? let private_state: treesync_private_state = {signature_key;} in - let private_si = new_private_treesync_state pr p private_state in - (private_si, verification_key) + let* private_si = new_private_treesync_state p private_state in + return (Some (private_si, (verification_key <: signature_public_key_nt dy_bytes))) + +val create_signature_keypair_proof: + {|invs:protocol_invariants|} -> + p:principal -> + tr:trace -> + Lemma + (requires + trace_invariant tr /\ + has_treesync_private_state_invariant invs + ) + (ensures ( + let (opt_res, tr_out) = create_signature_keypair p tr in + trace_invariant tr_out /\ ( + match opt_res with + | None -> True + | Some (private_si, verification_key) -> + is_verification_key "MLS.LeafSignKey" (principal_label p) tr_out verification_key + ) + )) +let create_signature_keypair_proof #invs p tr = () (*** Sign stuff ***) val external_path_has_event_later: #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 -> - prin:principal -> time0:timestamp -> time1:timestamp -> + 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 -> Lemma (requires - external_path_has_event prin time0 t p group_id /\ - time0 <$ time1 + external_path_has_event prin tr1 t p group_id /\ + tr1 <$ tr2 ) - (ensures external_path_has_event prin time1 t p group_id) -let external_path_has_event_later #tkt #l #li prin time0 time1 t p group_id = + (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 time0 group_id) (path_to_tree_list #dy_bytes #crypto_dy_bytes t auth_p); - for_allP_eq (tree_has_event prin time1 group_id) (path_to_tree_list #dy_bytes #crypto_dy_bytes t auth_p) + 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) #push-options "--z3rlimit 25" val authenticate_path: #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 -> - pr:preds -> p:principal -> gmgr_session:nat -> + p:principal -> gmgr_session:nat -> + 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} -> + crypto (option (pathsync dy_bytes tkt l 0 li)) +let authenticate_path #tkt #l p gmgr_session group_id tree path = + let* signature_nonce = mk_rand SigNonce (principal_label p) 32 in + let*? group_session = find_group_sessions p gmgr_session { group_id } in + let*? (|group_id', st|) = get_public_treesync_state #tkt p group_session.si_public in + let*? private_st = get_private_treesync_state p group_session.si_private in + 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 private_st.signature_key signature_nonce) in + return (Some auth_path) +#pop-options + +#push-options "--z3rlimit 25" +val authenticate_path_proof: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 -> + p:principal -> gmgr_session:nat -> group_id:mls_bytes dy_bytes -> tree:treesync dy_bytes tkt l 0 -> path:external_pathsync dy_bytes tkt l 0 li -> - LCrypto (pathsync dy_bytes tkt l 0 li) pr - (requires fun t0 -> - external_path_has_event p (trace_len t0) tree path group_id /\ - is_well_formed _ (is_publishable pr.global_usage (trace_len t0)) path /\ - has_treesync_invariants tkt pr + tr:trace -> + Lemma + (requires + external_path_has_event p tr tree path group_id /\ + is_well_formed _ (is_publishable tr) path /\ + trace_invariant tr /\ + has_treesync_invariants tkt invs ) - (ensures fun t0 auth_path t1 -> - is_well_formed _ (is_publishable pr.global_usage (trace_len t1)) auth_path /\ - trace_len t1 == trace_len t0 + 1 + (ensures ( + let (opt_auth_path, tr_out) = authenticate_path p gmgr_session group_id tree path tr in + trace_invariant tr_out /\ ( + match opt_auth_path with + | None -> True + | Some auth_path -> + is_well_formed _ (is_publishable tr_out) auth_path + ) + )) +let authenticate_path_proof #invs #tkt #l p gmgr_session group_id tree path tr = + let tr_in = tr in + let (signature_nonce, tr) = mk_rand SigNonce (principal_label p) 32 tr in + let (opt_group_session, tr) = find_group_sessions p gmgr_session { group_id } tr in + match opt_group_session with + | None -> () + | Some group_session -> ( + let (opt_st, tr) = get_public_treesync_state #tkt p group_session.si_public tr in + match opt_st with + | None -> () + | Some(|group_id', st|) -> ( + let (opt_private_st, tr) = get_private_treesync_state p group_session.si_private tr in + match opt_private_st with + | None -> () + | Some private_st -> ( + 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 ( + let (opt_auth_path, tr) = extract_result (external_path_to_path #dy_bytes #crypto_dy_bytes tree path group_id private_st.signature_key signature_nonce) tr in + match opt_auth_path with + | None -> () + | Some auth_path -> ( + let tr_out = tr in + wf_weaken_lemma _ (is_publishable tr_in) (is_publishable tr_out) path; + external_path_has_event_later p tr_in tr_out tree path group_id; + is_msg_external_path_to_path p public tr_out tree path group_id private_st.signature_key signature_nonce + ) + ) + ) + ) ) -let authenticate_path #tkt #l pr p gmgr_session group_id tree path = - let (|now0, signature_nonce|) = rand_gen #pr (readers [p_id p]) (sig_usage "???") in - let now1 = global_timestamp () in - let group_session = find_group_sessions pr p gmgr_session group_id in - let (|group_id', st|) = get_public_treesync_state #tkt pr p group_session.si_public now1 in - let private_st = get_private_treesync_state pr p group_session.si_private in - guard pr ( - (group_id = group_id') && - (l = st.levels) && - (tree = st.tree) && - length (signature_nonce <: dy_bytes) >= sign_sign_min_entropy_length #dy_bytes && - (path_is_filter_valid #dy_bytes #crypto_dy_bytes tree path) - ); - let auth_path = extract_result pr (external_path_to_path #dy_bytes #crypto_dy_bytes tree path group_id private_st.signature_key signature_nonce) in - wf_weaken_lemma _ (is_publishable pr.global_usage now0) (is_publishable pr.global_usage now1) path; - external_path_has_event_later p now0 now1 tree path group_id; - is_msg_external_path_to_path pr.global_usage p SecrecyLabels.public now1 tree path group_id private_st.signature_key signature_nonce; - auth_path #pop-options val authenticate_leaf_node_data_from_key_package: #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> + p:principal -> + si_private:nat -> + ln_data:leaf_node_data_nt dy_bytes tkt{ln_data.source == LNS_key_package} -> + crypto (option (leaf_node_nt dy_bytes tkt)) +let authenticate_leaf_node_data_from_key_package #tkt p si_private ln_data = + let* signature_nonce = mk_rand SigNonce (principal_label p) 32 in + let*? private_st = get_private_treesync_state 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 private_st.signature_key signature_nonce) + +val authenticate_leaf_node_data_from_key_package_proof: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> + p:principal -> si_private:nat -> - ln_data:leaf_node_data_nt dy_bytes tkt -> - LCrypto (leaf_node_nt dy_bytes tkt) pr - (requires fun t0 -> - ln_data.source == LNS_key_package /\ - is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_publishable pr.global_usage (trace_len t0)) ln_data /\ - leaf_node_has_event p (trace_len t0) ({data = ln_data; group_id = (); leaf_index = ();}) /\ - has_treesync_invariants tkt pr + ln_data:leaf_node_data_nt dy_bytes tkt{ln_data.source == LNS_key_package} -> + tr:trace -> + Lemma + (requires + is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_publishable tr) ln_data /\ + leaf_node_has_event p tr ({data = ln_data; group_id = (); leaf_index = ();}) /\ + trace_invariant tr /\ + has_treesync_invariants tkt invs ) - (ensures fun t0 ln t1 -> - is_well_formed _ (is_publishable pr.global_usage (trace_len t1)) ln /\ - trace_len t1 == trace_len t0 + 1 + (ensures ( + let (opt_ln, tr_out) = authenticate_leaf_node_data_from_key_package p si_private ln_data tr in + trace_invariant tr_out /\ ( + match opt_ln with + | None -> True + | Some ln -> + is_well_formed _ (is_publishable tr_out) ln + ) + )) +let authenticate_leaf_node_data_from_key_package_proof #invs #tkt p si_private ln_data tr = + let tr_in = tr in + let (signature_nonce, tr) = mk_rand SigNonce (principal_label p) 32 tr in + let (opt_private_st, tr) = get_private_treesync_state p si_private tr in + match opt_private_st with + | None -> () + | Some private_st -> ( + if not (length (signature_nonce <: dy_bytes) = sign_sign_min_entropy_length #dy_bytes) then () + else ( + let (opt_res, tr) = extract_result (sign_leaf_node_data_key_package #dy_bytes #crypto_dy_bytes ln_data private_st.signature_key signature_nonce) tr in + match opt_res with + | None -> () + | Some res -> ( + is_well_formed_prefix_weaken (ps_leaf_node_data_nt tkt) (is_publishable tr_in) (is_knowable_by public tr) ln_data; + is_msg_sign_leaf_node_data_key_package p public tr ln_data private_st.signature_key signature_nonce + ) + ) ) -let authenticate_leaf_node_data_from_key_package #tkt pr p si_private ln_data = - let (|now0, signature_nonce|) = rand_gen #pr (readers [p_id p]) (sig_usage "???") in - let now1 = global_timestamp () in - let private_st = get_private_treesync_state pr p si_private in - guard pr ( - (length (signature_nonce <: dy_bytes) = sign_sign_min_entropy_length #dy_bytes) - ); - is_well_formed_prefix_weaken (ps_leaf_node_data_nt tkt) (is_publishable pr.global_usage now0) (is_publishable pr.global_usage now1) ln_data; - let res = extract_result pr (sign_leaf_node_data_key_package #dy_bytes #crypto_dy_bytes ln_data private_st.signature_key signature_nonce) in - is_msg_sign_leaf_node_data_key_package pr.global_usage p SecrecyLabels.public now1 ln_data private_st.signature_key signature_nonce; - res val authenticate_leaf_node_data_from_update: #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> + p:principal -> si_private:nat -> - ln_data:leaf_node_data_nt dy_bytes tkt -> group_id:mls_bytes dy_bytes -> leaf_index:nat_lbytes 4 -> - LCrypto (leaf_node_nt dy_bytes tkt) pr - (requires fun t0 -> - ln_data.source == LNS_update /\ - is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_publishable pr.global_usage (trace_len t0)) ln_data /\ - is_publishable pr.global_usage (trace_len t0) group_id /\ - leaf_node_has_event p (trace_len t0) ({data = ln_data; group_id; leaf_index;}) /\ - tree_has_event p (trace_len t0) group_id (|0, leaf_index, TLeaf (Some ({data = ln_data; signature = empty #dy_bytes;} <: leaf_node_nt dy_bytes tkt))|) /\ - has_treesync_invariants tkt pr + 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 -> + crypto (option (leaf_node_nt dy_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 (principal_label p) 32 in + let*? private_st = get_private_treesync_state 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 private_st.signature_key signature_nonce) + +val authenticate_leaf_node_data_from_update_proof: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> + p:principal -> + si_private:nat -> + 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 -> + 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))|) /\ + trace_invariant tr /\ + has_treesync_invariants tkt invs ) - (ensures fun t0 ln t1 -> - is_well_formed _ (is_publishable pr.global_usage (trace_len t1)) ln /\ - trace_len t1 == trace_len t0 + 1 + (ensures ( + let (opt_ln, tr_out) = authenticate_leaf_node_data_from_update p si_private ln_data group_id leaf_index tr in + trace_invariant tr_out /\ ( + match opt_ln with + | None -> True + | Some ln -> + is_well_formed _ (is_publishable tr_out) ln + ) + )) +let authenticate_leaf_node_data_from_update_proof #invs #tkt p si_private ln_data group_id leaf_index tr = + let tr_in = tr in + let (signature_nonce, tr) = mk_rand SigNonce (principal_label p) 32 tr in + let (opt_private_st, tr) = get_private_treesync_state p si_private tr in + match opt_private_st with + | None -> () + | Some private_st -> ( + if not (length (signature_nonce <: dy_bytes) >= sign_sign_min_entropy_length #dy_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 private_st.signature_key signature_nonce) tr in + match opt_res with + | None -> () + | Some res -> ( + is_well_formed_prefix_weaken (ps_leaf_node_data_nt tkt) (is_publishable tr_in) (is_knowable_by public tr) ln_data; + is_msg_sign_leaf_node_data_update p public tr ln_data group_id leaf_index private_st.signature_key signature_nonce + ) + ) ) -let authenticate_leaf_node_data_from_update #tkt pr p si_private ln_data group_id leaf_index = - let (|now0, signature_nonce|) = rand_gen #pr (readers [p_id p]) (sig_usage "???") in - let now1 = global_timestamp () in - let private_st = get_private_treesync_state pr p si_private in - guard pr ( - (length (signature_nonce <: dy_bytes) >= sign_sign_min_entropy_length #dy_bytes) - ); - is_well_formed_prefix_weaken (ps_leaf_node_data_nt tkt) (is_publishable pr.global_usage now0) (is_publishable pr.global_usage now1) ln_data; - let res = extract_result pr (sign_leaf_node_data_update #dy_bytes #crypto_dy_bytes ln_data group_id leaf_index private_st.signature_key signature_nonce) in - is_msg_sign_leaf_node_data_update pr.global_usage p SecrecyLabels.public now1 ln_data group_id leaf_index private_st.signature_key signature_nonce; - res (*** Trigger events ***) -val tree_event_triggerable: #tkt:treekem_types dy_bytes -> pr:preds -> p:principal -> time:timestamp -> group_id:mls_bytes dy_bytes -> (l:nat & i:tree_index l & treesync dy_bytes tkt l i) -> prop -let tree_event_triggerable pr p time group_id t = - event_pred_at pr p time (tree_to_event group_id t) - -val trigger_one_tree_event: +#push-options "--ifuel 1" +val trigger_tree_list_event: #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> now:timestamp -> - group_id:mls_bytes dy_bytes -> t:(l:nat & i:tree_index l & treesync dy_bytes tkt l i) -> - squash (tree_event_triggerable pr p now group_id t) -> - LCrypto unit pr - (requires fun t0 -> now == trace_len t0) - (ensures fun t0 () t1 -> - did_event_occur_before p (trace_len t1) (tree_to_event group_id t) /\ - trace_len t1 == trace_len t0 + 1 + p:principal -> + group_id:mls_bytes dy_bytes -> tl:tree_list dy_bytes tkt -> + crypto unit +let rec trigger_tree_list_event #tkt p group_id tl = + match tl with + | [] -> return () + | h::t -> ( + trigger_event p (mk_group_has_tree_event group_id h);* + trigger_tree_list_event p group_id t ) -let trigger_one_tree_event #tkt pr p now group_id t proof = - trigger_event #pr p (tree_to_event group_id t) +#pop-options val trigger_tree_list_event_lemma: #tkt:treekem_types dy_bytes -> - p:principal -> now:timestamp -> + 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 -> - Lemma(tree_list_has_event p now group_id (h::t) <==> (tree_has_event p now group_id h /\ tree_list_has_event p now group_id t)) -let trigger_tree_list_event_lemma #tkt p now group_id h t = + 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 - assert(tree_list_has_event p now group_id (h::t) == ( - tree_has_event p now group_id h /\ - tree_list_has_event p now group_id t + assert(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 )) by ( norm [delta_only [`%tree_list_has_event; `%for_allP]; zeta; iota]; trefl() ) -#push-options "--fuel 1 --ifuel 1 --z3rlimit 25" -val trigger_tree_list_event: +#push-options "--ifuel 1 --fuel 1 --z3rlimit 10" +val trigger_tree_list_event_proof: + {|invs:protocol_invariants|} -> #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> now:timestamp -> + group_has_event_pred: event_predicate (group_has_tree_event dy_bytes tkt) -> + p:principal -> group_id:mls_bytes dy_bytes -> tl:tree_list dy_bytes tkt -> - proof_list:(i:nat{i < List.Tot.length tl} -> squash (tree_event_triggerable pr p (now+i) group_id (List.Tot.index tl i))) -> - LCrypto unit pr - (requires fun t0 -> now == trace_len t0) - (ensures fun t0 () t1 -> - tree_list_has_event p (trace_len t1) group_id tl /\ - trace_len t1 == trace_len t0 + (List.Tot.length tl) + tr:trace -> + Lemma + (requires + (forall t tr_extended. List.Tot.memP t tl /\ tr <$ tr_extended ==> group_has_event_pred tr_extended p (mk_group_has_tree_event group_id t)) /\ + trace_invariant tr /\ + has_event_pred invs group_has_event_pred ) - (decreases tl) -let rec trigger_tree_list_event #tkt pr p now group_id tl event_tl_proof = + (ensures ( + let ((), tr_out) = trigger_tree_list_event p group_id tl tr in + trace_invariant tr_out /\ + tree_list_has_event p tr_out group_id tl + )) +let rec trigger_tree_list_event_proof #invs #tkt group_has_event_pred p group_id tl tr = + let tr_in = tr in match tl with - | [] -> ( - normalize_term_spec (tree_list_has_event p now group_id tl) - ) - | h::t -> ( - // I lost so much time finding that F* needs the following assert - // WTF??? There is definitely a problem in SMT encoding - assert(Cons?.tl tl == t); - trigger_one_tree_event pr p now group_id h (event_tl_proof 0); - trigger_tree_list_event pr p (now+1) group_id t (fun i -> event_tl_proof (i+1)); - let now_end = now + List.Tot.length tl in - trigger_tree_list_event_lemma p now_end group_id h t + | [] -> 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 + 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` + trigger_event_trace_invariant group_has_event_pred p (mk_group_has_tree_event group_id tl_head) tr; + let ((), tr) = trigger_event p (mk_group_has_tree_event group_id tl_head) tr in + trigger_tree_list_event_proof group_has_event_pred p group_id tl_tail tr; + let ((), tr) = trigger_tree_list_event p group_id tl_tail tr in + trigger_tree_list_event_lemma p tr group_id tl_head tl_tail ) #pop-options val trigger_leaf_node_event: #tkt:treekem_types dy_bytes -> - pr:preds -> p:principal -> + p:principal -> ln_tbs:leaf_node_tbs_nt dy_bytes tkt -> - LCrypto unit pr - (requires fun t0 -> event_pred_at pr p (trace_len t0) (leaf_node_to_event ln_tbs)) - (ensures fun t0 () t1 -> - leaf_node_has_event p (trace_len t1) ln_tbs /\ - trace_len t1 == trace_len t0 + 1 + crypto unit +let trigger_leaf_node_event #tkt p ln_tbs = + trigger_event p ln_tbs + +val trigger_leaf_node_event_proof: + {|invs:protocol_invariants|} -> + #tkt:treekem_types dy_bytes -> + leaf_node_has_event_pred: event_predicate (leaf_node_tbs_nt dy_bytes tkt) -> + p:principal -> + ln_tbs:leaf_node_tbs_nt dy_bytes tkt -> + tr:trace -> + Lemma + (requires + leaf_node_has_event_pred tr p ln_tbs /\ + trace_invariant tr /\ + has_event_pred invs leaf_node_has_event_pred ) -let trigger_leaf_node_event #tkt pr p ln_tbs = - trigger_event #pr p (leaf_node_to_event ln_tbs) + (ensures ( + let ((), tr_out) = trigger_leaf_node_event p ln_tbs tr in + trace_invariant tr_out /\ + leaf_node_has_event p tr_out ln_tbs + )) +let trigger_leaf_node_event_proof #invs #tkt leaf_node_has_event_pred p ln_tbs tr = () + diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst index 3c3fbd5..63d8b44 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst @@ -1,19 +1,18 @@ module MLS.TreeSync.Symbolic.AuthServiceCache open Comparse +open DY.Core +open DY.Lib open MLS.NetworkTypes open MLS.TreeSync.NetworkTypes -open ComparseGlue -open GlobalRuntimeLib -open LabeledRuntimeAPI open MLS.Symbolic -open MLS.Symbolic.MapSession #set-options "--fuel 0 --ifuel 0" (*** AS cache types & invariants ***) -type as_cache_key (bytes:Type0) {|bytes_like bytes|} = { +[@@ with_bytes dy_bytes] +type as_cache_key = { verification_key: signature_public_key_nt bytes; credential: credential_nt bytes; } @@ -21,46 +20,47 @@ type as_cache_key (bytes:Type0) {|bytes_like bytes|} = { %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)) -type as_cache_value (bytes:Type0) {|bytes_like bytes|} = { +[@@ with_bytes dy_bytes] +type as_cache_value = { who: principal; [@@@ with_parser #bytes ps_string] usg: string; - time: timestamp; + time: nat; } %splice [ps_as_cache_value] (gen_parser (`as_cache_value)) %splice [ps_as_cache_value_is_well_formed] (gen_is_well_formed_lemma (`as_cache_value)) -val as_cache_types: map_types dy_bytes -let as_cache_types = { - key = as_cache_key dy_bytes; - ps_key = ps_as_cache_key; - value = as_cache_value dy_bytes; - ps_value = ps_as_cache_value; +instance as_cache_types: map_types as_cache_key as_cache_value = { + tag = "MLS.TreeSync.AuthServiceCache"; + ps_key_t = ps_as_cache_key; + ps_value_t = ps_as_cache_value; } -val as_cache_pred: map_predicate as_cache_types -let as_cache_pred = { - pred = (fun gu time (key:as_cache_types.key) value -> - value.time <$ time /\ - is_verification_key gu value.usg (readers [(p_id value.who)]) value.time key.verification_key /\ - is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_publishable gu value.time) key.credential +val as_cache_pred: {|crypto_invariants|} -> map_predicate as_cache_key as_cache_value #_ +let as_cache_pred #ci = { + pred = (fun tr prin state_id key value -> + 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 /\ + is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_publishable (prefix tr value.time)) key.credential ); - pred_later = (fun gu time0 time1 key value -> ()); - pred_is_msg = (fun gu time key value -> - assert(is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_publishable gu time) key.credential) + pred_later = (fun tr1 tr2 prin state_id key value -> ()); + pred_knowable = (fun tr prin state_id key value -> + assert(is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_knowable_by (principal_state_label prin state_id) tr) key.credential) ); } -val as_cache_label: string -let as_cache_label = "MLS.TreeSync.AuthServiceCache" +val has_as_cache_invariant: protocol_invariants -> prop +let has_as_cache_invariant invs = + has_map_session_invariant invs as_cache_pred -val has_as_cache_invariant: preds -> prop -let has_as_cache_invariant pr = - has_map_session_invariant as_cache_types as_cache_pred as_cache_label pr +val as_cache_tag_and_invariant: {|crypto_invariants|} -> string & local_bytes_state_predicate +let as_cache_tag_and_invariant #ci = (as_cache_types.tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant as_cache_pred)) (*** AS cache API ***) -let initialize_as_cache = initialize_map as_cache_types as_cache_pred as_cache_label -let add_verified_credential = add_key_value as_cache_types as_cache_pred as_cache_label -let find_verified_credential = find_value as_cache_types as_cache_pred as_cache_label +let initialize_as_cache = initialize_map as_cache_key as_cache_value +let add_verified_credential = add_key_value #as_cache_key #as_cache_value +let find_verified_credential = find_value #as_cache_key #as_cache_value diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst index 0c262b0..b84a374 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst @@ -1,13 +1,11 @@ module MLS.TreeSync.Symbolic.GlobalUsage -open FStar.Tactics -open LabeledCryptoAPI -open LabeledRuntimeAPI +open Comparse +open DY.Core +open DY.Lib open MLS.Crypto open MLS.TreeSync.NetworkTypes open MLS.Symbolic -open MLS.Symbolic.Session -open MLS.Symbolic.MapSession open MLS.TreeSync.Symbolic.LeafNodeSignature open MLS.TreeSync.Symbolic.AuthServiceCache open MLS.TreeSync.Symbolic.API.Sessions @@ -18,130 +16,97 @@ open MLS.TreeSync.Symbolic.API.KeyPackageManager (*** Predicate definition ***) -val treesync_key_usages: key_usages -let treesync_key_usages = { - dh_shared_secret_usage = (fun _ _ _ -> None); - dh_unknown_peer_usage = (fun _ _ -> None); - dh_usage_commutes_lemma = (fun () -> ()); - dh_unknown_peer_usage_lemma = (fun () -> ()); - kdf_extend_label = (fun _ _ _ _ _ -> None); - kdf_extract_usage = (fun _ _ _ -> None); - kdf_expand_usage = (fun _ _ _ -> None); -} +instance treesync_crypto_usages: crypto_usages = + default_crypto_usages -val can_sign_list: treekem_types dy_bytes -> list (valid_label & sign_pred) -let can_sign_list tkt = [ - (leaf_node_label, leaf_node_spred treesync_key_usages tkt); +val all_sign_preds: treekem_types dy_bytes -> list (valid_label & mls_sign_pred) +let all_sign_preds tkt = [ + leaf_node_tbs_tag_and_invariant tkt; ] -val treesync_usage_preds: treekem_types dy_bytes -> usage_preds -let treesync_usage_preds tkt = { - can_pke_encrypt = (fun _ _ _ _ -> False); - can_aead_encrypt = (fun _ _ _ _ _ -> False); - can_sign = mk_can_sign (can_sign_list tkt); - can_mac = (fun _ _ _ _ -> False); +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 + ); } -val treesync_global_usage: treekem_types dy_bytes -> global_usage -let treesync_global_usage tkt = { - usage_preds = treesync_usage_preds tkt; - key_usages = treesync_key_usages; +instance treesync_crypto_invariants (tkt:treekem_types dy_bytes): crypto_invariants = { + usages = treesync_crypto_usages; + preds = treesync_crypto_predicates tkt; } -val session_pred_list: tkt:treekem_types dy_bytes -> list (string & session_pred) -let session_pred_list tkt = [ - (as_cache_label, map_session_invariant as_cache_types as_cache_pred); - (group_manager_label, map_session_invariant group_manager_types group_manager_pred); - (key_package_manager_label, map_session_invariant (key_package_manager_types tkt) (key_package_manager_pred tkt)); - (treesync_public_state_label, treesync_public_state_pred tkt); - (treesync_private_state_label, treesync_private_state_pred); +val all_state_predicates: tkt:treekem_types dy_bytes -> list (string & local_bytes_state_predicate) +let all_state_predicates tkt = [ + as_cache_tag_and_invariant; + group_manager_tag_and_invariant; + key_package_manager_tag_and_invariant tkt; + treesync_public_state_tag_and_invariant tkt; + treesync_private_state_tag_and_invariant; ] -val treesync_trace_preds: tkt:treekem_types dy_bytes -> trace_preds (treesync_global_usage tkt) -let treesync_trace_preds tkt = { - can_trigger_event = (fun time prin e -> True); - session_st_inv = mk_global_session_pred (session_pred_list tkt) (treesync_global_usage tkt); - session_st_inv_lemma = (fun time prin si vi st -> ( - FStar.Classical.move_requires (mk_global_session_pred_is_msg (session_pred_list tkt) (treesync_global_usage tkt) time prin si vi) st - )); - session_st_inv_later = (fun time0 time1 prin si vi st -> - FStar.Classical.move_requires (mk_global_session_pred_later (session_pred_list tkt) (treesync_global_usage tkt) time0 time1 prin si vi) st - ); +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); + event_pred = mk_event_pred []; } -val treesync_preds: treekem_types dy_bytes -> preds -let treesync_preds tkt = { - global_usage = treesync_global_usage tkt; - trace_preds = treesync_trace_preds tkt; +val treesync_protocol_invariants: treekem_types dy_bytes -> protocol_invariants +let treesync_protocol_invariants tkt = { + crypto_invs = treesync_crypto_invariants tkt; + trace_invs = treesync_trace_invariants tkt; } (*** Proofs ***) -// This tactic is useful because `assert_norm` gets completely lost and eat all the RAM -inline_for_extraction noextract -val sign_memP_tactic: unit -> Tac unit -let sign_memP_tactic () = - norm [delta_only [`%List.Tot.Base.memP; `%can_sign_list]; iota; zeta] +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_pred (treesync_crypto_invariants tkt)) (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_pred_correct (treesync_crypto_invariants tkt) (all_sign_preds tkt); + norm_spec [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP (has_sign_pred (treesync_crypto_invariants tkt)) (all_sign_preds tkt)); + let dumb_lemma (x:prop) (y:prop): Lemma (requires x /\ x == y) (ensures y) = () in + dumb_lemma (for_allP (has_sign_pred (treesync_crypto_invariants tkt)) (all_sign_preds tkt)) (norm [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP (has_sign_pred (treesync_crypto_invariants tkt)) (all_sign_preds tkt))) val treesync_global_usage_has_leaf_node_tbs_invariant: tkt:treekem_types dy_bytes -> Lemma - (has_leaf_node_tbs_invariant tkt (treesync_global_usage tkt)) - [SMTPat (has_leaf_node_tbs_invariant tkt (treesync_global_usage tkt))] + (has_leaf_node_tbs_invariant tkt (treesync_crypto_invariants tkt)) + [SMTPat (has_leaf_node_tbs_invariant tkt (treesync_crypto_invariants tkt))] let treesync_global_usage_has_leaf_node_tbs_invariant tkt = - assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (can_sign_list tkt))); - assert(List.Tot.memP (leaf_node_label, (leaf_node_spred treesync_key_usages tkt)) (can_sign_list tkt)) by (sign_memP_tactic()); - mk_can_sign_correct (treesync_global_usage tkt) (can_sign_list tkt) leaf_node_label (leaf_node_spred treesync_key_usages tkt) - -inline_for_extraction noextract -val session_memP_tactic: unit -> Tac unit -let session_memP_tactic () = - norm [delta_only [`%List.Tot.Base.memP; `%session_pred_list]; iota; zeta] - -val treesync_preds_has_as_cache_invariant: tkt:treekem_types dy_bytes -> Lemma - (has_as_cache_invariant (treesync_preds tkt)) - [SMTPat (has_as_cache_invariant (treesync_preds tkt))] -let treesync_preds_has_as_cache_invariant tkt = - let lab = as_cache_label in - let spred = (map_session_invariant as_cache_types as_cache_pred) in - assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (session_pred_list tkt))); - assert(List.Tot.memP (lab, spred) (session_pred_list tkt)) by (session_memP_tactic()); - mk_global_session_pred_correct (treesync_preds tkt) (session_pred_list tkt) lab spred - -val treesync_preds_has_group_manager_invariant: tkt:treekem_types dy_bytes -> Lemma - (has_group_manager_invariant (treesync_preds tkt)) - [SMTPat (has_group_manager_invariant (treesync_preds tkt))] -let treesync_preds_has_group_manager_invariant tkt = - let lab = group_manager_label in - let spred = (map_session_invariant group_manager_types group_manager_pred) in - assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (session_pred_list tkt))); - assert(List.Tot.memP (lab, spred) (session_pred_list tkt)) by (session_memP_tactic()); - mk_global_session_pred_correct (treesync_preds tkt) (session_pred_list tkt) lab spred - -val treesync_preds_has_key_package_manager_invariant: tkt:treekem_types dy_bytes -> Lemma - (has_key_package_manager_invariant tkt (treesync_preds tkt)) - [SMTPat (has_key_package_manager_invariant tkt (treesync_preds tkt))] -let treesync_preds_has_key_package_manager_invariant tkt = - let lab = key_package_manager_label in - let spred = (map_session_invariant (key_package_manager_types tkt) (key_package_manager_pred tkt)) in - assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (session_pred_list tkt))); - assert(List.Tot.memP (lab, spred) (session_pred_list tkt)) by (session_memP_tactic()); - mk_global_session_pred_correct (treesync_preds tkt) (session_pred_list tkt) lab spred - -val treesync_preds_has_treesync_public_state_invariant: tkt:treekem_types dy_bytes -> Lemma - (has_treesync_public_state_invariant tkt (treesync_preds tkt)) - [SMTPat (has_treesync_public_state_invariant tkt (treesync_preds tkt))] -let treesync_preds_has_treesync_public_state_invariant tkt = - let lab = treesync_public_state_label in - let spred = treesync_public_state_pred tkt in - assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (session_pred_list tkt))); - assert(List.Tot.memP (lab, spred) (session_pred_list tkt)) by (session_memP_tactic()); - mk_global_session_pred_correct (treesync_preds tkt) (session_pred_list tkt) lab spred - -val treesync_preds_has_treesync_private_state_invariant: tkt:treekem_types dy_bytes -> Lemma - (has_treesync_private_state_invariant (treesync_preds tkt)) - [SMTPat (has_treesync_private_state_invariant (treesync_preds tkt))] -let treesync_preds_has_treesync_private_state_invariant tkt = - let lab = treesync_private_state_label in - let spred = treesync_private_state_pred in - assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (session_pred_list tkt))); - assert(List.Tot.memP (lab, spred) (session_pred_list tkt)) by (session_memP_tactic()); - mk_global_session_pred_correct (treesync_preds tkt) (session_pred_list tkt) lab spred + all_sign_preds_has_all_sign_preds 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); + 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 + (has_as_cache_invariant (treesync_protocol_invariants tkt)) + [SMTPat (has_as_cache_invariant (treesync_protocol_invariants tkt))] +let treesync_protocol_invariants_has_as_cache_invariant tkt = + all_state_predicates_has_all_state_predicates tkt + +val treesync_protocol_invariants_has_group_manager_invariant: tkt:treekem_types dy_bytes -> Lemma + (has_group_manager_invariant (treesync_protocol_invariants tkt)) + [SMTPat (has_group_manager_invariant (treesync_protocol_invariants tkt))] +let treesync_protocol_invariants_has_group_manager_invariant tkt = + all_state_predicates_has_all_state_predicates tkt + +val treesync_protocol_invariants_has_key_package_manager_invariant: tkt:treekem_types dy_bytes -> Lemma + (has_key_package_manager_invariant tkt (treesync_protocol_invariants tkt)) + [SMTPat (has_key_package_manager_invariant tkt (treesync_protocol_invariants tkt))] +let treesync_protocol_invariants_has_key_package_manager_invariant tkt = + all_state_predicates_has_all_state_predicates tkt + +val treesync_protocol_invariants_has_treesync_public_state_invariant: tkt:treekem_types dy_bytes -> Lemma + (has_treesync_public_state_invariant tkt (treesync_protocol_invariants tkt)) + [SMTPat (has_treesync_public_state_invariant tkt (treesync_protocol_invariants tkt))] +let treesync_protocol_invariants_has_treesync_public_state_invariant tkt = + all_state_predicates_has_all_state_predicates tkt + +val treesync_protocol_invariants_has_treesync_private_state_invariant: tkt:treekem_types dy_bytes -> Lemma + (has_treesync_private_state_invariant (treesync_protocol_invariants tkt)) + [SMTPat (has_treesync_private_state_invariant (treesync_protocol_invariants tkt))] +let treesync_protocol_invariants_has_treesync_private_state_invariant tkt = + all_state_predicates_has_all_state_predicates tkt diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.IsWellFormed.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.IsWellFormed.fst index dd618bf..8ae4aa8 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.IsWellFormed.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.IsWellFormed.fst @@ -273,26 +273,19 @@ let rec is_well_formed_set_path_leaf #bytes #bl pre #tkt #l #i #li p ln = | PLeaf _ -> () | PNode _ p_next -> is_well_formed_set_path_leaf pre p_next ln +open DY.Core open MLS.Symbolic -val pre_is_hash_compatible_is_msg: - p:global_usage -> l:label -> i:timestamp -> +val pre_is_hash_compatible_is_knowable_by: + {|crypto_invariants|} -> l:label -> tr:trace -> Lemma - (pre_is_hash_compatible (is_msg p l i)) - [SMTPat (pre_is_hash_compatible (is_msg p l i))] -let pre_is_hash_compatible_is_msg p l i = - introduce forall b. (is_msg p l i b /\ Success? (hash_hash b)) ==> is_msg p l i (Success?.v (hash_hash b)) - with ( - introduce _ ==> _ - with _. ( - LabeledCryptoAPI.hash_lemma #p #i #l b - ) - ) + (pre_is_hash_compatible (is_knowable_by l tr)) + [SMTPat (pre_is_hash_compatible (is_knowable_by l tr))] +let pre_is_hash_compatible_is_knowable_by #ci l tr = () -val pre_is_hash_compatible_is_valid: - p:global_usage -> i:timestamp -> +val pre_is_hash_compatible_bytes_invariant: + {|crypto_invariants|} -> tr:trace -> Lemma - (pre_is_hash_compatible (is_valid p i)) - [SMTPat (pre_is_hash_compatible (is_valid p i))] -let pre_is_hash_compatible_is_valid p i = - pre_is_hash_compatible_is_msg p SecrecyLabels.private_label i + (pre_is_hash_compatible (bytes_invariant tr)) + [SMTPat (pre_is_hash_compatible (bytes_invariant tr))] +let pre_is_hash_compatible_bytes_invariant tr = () diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst index 41fa73b..561ff36 100644 --- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst +++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst @@ -2,6 +2,8 @@ module MLS.TreeSync.Symbolic.LeafNodeSignature open FStar.Mul open Comparse +open DY.Core +open DY.Lib open MLS.Crypto open MLS.Tree open MLS.NetworkTypes @@ -26,46 +28,41 @@ open MLS.Result (*** Predicates ***) -type dy_as_token_ (bytes:Type0) {|bytes_like bytes|} = { +[@@ with_bytes dy_bytes] +type dy_as_token = { who: principal; - time: timestamp; + time: nat; } -%splice [ps_dy_as_token_] (gen_parser (`dy_as_token_)) -%splice [ps_dy_as_token__is_well_formed] (gen_is_well_formed_lemma (`dy_as_token_)) - -let dy_as_token = dy_as_token_ dy_bytes -let ps_dy_as_token: parser_serializer dy_bytes dy_as_token = ps_dy_as_token_ +%splice [ps_dy_as_token] (gen_parser (`dy_as_token)) +%splice [ps_dy_as_token_is_well_formed] (gen_is_well_formed_lemma (`dy_as_token)) /// Instantiation of the abstract "Authentication Service" for DY*. /// The token is a a principal and a timestamp, /// and the AS attests that the signature verification key belonged to that principal at that time. -val dy_asp: global_usage -> timestamp -> as_parameters dy_bytes -let dy_asp gu current_time = { +val dy_asp: {|crypto_invariants|} -> trace -> as_parameters dy_bytes +let dy_asp #ci tr = { token_t = dy_as_token; credential_ok = (fun (vk, cred) token -> - token.time <$ current_time /\ - is_verification_key gu "MLS.LeafSignKey" (readers [p_id token.who]) token.time vk + token.time <= (DY.Core.Trace.Type.length tr) /\ + bytes_invariant (prefix tr token.time) vk /\ + get_signkey_usage vk == SigKey "MLS.LeafSignKey" /\ + get_signkey_label vk == principal_label token.who ); valid_successor = (fun (vk_old, cred_old) (vk_new, cred_new) -> True ); } -val leaf_node_to_event: - #tkt:treekem_types dy_bytes -> - leaf_node_tbs_nt dy_bytes tkt -> - event -let leaf_node_to_event #tkt ln_tbs = - let evt_bytes = serialize _ ln_tbs in - ("MLS.TreeSync.LeafNodeEvent", [evt_bytes]) +instance event_leaf_node_event (tkt:treekem_types dy_bytes): event (leaf_node_tbs_nt dy_bytes tkt) = + mk_event_instance "MLS.TreeSync.LeafNodeEvent" val leaf_node_has_event: #tkt:treekem_types dy_bytes -> - principal -> timestamp -> leaf_node_tbs_nt dy_bytes tkt -> + principal -> trace -> leaf_node_tbs_nt dy_bytes tkt -> prop -let leaf_node_has_event #tkt prin time ln_tbs = - did_event_occur_before prin time (leaf_node_to_event ln_tbs) +let leaf_node_has_event #tkt prin tr ln_tbs = + event_triggered tr prin ln_tbs type group_has_tree_event (bytes:Type0) {|bytes_like bytes|} (tkt:treekem_types bytes) = { group_id: mls_bytes bytes; @@ -94,36 +91,37 @@ let tree_has_event_arithmetic_lemma l i = ) #pop-options -val tree_to_event: +instance event_group_has_tree_event (tkt:treekem_types dy_bytes): event (group_has_tree_event dy_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) -> - event -let tree_to_event #tkt group_id (|l, i, t|) = + group_has_tree_event dy_bytes tkt +let mk_group_has_tree_event #tkt group_id (|l, i, t|) = tree_has_event_arithmetic_lemma l i; - let evt: group_has_tree_event dy_bytes tkt = { + { group_id; l; i = i/(pow2 l); t; - } in - let evt_bytes = serialize _ evt in - ("MLS.TreeSync.GroupHasTreeEvent", [evt_bytes]) + } val tree_has_event: #tkt:treekem_types dy_bytes -> - principal -> timestamp -> + principal -> trace -> mls_bytes dy_bytes -> (l:nat & i:tree_index l & treesync dy_bytes tkt l i) -> prop -let tree_has_event #tkt prin time group_id (|l, i, t|) = - did_event_occur_before prin time (tree_to_event group_id (|l, i, t|)) +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 -> - principal -> timestamp -> + principal -> trace -> mls_bytes dy_bytes -> tree_list dy_bytes tkt -> prop -let tree_list_has_event #tkt prin time group_id tl = - for_allP (tree_has_event prin time group_id) tl +let tree_list_has_event #tkt prin tr group_id tl = + for_allP (tree_has_event prin tr group_id) tl val leaf_node_label: string let leaf_node_label = "LeafNodeTBS" @@ -133,38 +131,52 @@ let leaf_node_label = "LeafNodeTBS" /// the leaf attests the existence of a tree list, /// that is parent-hash linked and goes up to the root, /// furthermore one event "GroupHasTreeEvent" was triggered for each of these trees. -val leaf_node_spred: - key_usages -> treekem_types dy_bytes -> - sign_pred -let leaf_node_spred ku tkt usg time vk ln_tbs_bytes = - match (parse (leaf_node_tbs_nt dy_bytes tkt) ln_tbs_bytes) with - | None -> False - | Some ln_tbs -> ( - exists prin. - leaf_node_has_event prin time ln_tbs /\ ( - match ln_tbs.data.source with - | LNS_commit -> ( - exists (tl: tree_list dy_bytes tkt). - get_signkey_label ku vk == readers [p_id prin] /\ - tree_list_starts_with_tbs tl ln_tbs_bytes /\ - tree_list_is_parent_hash_linkedP tl /\ - tree_list_ends_at_root tl /\ - tree_list_is_canonicalized ln_tbs.leaf_index tl /\ - tree_list_has_event prin time ln_tbs.group_id tl - ) - | LNS_update -> ( - get_signkey_label ku vk == readers [p_id prin] /\ - tree_has_event prin time 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))|) - ) - | LNS_key_package -> True - ) - ) +#push-options "--fuel 0 --z3rlimit 25" +val leaf_node_sign_pred: + {|crypto_usages|} -> treekem_types dy_bytes -> + mls_sign_pred +let leaf_node_sign_pred #cu tkt = { + pred = (fun tr vk ln_tbs_bytes -> + match (parse (leaf_node_tbs_nt dy_bytes tkt) ln_tbs_bytes) with + | None -> False + | Some ln_tbs -> ( + exists prin. + leaf_node_has_event prin tr ln_tbs /\ ( + match ln_tbs.data.source with + | LNS_commit -> ( + exists (tl: tree_list dy_bytes tkt). + get_signkey_label vk == principal_label prin /\ + tree_list_starts_with_tbs tl ln_tbs_bytes /\ + tree_list_is_parent_hash_linkedP tl /\ + tree_list_ends_at_root tl /\ + tree_list_is_canonicalized ln_tbs.leaf_index tl /\ + tree_list_has_event prin tr ln_tbs.group_id tl + ) + | LNS_update -> ( + get_signkey_label vk == principal_label prin /\ + 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))|) + ) + | LNS_key_package -> True + ) + ) + ); + pred_later = (fun tr1 tr2 vk 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) + with ( + for_allP_eq (tree_has_event prin tr group_id) tl + ) + ); +} +#pop-options val has_leaf_node_tbs_invariant: - treekem_types dy_bytes -> global_usage -> + treekem_types dy_bytes -> crypto_invariants -> prop -let has_leaf_node_tbs_invariant tkt gu = - has_sign_pred gu leaf_node_label (leaf_node_spred gu.key_usages tkt) +let has_leaf_node_tbs_invariant tkt ci = + has_sign_pred ci (leaf_node_label, leaf_node_sign_pred tkt) + +val leaf_node_tbs_tag_and_invariant: {|crypto_usages|} -> treekem_types dy_bytes -> (valid_label & mls_sign_pred) +let leaf_node_tbs_tag_and_invariant #cu tkt = (leaf_node_label, leaf_node_sign_pred tkt) (*** Proof of verification, for a tree ***) @@ -292,37 +304,38 @@ let rec is_well_formed_leaf_at #bytes #bl #tkt #l #i pre t li = /// we conclude. #push-options "--z3rlimit 100" val parent_hash_implies_event: + {|ci:crypto_invariants|} -> #tkt:treekem_types dy_bytes -> #l:nat -> #i:tree_index l -> - gu:global_usage -> time:timestamp -> - group_id:mls_bytes dy_bytes -> t:treesync dy_bytes tkt l i -> ast:as_tokens dy_bytes (dy_asp gu time).token_t l i -> + 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 -> Lemma (requires - has_leaf_node_tbs_invariant tkt gu /\ + has_leaf_node_tbs_invariant tkt ci /\ unmerged_leaves_ok t /\ parent_hash_invariant t /\ valid_leaves_invariant group_id t /\ node_has_parent_hash t /\ all_credentials_ok t ast /\ - is_well_formed _ (is_valid gu time) t /\ - is_valid gu time group_id + is_well_formed _ (bytes_invariant tr) t /\ + bytes_invariant tr group_id ) (ensures ( let authentifier_li = get_authentifier_index t in let authentifier = (Some?.v (leaf_at ast authentifier_li)).who in ( - tree_has_event authentifier time group_id (|l, i, (canonicalize t authentifier_li)|) + tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|) ) \/ ( - is_corrupt time (p_id authentifier) + is_corrupt tr (principal_label authentifier) ) )) -let parent_hash_implies_event #tkt #l #i gu time group_id t ast = +let parent_hash_implies_event #ci #tkt #l #i tr group_id t ast = let my_tl = parent_hash_invariant_to_tree_list t in let (|leaf_l, leaf_i, leaf|) = List.Tot.hd my_tl in tree_list_head_subtree_tail my_tl; leaf_at_subtree_leaf leaf t; leaf_at_valid_leaves group_id t leaf_i; - is_well_formed_leaf_at (is_valid gu time) t leaf_i; + is_well_formed_leaf_at (bytes_invariant tr) t leaf_i; let TLeaf (Some ln) = leaf in let ln_tbs: leaf_node_tbs_nt dy_bytes tkt = { data = ln.data; @@ -333,32 +346,28 @@ let parent_hash_implies_event #tkt #l #i gu time group_id t ast = let leaf_token = Some?.v (leaf_at ast leaf_i) in let authentifier = leaf_token.who in let authentifier_li = leaf_i in - let leaf_sk_label = readers [p_id leaf_token.who] in - serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (is_valid gu time) ln_tbs; - verify_with_label_is_valid gu (leaf_node_spred gu.key_usages tkt) "MLS.LeafSignKey" leaf_sk_label time ln.data.signature_key "LeafNodeTBS" ln_tbs_bytes ln.signature; + let leaf_sk_label = principal_label leaf_token.who in + serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (bytes_invariant tr) ln_tbs; + bytes_invariant_verify_with_label (leaf_node_sign_pred tkt) tr ln.data.signature_key "LeafNodeTBS" ln_tbs_bytes ln.signature; - introduce (exists time_sig. time_sig <$ time /\ leaf_node_spred gu.key_usages tkt "MLS.LeafSignKey" time_sig ln.data.signature_key ln_tbs_bytes) ==> tree_has_event authentifier time group_id (|l, i, (canonicalize t authentifier_li)|) + introduce ((leaf_node_sign_pred tkt).pred tr ln.data.signature_key ln_tbs_bytes) ==> tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|) with _. ( - eliminate exists time_sig. time_sig <$ time /\ leaf_node_spred gu.key_usages tkt "MLS.LeafSignKey" time_sig ln.data.signature_key ln_tbs_bytes - returns tree_has_event authentifier time group_id (|l, i, (canonicalize t authentifier_li)|) - with _. ( + ( parse_serialize_inv_lemma #dy_bytes (leaf_node_tbs_nt dy_bytes tkt) ln_tbs; eliminate exists (prin:principal) (leaf_tl: tree_list dy_bytes tkt). - get_signkey_label gu.key_usages ln.data.signature_key == readers [p_id prin] /\ + get_signkey_label ln.data.signature_key == principal_label prin /\ 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 /\ tree_list_is_canonicalized authentifier_li leaf_tl /\ - tree_list_has_event prin time_sig ln_tbs.group_id leaf_tl - returns tree_has_event authentifier time group_id (|l, i, (canonicalize t authentifier_li)|) + tree_list_has_event prin tr ln_tbs.group_id leaf_tl + returns tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|) with _. ( let (b1, b2) = parent_hash_guarantee_theorem my_tl leaf_tl ln_tbs_bytes in - hash_hash_inj b1 b2; + FStar.Classical.move_requires_2 hash_injective b1 b2; last_tree_equivalent my_tl leaf_tl leaf_i; - for_allP_eq (tree_has_event prin time_sig group_id) leaf_tl; - is_verification_key_to_signkey_label gu "MLS.LeafSignKey" (readers [p_id authentifier]) time ln.data.signature_key; - readers_is_injective prin authentifier; + for_allP_eq (tree_has_event prin tr group_id) leaf_tl; let (|_, _, original_t|) = List.Tot.index leaf_tl (List.Tot.length my_tl - 1) in List.Tot.lemma_index_memP leaf_tl (List.Tot.length my_tl - 1); for_allP_eq (tree_is_canonicalized authentifier_li) leaf_tl; @@ -367,10 +376,8 @@ let parent_hash_implies_event #tkt #l #i gu time group_id t ast = ) ); - introduce (can_flow time leaf_sk_label public) ==> is_corrupt time (p_id ((Some?.v (leaf_at ast (get_authentifier_index t))).who)) - with _. ( - can_flow_to_public_implies_corruption time (p_id leaf_token.who) - ) + introduce (can_flow tr leaf_sk_label public) ==> is_corrupt tr (principal_label ((Some?.v (leaf_at ast (get_authentifier_index t))).who)) + with _. () #pop-options (*** Proof of verification, for a state ***) @@ -432,17 +439,19 @@ let rec all_credentials_ok_subtree #bytes #cb #tkt #asp #lp #ld #ip #id d p ast_ /// - or the principal at the leaf is corrupt. /// This theorem is mostly a wrapper around `parent_hash_implies_event`. val state_implies_event: + {|ci:crypto_invariants|} -> #tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes -> #l:nat -> #i:tree_index l -> - gu:global_usage -> time:timestamp -> - st:treesync_state dy_bytes tkt (dy_asp gu time) group_id -> t:treesync dy_bytes tkt l i -> ast:as_tokens dy_bytes (dy_asp gu time).token_t l i -> + 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 -> Lemma (requires - has_leaf_node_tbs_invariant tkt gu /\ + has_leaf_node_tbs_invariant tkt ci /\ node_has_parent_hash t /\ - is_well_formed _ (is_valid gu time) (st.tree <: treesync _ _ _ _) /\ - is_valid gu time group_id /\ + is_well_formed _ (bytes_invariant tr) (st.tree <: treesync _ _ _ _) /\ + bytes_invariant tr group_id /\ is_subtree_of t st.tree /\ - is_subtree_of ast st.tokens + is_subtree_of ast st.tokens /\ + treesync_state_valid (dy_asp tr) st ) (ensures ( // The following line is only there as precondition for the rest of the theorem @@ -450,19 +459,19 @@ val state_implies_event: let authentifier_li = get_authentifier_index t in let authentifier = (Some?.v (leaf_at ast authentifier_li)).who in ( - tree_has_event authentifier time group_id (|l, i, (canonicalize t authentifier_li)|) + tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|) ) \/ ( - is_corrupt time (p_id authentifier) + is_corrupt tr (principal_label authentifier) ) ) )) -let state_implies_event #tkt #group_id #l #i gu time st t ast = +let state_implies_event #ci #tkt #group_id #l #i tr st t ast = unmerged_leaves_ok_subtree t st.tree; parent_hash_invariant_subtree t st.tree; valid_leaves_invariant_subtree group_id t st.tree; - is_well_formed_treesync_subtree (is_valid gu time) t st.tree; + is_well_formed_treesync_subtree (bytes_invariant tr) t st.tree; all_credentials_ok_subtree t st.tree ast st.tokens; - parent_hash_implies_event gu time group_id t ast + parent_hash_implies_event tr group_id t ast (*** Proof of path signature ***) @@ -606,10 +615,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 -> #l:nat -> #li:leaf_index l 0 -> - prin:principal -> time:timestamp -> + 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 -> prop -let external_path_has_event #tkt #l #li prin time t p group_id = +let external_path_has_event #tkt #l #li prin tr t p group_id = (get_path_leaf p).source == LNS_update /\ li < pow2 32 /\ Success? (external_path_to_path_nosig t p group_id) /\ ( @@ -619,8 +628,8 @@ let external_path_has_event #tkt #l #li prin time t p group_id = 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); - leaf_node_has_event prin time ({data = auth_ln.data; group_id; leaf_index = li;}) /\ - tree_list_has_event prin time group_id (path_to_tree_list t auth_p) + 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) ) /// Proof that the path generated by `external_path_to_path` @@ -632,9 +641,10 @@ let external_path_has_event #tkt #l #li prin time t p group_id = /// With label= SecrecyLabels.private_label, we get a version with `is_valid`. #push-options "--z3rlimit 100" val is_msg_external_path_to_path: + {|ci:crypto_invariants|} -> #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 -> - gu:global_usage -> prin:principal -> label:label -> time:timestamp -> + 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 -> Lemma @@ -643,18 +653,18 @@ val is_msg_external_path_to_path: Success? (external_path_to_path t p group_id sk nonce) /\ path_is_filter_valid t p /\ unmerged_leaves_ok t /\ - external_path_has_event prin time t p group_id /\ - is_well_formed _ (is_msg gu label time) t /\ - is_well_formed _ (is_msg gu label time) p /\ - is_msg gu label time group_id /\ - is_valid gu time sk /\ get_usage gu sk == Some (sig_usage "MLS.LeafSignKey") /\ - is_valid gu time nonce /\ - get_label gu sk == readers [p_id prin] /\ - get_label gu nonce == readers [p_id prin] /\ - has_leaf_node_tbs_invariant tkt gu + external_path_has_event prin tr t p group_id /\ + 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 nonce /\ get_usage nonce == SigNonce /\ + get_label sk == principal_label prin /\ + get_label nonce == principal_label prin /\ + has_leaf_node_tbs_invariant tkt ci ) - (ensures is_well_formed _ (is_msg gu label time) (Success?.v (external_path_to_path t p group_id sk nonce))) -let is_msg_external_path_to_path #tkt #l #li gu prin label time t p group_id sk nonce = + (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 ln_data = get_path_leaf p in let new_ln_data = { ln_data with source = LNS_commit; parent_hash = computed_parent_hash; } in @@ -669,82 +679,81 @@ let is_msg_external_path_to_path #tkt #l #li gu prin label time t p group_id sk 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_msg gu label time) t p (root_parent_hash #dy_bytes); - is_well_formed_get_path_leaf (is_msg gu label time) p; - serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (is_msg gu label time) ({data = new_ln_data; group_id; leaf_index = li;}); + pre_compute_leaf_parent_hash_from_path (is_knowable_by label tr) t p (root_parent_hash #dy_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;}); let tl = path_to_tree_list t unsigned_path in path_to_tree_list_lemma t unsigned_path; introduce exists prin tl. - get_signkey_label gu.key_usages (CryptoLib.vk sk) == readers [p_id prin] /\ + get_signkey_label (vk sk) == principal_label prin /\ tree_list_starts_with_tbs tl new_ln_tbs_bytes /\ tree_list_is_parent_hash_linkedP tl /\ tree_list_ends_at_root tl /\ - tree_list_has_event prin time new_ln_tbs.group_id tl /\ + tree_list_has_event prin tr new_ln_tbs.group_id tl /\ tree_list_is_canonicalized li tl /\ - leaf_node_has_event prin time new_ln_tbs - with prin tl and ( - LabeledCryptoAPI.vk_lemma #gu #time #(readers [p_id prin]) sk - ); + leaf_node_has_event prin tr new_ln_tbs + with prin tl and (); parse_serialize_inv_lemma #dy_bytes (leaf_node_tbs_nt dy_bytes tkt) new_ln_tbs; - sign_with_label_valid gu (leaf_node_spred gu.key_usages tkt) "MLS.LeafSignKey" time sk "LeafNodeTBS" new_ln_tbs_bytes nonce; - is_well_formed_set_path_leaf (is_msg gu label time) p new_ln + bytes_invariant_sign_with_label (leaf_node_sign_pred tkt) tr sk "LeafNodeTBS" new_ln_tbs_bytes nonce; + is_well_formed_set_path_leaf (is_knowable_by label tr) p new_ln #pop-options (*** Proof of individual leaf signature ***) #push-options "--z3rlimit 25" val is_msg_sign_leaf_node_data_key_package: + {|ci:crypto_invariants|} -> #tkt:treekem_types dy_bytes -> - gu:global_usage -> prin:principal -> label:label -> time:timestamp -> + prin:principal -> label:label -> tr:trace -> ln_data:leaf_node_data_nt dy_bytes tkt -> sk:dy_bytes -> nonce:sign_nonce dy_bytes -> Lemma (requires ln_data.source == LNS_key_package /\ Success? (sign_leaf_node_data_key_package ln_data sk nonce) /\ - leaf_node_has_event prin time ({data = ln_data; group_id = (); leaf_index = ();}) /\ - is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_msg gu label time) ln_data /\ - is_valid gu time sk /\ get_usage gu sk == Some (sig_usage "MLS.LeafSignKey") /\ - is_valid gu time nonce /\ - get_label gu sk == readers [p_id prin] /\ - get_label gu nonce == readers [p_id prin] /\ - has_leaf_node_tbs_invariant tkt gu + 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 nonce /\ get_usage nonce == SigNonce /\ + get_label sk == principal_label prin /\ + get_label nonce == principal_label prin /\ + has_leaf_node_tbs_invariant tkt ci ) - (ensures is_well_formed _ (is_msg gu label time) (Success?.v (sign_leaf_node_data_key_package ln_data sk nonce))) -let is_msg_sign_leaf_node_data_key_package #tkt gu prin label time ln_data sk nonce = + (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_msg gu label time) ln_tbs; - sign_with_label_valid gu (leaf_node_spred gu.key_usages tkt) "MLS.LeafSignKey" time sk "LeafNodeTBS" ln_tbs_bytes nonce + serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (is_knowable_by label tr) ln_tbs; + bytes_invariant_sign_with_label (leaf_node_sign_pred tkt) tr sk "LeafNodeTBS" ln_tbs_bytes nonce #pop-options #push-options "--z3rlimit 25" val is_msg_sign_leaf_node_data_update: + {|ci:crypto_invariants|} -> #tkt:treekem_types dy_bytes -> - gu:global_usage -> prin:principal -> label:label -> time:timestamp -> + 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 -> 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 time ({data = ln_data; group_id; leaf_index;}) /\ - tree_has_event prin time 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_msg gu label time) ln_data /\ - is_msg gu label time group_id /\ - is_valid gu time sk /\ get_usage gu sk == Some (sig_usage "MLS.LeafSignKey") /\ - is_valid gu time nonce /\ - get_label gu sk == readers [p_id prin] /\ - get_label gu nonce == readers [p_id prin] /\ - has_leaf_node_tbs_invariant tkt gu + 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))|) /\ + 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 nonce /\ get_usage nonce == SigNonce /\ + get_label sk == principal_label prin /\ + get_label nonce == principal_label prin /\ + has_leaf_node_tbs_invariant tkt ci ) - (ensures is_well_formed _ (is_msg gu label time) (Success?.v (sign_leaf_node_data_update ln_data group_id leaf_index sk nonce))) -let is_msg_sign_leaf_node_data_update #tkt gu prin label time ln_data group_id leaf_index sk nonce = + (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_msg gu label time) ln_tbs; - LabeledCryptoAPI.vk_lemma #gu #time #(readers [p_id prin]) sk; - sign_with_label_valid gu (leaf_node_spred gu.key_usages tkt) "MLS.LeafSignKey" time sk "LeafNodeTBS" ln_tbs_bytes nonce + serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (is_knowable_by label tr) ln_tbs; + bytes_invariant_sign_with_label (leaf_node_sign_pred tkt) tr sk "LeafNodeTBS" ln_tbs_bytes nonce #pop-options