Merge branch 'refactor' into revised_api_please_rebase_before_merging

fstar/api/MLS.fst

@@ -257,7 +257,7 @@ let process_commit state wire_format message message_auth =
   let state = { state with confirmed_transcript_hash; interim_transcript_hash } in
   // 4. Check confirmation tag
   let? () = (
-    let confirmation_key = state.treekem_state.keyschedule_state.epoch_keys.confirmation_key in
+    let confirmation_key = (MLS.TreeKEM.API.get_epoch_keys state.treekem_state).confirmation_key in
     let? confirmation_tag_ok = MLS.TreeDEM.API.verify_confirmation_tag state.treedem_state full_message confirmation_key confirmed_transcript_hash in
     if not confirmation_tag_ok then
       error "process_commit: invalid confirmation tag"
@@ -276,8 +276,8 @@ let process_commit state wire_format message message_auth =
     my_leaf_index;
     group_context;
     encryption_secret;
-    sender_data_secret = state.treekem_state.keyschedule_state.epoch_keys.sender_data_secret;
-    membership_key = state.treekem_state.keyschedule_state.epoch_keys.membership_key;
+    sender_data_secret = (MLS.TreeKEM.API.get_epoch_keys state.treekem_state).sender_data_secret;
+    membership_key = (MLS.TreeKEM.API.get_epoch_keys state.treekem_state).membership_key;
     my_signature_key = state.sign_private_key;
     verification_keys = get_verification_keys state.treesync_state.tree;
   } in
@@ -392,8 +392,8 @@ let create e cred private_sign_key group_id =
     my_leaf_index = leaf_index;
     group_context;
     encryption_secret;
-    sender_data_secret = treekem_state.keyschedule_state.epoch_keys.sender_data_secret;
-    membership_key = treekem_state.keyschedule_state.epoch_keys.membership_key;
+    sender_data_secret = (MLS.TreeKEM.API.get_epoch_keys treekem_state).sender_data_secret;
+    membership_key = (MLS.TreeKEM.API.get_epoch_keys treekem_state).membership_key;
     my_signature_key = private_sign_key;
     verification_keys = get_verification_keys treesync_state.tree;
   } in
@@ -577,7 +577,7 @@ let generate_commit state e proposals =
   let new_group_context = { provisional_group_context with confirmed_transcript_hash } in
   let? commit_result = MLS.TreeKEM.API.finalize_create_commit pending_commit new_group_context None in
   let state = { state with pending_updatepath = (update_path, (commit_result.new_state, commit_result.encryption_secret))::state.pending_updatepath } in
-  let? auth_commit = MLS.TreeDEM.API.finish_authenticate_commit half_auth_commit commit_result.new_state.keyschedule_state.epoch_keys.confirmation_key confirmed_transcript_hash in
+  let? auth_commit = MLS.TreeDEM.API.finish_authenticate_commit half_auth_commit (MLS.TreeKEM.API.get_epoch_keys commit_result.new_state).confirmation_key confirmed_transcript_hash in
   let? reuse_guard, e = chop_entropy e 4 in
   assume(Seq.length reuse_guard == length #bytes reuse_guard);
   let? (commit_ct, new_treedem_state) = MLS.TreeDEM.API.protect_private state.treedem_state auth_commit reuse_guard in
@@ -681,15 +681,10 @@ let process_welcome_message w (sign_pk, sign_sk) lookup =
   let treesync = treesync_state.tree in
   let l = treesync_state.levels in
   let? _ = ( //Check signature
-    let? group_info_ok = verify_welcome_group_info (fun leaf_ind ->
-      if not (leaf_ind < pow2 l) then
-        error "process_welcome_message: leaf_ind too big"
-      else (
-        let? sender_leaf_package = from_option "process_welcome_message: signer leaf is blanked (1)" (leaf_at treesync leaf_ind) in
-        return (sender_leaf_package.data.signature_key <: bytes)
-      )
-    ) group_info in
-    return ()
+    let? signer_verification_key = get_signer_verification_key treesync group_info in
+    if not (verify_welcome_group_info signer_verification_key group_info) then
+      error "process_welcome_message: bad GroupInfo signature"
+    else return ()
   ) in
   let? leaf_index = find_my_index treesync sign_pk in
   let opt_path_secret_and_inviter_ind: option (bytes & nat) = match secrets.path_secret with | None -> None | Some {path_secret} -> Some (path_secret, group_info.tbs.signer) in
@@ -708,7 +703,7 @@ let process_welcome_message w (sign_pk, sign_sk) lookup =
   let? group_context = compute_group_context group_id epoch tree_hash confirmed_transcript_hash in
 
   let? () = (
-    let? computed_confirmation_tag = MLS.TreeDEM.Message.Framing.compute_message_confirmation_tag treekem_state.keyschedule_state.epoch_keys.confirmation_key confirmed_transcript_hash in
+    let? computed_confirmation_tag = MLS.TreeDEM.Message.Framing.compute_message_confirmation_tag (MLS.TreeKEM.API.get_epoch_keys treekem_state).confirmation_key confirmed_transcript_hash in
     if not ((group_info.tbs.confirmation_tag <: bytes) = (computed_confirmation_tag <: bytes)) then
       error "process_welcome_message: bad confirmation_tag"
     else return ()
@@ -719,8 +714,8 @@ let process_welcome_message w (sign_pk, sign_sk) lookup =
     my_leaf_index = leaf_index;
     group_context;
     encryption_secret;
-    sender_data_secret = treekem_state.keyschedule_state.epoch_keys.sender_data_secret;
-    membership_key = treekem_state.keyschedule_state.epoch_keys.membership_key;
+    sender_data_secret = (MLS.TreeKEM.API.get_epoch_keys treekem_state).sender_data_secret;
+    membership_key = (MLS.TreeKEM.API.get_epoch_keys treekem_state).membership_key;
     my_signature_key = sign_sk;
     verification_keys = get_verification_keys treesync_state.tree;
   } in

fstar/bootstrap/MLS.Bootstrap.Welcome.fst

@@ -3,6 +3,7 @@ module MLS.Bootstrap.Welcome
 open Comparse
 open MLS.NetworkTypes
 open MLS.TreeSync.NetworkTypes
+open MLS.TreeSync.Types
 open MLS.TreeKEM.NetworkTypes
 open MLS.Bootstrap.NetworkTypes
 open MLS.Bootstrap.KeyPackageRef
@@ -164,11 +165,25 @@ let sign_welcome_group_info #bytes #cb sign_sk gi_tbs rand =
   let? signature = mk_mls_bytes signature "sign_welcome_group_info" "signature" in
   return ({tbs = gi_tbs; signature;})
 
+val get_signer_verification_key:
+  #bytes:Type0 -> {|bytes_like bytes|} -> #tkt:treekem_types bytes ->
+  #l:nat ->
+  treesync bytes tkt l 0 ->
+  group_info_nt bytes ->
+  result bytes
+let get_signer_verification_key #bytes #bl #tkt #l t group_info =
+  if not (group_info.tbs.signer < pow2 l) then
+    error "get_signer_verification_key: signer too big"
+  else (
+    match leaf_at t group_info.tbs.signer with
+    | None -> error "get_signer_verification_key: signer is a blank leaf"
+    | Some ln -> return ln.data.signature_key
+  )
+
 val verify_welcome_group_info:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
-  (nat -> result (verif_key:bytes)) -> group_info_nt bytes ->
-  result bool
-let verify_welcome_group_info #bytes #cb get_sign_pk gi =
-  let? sign_pk = get_sign_pk gi.tbs.signer in
+  bytes -> group_info_nt bytes ->
+  bool
+let verify_welcome_group_info #bytes #cb sign_pk gi =
   let tbs_bytes: bytes = serialize (group_info_tbs_nt bytes) gi.tbs in
-  return (verify_with_label sign_pk "GroupInfoTBS" tbs_bytes gi.signature)
+  verify_with_label sign_pk "GroupInfoTBS" tbs_bytes gi.signature

fstar/test/MLS.Test.FromExt.Welcome.fst

@@ -50,7 +50,7 @@ let test_welcome_one t =
 
     let (group_info, group_secrets, (_, my_init_decryption_key)) = extract_result (decrypt_welcome welcome (fun ref -> if ref = kp_ref then Some init_priv else None) (fun x -> return x)) in
 
-    if not (extract_result (verify_welcome_group_info (fun _ -> return signer_pub) group_info)) then (
+    if not (verify_welcome_group_info signer_pub group_info) then (
       failwith "test_welcome_one: bad signature"
     );
 

fstar/treedem/MLS.TreeDEM.NetworkTypes.fst

@@ -109,6 +109,8 @@ type proposal_nt (bytes:Type0) {|bytes_like bytes|} =
 
 %splice [ps_proposal_nt] (gen_parser (`proposal_nt))
 
+instance parseable_serializeable_proposal_nt (bytes:Type0) {|bytes_like bytes|}: parseable_serializeable bytes (proposal_nt bytes) = mk_parseable_serializeable ps_proposal_nt
+
 /// enum {
 ///   reserved(0),
 ///   proposal(1),

fstar/treekem/code/MLS.TreeKEM.API.KeySchedule.fst

@@ -55,3 +55,11 @@ let commit #bytes #cb st opt_commit_secret opt_psk new_group_context =
     joiner_secret;
     welcome_secret;
   })
+
+val export:
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  treekem_keyschedule_state bytes ->
+  valid_label -> bytes -> len:nat ->
+  result (lbytes bytes len)
+let export #bytes #cb st label context len =
+  mls_exporter st.epoch_keys.exporter_secret label context len

fstar/treekem/code/MLS.TreeKEM.API.fst

@@ -187,3 +187,20 @@ let finalize_create_commit #bytes #cb #leaf_ind pending new_group_context opt_ps
     welcome_secret = additional_secrets.welcome_secret;
     joiner_secret = additional_secrets.joiner_secret;
   }
+
+(*** Getters ***)
+
+val get_epoch_keys:
+  #bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat ->
+  treekem_state bytes leaf_ind ->
+  epoch_keys bytes
+let get_epoch_keys #bytes #cb #leaf_ind st =
+  st.keyschedule_state.epoch_keys
+
+val export:
+  #bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat ->
+  treekem_state bytes leaf_ind ->
+  valid_label -> bytes -> len:nat ->
+  result (lbytes bytes len)
+let export #bytes #cb st label context len =
+  KS.export st.keyschedule_state label context len