From 022e30a934a7ca97de8b4dc25b4ff1b44c693516 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= <theophile@wallez.net>
Date: Thu, 1 Aug 2024 21:03:02 +0200
Subject: [PATCH] cleanup: move SignWithLabel splitting in a separate file

and introduce two layers of predicate splitting:
- one based on the usage of signature keys,
  to combine with other protocols (new)
- one based on SignWithLabel,
  to combine with other MLS sub-protocols
---
 Makefile                                      |   2 +-
 .../proofs/MLS.Crypto.Derived.Lemmas.fst      |  13 ++
 ....Crypto.Derived.Symbolic.SignWithLabel.fst | 211 ++++++++++++++++++
 fstar/symbolic/MLS.Symbolic.fst               | 170 --------------
 .../MLS.TreeSync.Symbolic.GlobalUsage.fst     |  80 +++----
 ...LS.TreeSync.Symbolic.LeafNodeSignature.fst |  11 +-
 6 files changed, 264 insertions(+), 223 deletions(-)
 create mode 100644 fstar/common/proofs/MLS.Crypto.Derived.Lemmas.fst
 create mode 100644 fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst

diff --git a/Makefile b/Makefile
index ac3a8ba..4627209 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@ DY_HOME       ?= $(MLS_HOME)/../dolev-yao-star
 NO_DY ?=
 USE_DY = $(if $(NO_DY),, 1)
 
-INNER_SOURCE_DIRS = api bootstrap common/code common/proofs glue/code glue/proofs test treedem treekem/code treekem/proofs treemath treesync/code treesync/proofs $(if $(USE_DY), symbolic treesync/symbolic)
+INNER_SOURCE_DIRS = api bootstrap common/code common/proofs common/symbolic glue/code glue/proofs test treedem treekem/code treekem/proofs treemath treesync/code treesync/proofs $(if $(USE_DY), symbolic treesync/symbolic)
 
 HACL_SNAPSHOT_DIR = $(MLS_HOME)/hacl-star-snapshot
 SOURCE_DIRS = $(addprefix $(MLS_HOME)/fstar/, $(INNER_SOURCE_DIRS))
diff --git a/fstar/common/proofs/MLS.Crypto.Derived.Lemmas.fst b/fstar/common/proofs/MLS.Crypto.Derived.Lemmas.fst
new file mode 100644
index 0000000..93000cf
--- /dev/null
+++ b/fstar/common/proofs/MLS.Crypto.Derived.Lemmas.fst
@@ -0,0 +1,13 @@
+module MLS.Crypto.Derived.Lemmas
+
+open MLS.Crypto.Derived
+
+#push-options "--fuel 0 --ifuel 0"
+
+val get_mls_label_inj:
+  l1:valid_label -> l2:valid_label ->
+  Lemma
+  (requires get_mls_label l1 == get_mls_label l2)
+  (ensures l1 == l2)
+let get_mls_label_inj l1 l2 =
+  String.concat_injective "MLS 1.0 " "MLS 1.0 " l1 l2
diff --git a/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst b/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
new file mode 100644
index 0000000..d84f660
--- /dev/null
+++ b/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
@@ -0,0 +1,211 @@
+module MLS.Crypto.Derived.Symbolic.SignWithLabel
+
+open Comparse
+open DY.Core
+open DY.Lib
+open MLS.NetworkTypes
+open MLS.Crypto
+open MLS.Crypto.Derived.Lemmas
+open MLS.Symbolic
+open MLS.Result
+
+#push-options "--fuel 0 --ifuel 0"
+
+(*** Split predicate for SignWithLabel ***)
+
+noeq
+type signwithlabel_crypto_pred {|crypto_usages|} = {
+  pred: trace -> vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes -> prop;
+  pred_later:
+    tr1:trace -> tr2:trace ->
+    vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes ->
+    Lemma
+    (requires pred tr1 vk msg /\ tr1 <$ tr2)
+    (ensures pred tr2 vk msg)
+  ;
+}
+
+let split_signwithlabel_crypto_pred_params {|crypto_usages|}: split_function_parameters = {
+  tag_set_t = valid_label;
+  tag_t = mls_ascii_string;
+  is_disjoint = unequal;
+  tag_belong_to = (fun tag tag_set ->
+    tag = get_mls_label tag_set
+  );
+  cant_belong_to_disjoint_sets = (fun tag tag_set_1 tag_set_2 ->
+    FStar.Classical.move_requires_2 get_mls_label_inj tag_set_1 tag_set_2
+  );
+
+  tagged_data_t = (trace & (vk:bytes{SigKey? (get_signkey_usage vk)}) & bytes);
+  raw_data_t = (trace & (vk:bytes{SigKey? (get_signkey_usage vk)}) & bytes);
+  output_t = prop;
+
+  decode_tagged_data = (fun (tr, vk, data) -> (
+    match parse (sign_content_nt bytes) data with
+    | Some ({label; content}) -> Some (label, (tr, vk, content))
+    | None -> None
+  ));
+
+  local_fun_t = signwithlabel_crypto_pred;
+  global_fun_t = trace -> vk:bytes{SigKey? (get_signkey_usage vk)} -> bytes -> prop;
+
+  default_global_fun = (fun tr vk content -> False);
+
+
+  apply_local_fun = (fun pred (tr, vk, content) -> pred.pred tr vk content);
+  apply_global_fun = (fun pred (tr, vk, msg) -> pred tr vk msg);
+  mk_global_fun = (fun pred tr vk msg -> pred (tr, vk, msg));
+  apply_mk_global_fun = (fun _ _ -> ());
+}
+
+#push-options "--ifuel 1"
+val has_signwithlabel_pred: {|cusgs:crypto_usages|} -> sign_crypto_predicate cusgs -> (valid_label & signwithlabel_crypto_pred) -> prop
+let has_signwithlabel_pred #cusgs sign_pred (lab, local_pred) =
+  forall tr vk msg.
+    {:pattern sign_pred.pred tr vk msg}
+    match parse (sign_content_nt bytes) msg with
+    | Some {label; content} -> (
+      label == get_mls_label lab ==> (
+        sign_pred.pred tr vk msg ==
+        local_pred.pred tr vk content
+      )
+    )
+    | _ -> True
+#pop-options
+
+val intro_has_signwithlabel_pred:
+  {|cusgs:crypto_usages|} ->
+  sign_pred:sign_crypto_predicate cusgs -> tagged_local_pred:(valid_label & signwithlabel_crypto_pred) ->
+  Lemma
+  (requires has_local_fun split_signwithlabel_crypto_pred_params sign_pred.pred tagged_local_pred)
+  (ensures has_signwithlabel_pred sign_pred tagged_local_pred)
+let intro_has_signwithlabel_pred #cusgs sign_pred (tag, local_pred) =
+  introduce
+    forall tr vk msg.
+      match parse (sign_content_nt bytes) msg with
+      | Some {label; content} -> (
+        label == get_mls_label tag ==> (
+          sign_pred.pred tr vk msg ==
+          local_pred.pred tr vk content
+        )
+      )
+      | _ -> True
+  with (
+    has_local_fun_elim split_signwithlabel_crypto_pred_params sign_pred.pred tag local_pred (tr, vk, msg)
+  )
+
+val mk_global_mls_sign_pred:
+  {|crypto_usages|} ->
+  list (valid_label & signwithlabel_crypto_pred) ->
+  trace -> vk:bytes{SigKey? (get_signkey_usage vk)} -> bytes ->
+  prop
+let mk_global_mls_sign_pred tagged_local_preds vk msg =
+  mk_global_fun split_signwithlabel_crypto_pred_params tagged_local_preds vk msg
+
+#push-options "--ifuel 2"
+val mk_global_mls_sign_pred_later:
+  {|crypto_usages|} ->
+  tagged_local_preds:list (valid_label & signwithlabel_crypto_pred) ->
+  tr1:trace -> tr2:trace ->
+  vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes ->
+  Lemma
+  (requires
+    mk_global_mls_sign_pred tagged_local_preds tr1 vk msg /\
+    tr1 <$ tr2
+  )
+  (ensures mk_global_mls_sign_pred tagged_local_preds tr2 vk msg)
+let mk_global_mls_sign_pred_later tagged_local_preds tr1 tr2 vk msg =
+  mk_global_fun_eq split_signwithlabel_crypto_pred_params tagged_local_preds (tr1, vk, msg);
+  mk_global_fun_eq split_signwithlabel_crypto_pred_params tagged_local_preds (tr2, vk, msg);
+  introduce forall lpred content. split_signwithlabel_crypto_pred_params.apply_local_fun lpred (tr1, vk, content) ==> split_signwithlabel_crypto_pred_params.apply_local_fun lpred (tr2, vk, content) with (
+    introduce _ ==> _ with _. lpred.pred_later tr1 tr2 vk content
+  )
+#pop-options
+
+val mk_mls_sign_pred:
+  {|cusgs:crypto_usages|} ->
+  list (valid_label & signwithlabel_crypto_pred) ->
+  sign_crypto_predicate cusgs
+let mk_mls_sign_pred #cusgs tagged_local_preds = {
+  pred = mk_global_mls_sign_pred tagged_local_preds;
+  pred_later = mk_global_mls_sign_pred_later tagged_local_preds;
+}
+
+#push-options "--ifuel 1"
+val mk_mls_sign_pred_correct:
+  {|cusgs:crypto_usages|} ->
+  sign_pred:sign_crypto_predicate cusgs -> tagged_local_preds:list (valid_label & signwithlabel_crypto_pred) ->
+  Lemma
+  (requires
+    sign_pred == mk_mls_sign_pred tagged_local_preds /\
+    List.Tot.no_repeats_p (List.Tot.map fst tagged_local_preds)
+  )
+  (ensures for_allP (has_signwithlabel_pred sign_pred) tagged_local_preds)
+let mk_mls_sign_pred_correct sign_pred tagged_local_preds =
+  for_allP_eq (has_signwithlabel_pred sign_pred) tagged_local_preds;
+  no_repeats_p_implies_for_all_pairsP_unequal (List.Tot.map fst tagged_local_preds);
+  FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_signwithlabel_crypto_pred_params tagged_local_preds));
+  FStar.Classical.forall_intro (FStar.Classical.move_requires (intro_has_signwithlabel_pred sign_pred))
+#pop-options
+
+(*** ***)
+
+val has_mls_signwithlabel_pred: {|crypto_invariants|} -> (valid_label & signwithlabel_crypto_pred) -> prop
+let has_mls_signwithlabel_pred #cinvs tagged_local_pred =
+  exists mls_sign_pred.
+    has_sign_predicate cinvs ("MLS.LeafSignKey", mls_sign_pred) /\
+    has_signwithlabel_pred mls_sign_pred tagged_local_pred
+
+(*** Lemmas on SignWithLabel and VerifyWithLabel ***)
+
+val bytes_invariant_sign_with_label:
+  {|crypto_invariants|} -> spred:signwithlabel_crypto_pred -> tr:trace ->
+  sk:bytes -> lab:valid_label -> msg:mls_bytes bytes -> nonce:sign_nonce bytes ->
+  Lemma
+  (requires
+    bytes_invariant tr sk /\
+    bytes_invariant tr nonce /\
+    bytes_invariant tr msg /\
+    get_usage sk == SigKey "MLS.LeafSignKey" empty /\
+    SigNonce? (get_usage nonce) /\
+    (get_label sk) `can_flow tr` (get_label nonce) /\
+    spred.pred tr (vk sk) msg /\
+    has_mls_signwithlabel_pred (lab, spred)
+  )
+  (ensures
+    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 bytes_invariant_sign_with_label #ci spred tr sk lab msg nonce =
+  let sign_content: sign_content_nt bytes = {
+    label = get_mls_label lab;
+    content = msg;
+  } in
+  serialize_wf_lemma (sign_content_nt bytes) (bytes_invariant tr) sign_content;
+  serialize_wf_lemma (sign_content_nt bytes) (is_knowable_by (get_label msg) tr) sign_content
+
+val bytes_invariant_verify_with_label:
+  {|ci:crypto_invariants|} -> spred:signwithlabel_crypto_pred -> tr:trace ->
+  vk:bytes -> lab:valid_label -> content:mls_bytes bytes -> signature:bytes ->
+  Lemma
+  (requires
+    bytes_invariant tr vk /\
+    bytes_invariant tr content /\
+    bytes_invariant tr signature /\
+    verify_with_label vk lab content signature /\
+    has_mls_signwithlabel_pred (lab, spred)
+  )
+  (ensures
+    (
+      get_signkey_usage vk == SigKey "MLS.LeafSignKey" empty ==>
+      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 bytes = {
+    label = get_mls_label lab;
+    content = content;
+  } in
+  serialize_wf_lemma (sign_content_nt bytes) (bytes_invariant tr) sign_content
diff --git a/fstar/symbolic/MLS.Symbolic.fst b/fstar/symbolic/MLS.Symbolic.fst
index 7df814a..e8334d8 100644
--- a/fstar/symbolic/MLS.Symbolic.fst
+++ b/fstar/symbolic/MLS.Symbolic.fst
@@ -3,8 +3,6 @@ module MLS.Symbolic
 open Comparse
 open DY.Core
 open MLS.Crypto
-open MLS.NetworkTypes
-open DY.Lib.SplitFunction
 open MLS.Result
 
 #push-options "--fuel 0 --ifuel 0"
@@ -99,171 +97,3 @@ let dy_bytes_has_crypto acs = {
 #pop-options
 
 instance crypto_dy_bytes: crypto_bytes dy_bytes = dy_bytes_has_crypto AC_mls_128_dhkemx25519_chacha20poly1305_sha256_ed25519
-
-(*** Labeled signature predicate ***)
-
-val get_mls_label_inj:
-  l1:valid_label -> l2:valid_label ->
-  Lemma
-  (requires get_mls_label l1 == get_mls_label l2)
-  (ensures l1 == l2)
-let get_mls_label_inj l1 l2 =
-  String.concat_injective "MLS 1.0 " "MLS 1.0 " l1 l2
-
-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)
-  ;
-}
-
-let split_sign_pred_params {|crypto_usages|}: split_function_parameters = {
-  tag_set_t = valid_label;
-  tag_t = mls_ascii_string;
-  is_disjoint = unequal;
-  tag_belong_to = (fun tag tag_set ->
-    tag = get_mls_label tag_set
-  );
-  cant_belong_to_disjoint_sets = (fun tag tag_set_1 tag_set_2 ->
-    FStar.Classical.move_requires_2 get_mls_label_inj tag_set_1 tag_set_2
-  );
-
-  tagged_data_t = (trace & verif_key_t & dy_bytes);
-  raw_data_t = (trace & verif_key_t & dy_bytes);
-  output_t = prop;
-
-  decode_tagged_data = (fun (tr, key, data) -> (
-    match parse (sign_content_nt dy_bytes) data with
-    | Some ({label; content}) -> Some (label, (tr, key, content))
-    | None -> None
-  ));
-
-  local_fun_t = mls_sign_pred;
-  global_fun_t = trace -> verif_key_t -> dy_bytes -> prop;
-
-  default_global_fun = (fun tr vk content -> False);
-
-
-  apply_local_fun = (fun pred (tr, vk, content) -> pred.pred tr vk content);
-  apply_global_fun = (fun pred (tr, vk, msg) -> pred tr vk msg);
-  mk_global_fun = (fun pred tr vk msg -> pred (tr, vk, msg));
-  apply_mk_global_fun = (fun _ _ -> ());
-}
-
-val has_sign_pred: crypto_invariants -> (valid_label & mls_sign_pred) -> prop
-let has_sign_pred ci (lab, spred) =
-  has_local_fun split_sign_pred_params ((sign_pred #ci).pred) (lab, spred)
-
-#push-options "--z3rlimit 25"
-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
-    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
-    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 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) (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_params.decode_tagged_data (tr, (vk sk), sign_content_bytes) == Some (get_mls_label lab, (tr, (vk sk), msg)))
-#pop-options
-
-val bytes_invariant_verify_with_label:
-  {|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 ci (lab, spred) /\
-    bytes_invariant tr vk /\
-    bytes_invariant tr content /\
-    bytes_invariant tr signature /\
-    verify_with_label vk lab content signature
-  )
-  (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) (bytes_invariant tr) sign_content;
-  let sign_content_bytes = serialize _ sign_content in
-  if SigKey? (get_signkey_usage vk) then
-    assert(split_sign_pred_params.decode_tagged_data (tr, vk, sign_content_bytes) == Some (get_mls_label lab, (tr, vk, content)))
-  else ()
-
-val mk_sign_pred:
-  {|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_fun split_sign_pred_params 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
-    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_fun_eq split_sign_pred_params lspred (tr1, vk, msg);
-  mk_global_fun_eq split_sign_pred_params lspred (tr2, vk, msg);
-
-  introduce forall lpred content. split_sign_pred_params.apply_local_fun lpred (tr1, vk, content) ==> split_sign_pred_params.apply_local_fun lpred (tr2, vk, content) with (
-    introduce _ ==> _ with _. lpred.pred_later tr1 tr2 vk content
-  );
-  match parse (sign_content_nt dy_bytes) msg with
-  | Some _ -> ()
-  | None -> ()
-#pop-options
-
-#push-options "--ifuel 1"
-val mk_sign_pred_correct:
-  ci:crypto_invariants -> lspred:list (valid_label & mls_sign_pred) ->
-  Lemma
-  (requires
-    sign_pred.pred == mk_sign_pred lspred /\
-    List.Tot.no_repeats_p (List.Tot.map fst lspred)
-  )
-  (ensures for_allP (has_sign_pred ci) lspred)
-let mk_sign_pred_correct ci lspred =
-  for_allP_eq (has_sign_pred ci) lspred;
-  no_repeats_p_implies_for_all_pairsP_unequal (List.Tot.map fst lspred);
-  FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_sign_pred_params lspred))
-#pop-options
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
index a839b40..78ab9d4 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
@@ -6,11 +6,13 @@ open DY.Lib
 open MLS.Crypto
 open MLS.TreeSync.NetworkTypes
 open MLS.Symbolic
+open MLS.Crypto.Derived.Symbolic.SignWithLabel
 open MLS.TreeSync.Symbolic.LeafNodeSignature
 open MLS.TreeSync.Symbolic.AuthServiceCache
 open MLS.TreeSync.Symbolic.API.Sessions
 open MLS.TreeSync.Symbolic.API.GroupManager
 open MLS.TreeSync.Symbolic.API.KeyPackageManager
+open MLS.TreeSync.Symbolic.API
 
 #set-options "--fuel 0 --ifuel 0"
 
@@ -19,20 +21,24 @@ open MLS.TreeSync.Symbolic.API.KeyPackageManager
 instance treesync_crypto_usages: crypto_usages =
   default_crypto_usages
 
-val all_sign_preds: treekem_types dy_bytes -> list (valid_label & mls_sign_pred)
-let all_sign_preds tkt = [
+val all_signwithlabel_preds: treekem_types dy_bytes -> list (valid_label & signwithlabel_crypto_pred)
+let all_signwithlabel_preds tkt = [
   leaf_node_tbs_tag_and_invariant tkt;
 ]
 
+val mls_sign_pred: treekem_types dy_bytes -> sign_crypto_predicate treesync_crypto_usages
+let mls_sign_pred tkt =
+  mk_mls_sign_pred (all_signwithlabel_preds tkt)
+
+val all_sign_preds: treekem_types dy_bytes -> list (string & sign_crypto_predicate treesync_crypto_usages)
+let all_sign_preds tkt = [
+  ("MLS.LeafSignKey", mls_sign_pred tkt)
+]
+
 val treesync_crypto_predicates: treekem_types dy_bytes -> crypto_predicates treesync_crypto_usages
 let treesync_crypto_predicates tkt = {
   default_crypto_predicates treesync_crypto_usages with
-  sign_pred = {
-    pred = mk_sign_pred (all_sign_preds tkt);
-    pred_later = (fun tr1 tr2 vk msg ->
-      mk_sign_pred_later (all_sign_preds tkt) tr1 tr2 vk msg
-    );
-  }
+  sign_pred = mk_sign_predicate (all_sign_preds tkt);
 }
 
 instance treesync_crypto_invariants (tkt:treekem_types dy_bytes): crypto_invariants = {
@@ -63,19 +69,21 @@ let treesync_protocol_invariants tkt = {
 
 (*** Proofs ***)
 
-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)))
+#push-options "--ifuel 1 --fuel 1"
+val all_signwithlabel_preds_has_all_signwithlabel_preds: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_signwithlabel_preds; `%for_allP]; iota; zeta] (for_allP (has_signwithlabel_pred (mls_sign_pred tkt)) (all_signwithlabel_preds tkt)))
+let all_signwithlabel_preds_has_all_signwithlabel_preds tkt =
+  assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_signwithlabel_preds tkt)));
+  mk_mls_sign_pred_correct (mls_sign_pred tkt) (all_signwithlabel_preds tkt);
+  norm_spec [delta_only [`%all_signwithlabel_preds; `%for_allP]; iota; zeta] (for_allP (has_signwithlabel_pred (mls_sign_pred tkt)) (all_signwithlabel_preds tkt))
+#pop-options
+
+#push-options "--ifuel 1 --fuel 1"
+val all_sign_preds_has_all_sign_preds: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP (has_sign_predicate (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_crypto_invariants tkt))
-  [SMTPat (has_leaf_node_tbs_invariant tkt (treesync_crypto_invariants tkt))]
-let treesync_global_usage_has_leaf_node_tbs_invariant tkt =
-  all_sign_preds_has_all_sign_preds tkt
+  mk_sign_predicate_correct (treesync_crypto_invariants tkt) (all_sign_preds tkt);
+  norm_spec [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP (has_sign_predicate (treesync_crypto_invariants tkt)) (all_sign_preds tkt))
+#pop-options
 
 val all_state_predicates_has_all_state_predicates: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate (treesync_protocol_invariants tkt)) (all_state_predicates tkt)))
 let all_state_predicates_has_all_state_predicates tkt =
@@ -83,32 +91,10 @@ let all_state_predicates_has_all_state_predicates tkt =
   mk_state_pred_correct (treesync_protocol_invariants tkt) (all_state_predicates tkt);
   norm_spec [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate (treesync_protocol_invariants tkt)) (all_state_predicates tkt))
 
-val treesync_protocol_invariants_has_as_cache_invariant: tkt:treekem_types dy_bytes -> Lemma
-  (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 =
+val treesync_protocol_invariants_has_has_treesync_invariants: tkt:treekem_types dy_bytes -> Lemma
+  (has_treesync_invariants tkt (treesync_protocol_invariants tkt))
+  [SMTPat (has_treesync_invariants tkt (treesync_protocol_invariants tkt))]
+let treesync_protocol_invariants_has_has_treesync_invariants tkt =
+  all_signwithlabel_preds_has_all_signwithlabel_preds tkt;
+  all_sign_preds_has_all_sign_preds tkt;
   all_state_predicates_has_all_state_predicates tkt
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
index fbba620..5c5d86d 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
@@ -21,6 +21,7 @@ open MLS.TreeSync.Proofs.ParentHashGuarantees
 open MLS.TreeSync.API.Types
 open MLS.TreeSync.Symbolic.IsWellFormed
 open MLS.TreeSync.Symbolic.Parsers
+open MLS.Crypto.Derived.Symbolic.SignWithLabel
 open MLS.Symbolic
 open MLS.Result
 
@@ -134,7 +135,7 @@ let leaf_node_label = "LeafNodeTBS"
 #push-options "--fuel 0 --z3rlimit 25"
 val leaf_node_sign_pred:
   {|crypto_usages|} -> treekem_types dy_bytes ->
-  mls_sign_pred
+  signwithlabel_crypto_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
@@ -169,14 +170,14 @@ let leaf_node_sign_pred #cu tkt = {
 }
 #pop-options
 
+val leaf_node_tbs_tag_and_invariant: {|crypto_usages|} -> treekem_types dy_bytes -> (valid_label & signwithlabel_crypto_pred)
+let leaf_node_tbs_tag_and_invariant #cu tkt = (leaf_node_label, leaf_node_sign_pred tkt)
+
 val has_leaf_node_tbs_invariant:
   treekem_types dy_bytes -> crypto_invariants ->
   prop
 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)
+  has_mls_signwithlabel_pred (leaf_node_tbs_tag_and_invariant tkt)
 
 (*** Proof of verification, for a tree ***)