cleanup: move confirmation tag where it belongs

fstar/api/MLS.fst

@@ -254,8 +254,8 @@ 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 = (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
+    let confirmation_tag = (MLS.TreeKEM.API.get_epoch_keys state.treekem_state).confirmation_tag in
+    let? confirmation_tag_ok = MLS.TreeDEM.API.verify_confirmation_tag state.treedem_state full_message confirmation_tag in
     if not confirmation_tag_ok then
       error "process_commit: invalid confirmation tag"
     else return ()
@@ -372,17 +372,17 @@ let create e cred private_sign_key group_id =
     //TODO AS check
     return (MLS.TreeSync.API.finalize_create create_pend ())
   ) in
+  let? tree_hash = MLS.TreeSync.API.compute_tree_hash treesync_state in
+  let epoch = 0 in
+  let confirmed_transcript_hash = Seq.empty in
+  let? group_context = compute_group_context group_id epoch tree_hash confirmed_transcript_hash in
   let treekem = treesync_to_treekem treesync_state.tree in
   // 10. In principle, the above process could be streamlined by having the
   // creator directly create a tree and choose a random value for first epoch's
   // epoch secret.
   let? epoch_secret, e = chop_entropy e 32 in
-  let? (treekem_state, encryption_secret) = MLS.TreeKEM.API.create leaf_decryption_key key_package.tbs.leaf_node.data.content epoch_secret in
+  let? (treekem_state, encryption_secret) = MLS.TreeKEM.API.create leaf_decryption_key key_package.tbs.leaf_node.data.content epoch_secret group_context in
 
-  let? tree_hash = MLS.TreeSync.API.compute_tree_hash treesync_state in
-  let epoch = 0 in
-  let confirmed_transcript_hash = Seq.empty in
-  let? group_context = compute_group_context group_id epoch tree_hash confirmed_transcript_hash in
   let leaf_index = 0 in
   let? treedem_state = MLS.TreeDEM.API.init {
     tree_height = 0;
@@ -574,7 +574,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 [] 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 (MLS.TreeKEM.API.get_epoch_keys commit_result.new_state).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_tag 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
@@ -704,8 +704,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 (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
+    if not ((group_info.tbs.confirmation_tag <: bytes) = (MLS.TreeKEM.API.get_epoch_keys treekem_state).confirmation_tag) then
       error "process_welcome_message: bad confirmation_tag"
     else return ()
   ) in

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

@@ -13,6 +13,7 @@ open MLS.Crypto
 open MLS.TreeDEM.NetworkTypes
 open MLS.TreeDEM.Message.Transcript
 open MLS.TreeDEM.Message.Framing
+open MLS.TreeKEM.KeySchedule
 
 val test_transcript_hashes_one: transcript_hashes_test -> ML bool
 let test_transcript_hashes_one t =
@@ -33,16 +34,16 @@ let test_transcript_hashes_one t =
       let confirmation_key = hex_string_to_bytes t.confirmation_key in
       let interim_transcript_hash_before = hex_string_to_bytes t.interim_transcript_hash_before in
       let confirmed_transcript_hash_after = extract_result (compute_confirmed_transcript_hash authenticated_content.wire_format authenticated_content.content authenticated_content.auth.signature interim_transcript_hash_before) in
-      let confirmation_tag = extract_result (compute_message_confirmation_tag confirmation_key confirmed_transcript_hash_after) in
+      let confirmation_tag = extract_result (compute_confirmation_tag confirmation_key confirmed_transcript_hash_after) in
       let interim_transcript_hash_after = extract_result (compute_interim_transcript_hash #bytes authenticated_content.auth.confirmation_tag confirmed_transcript_hash_after) in
       check_equal "confirmed_transcript_hash_after" (bytes_to_hex_string) (hex_string_to_bytes t.confirmed_transcript_hash_after) (confirmed_transcript_hash_after);
       check_equal "interim_transcript_hash_after" (bytes_to_hex_string) (hex_string_to_bytes t.interim_transcript_hash_after) (interim_transcript_hash_after);
 
       if not (authenticated_content.content.content.content_type = CT_commit) then
         failwith "test_transcript_hashes_one: not a commit"
-      else if not (extract_result (check_authenticated_content_confirmation_tag authenticated_content confirmation_key confirmed_transcript_hash_after)) then
-        failwith "test_transcript_hashes_one: bad confirmation_tag"
-      ;
+      else (
+        check_equal "confirmation_tag" (bytes_to_hex_string) (authenticated_content.auth.confirmation_tag) (confirmation_tag)
+      );
       true
     )
   end

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

@@ -58,7 +58,7 @@ let test_welcome_one t =
     let joiner_secret = group_secrets.joiner_secret in
     let epoch_secret = extract_result (secret_joiner_to_epoch joiner_secret [] group_context) in
     let confirmation_key = extract_result (secret_epoch_to_confirmation #bytes epoch_secret) in
-    let confirmation_tag = extract_result (compute_message_confirmation_tag #bytes confirmation_key group_info.tbs.group_context.confirmed_transcript_hash) in
+    let confirmation_tag = extract_result (compute_confirmation_tag #bytes confirmation_key group_info.tbs.group_context.confirmed_transcript_hash) in
     check_equal "confirmation_tag" (bytes_to_hex_string) (group_info.tbs.confirmation_tag) (confirmation_tag);
     true
   end

fstar/treedem/MLS.TreeDEM.API.fst

@@ -101,19 +101,20 @@ let start_authenticate_commit #bytes #cb st wf msg nonce =
 val finish_authenticate_commit:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
   msg:half_authenticated_commit bytes ->
-  bytes -> bytes ->
+  bytes ->
   result (res:authenticated_content_nt bytes{res.wire_format == msg.wire_format /\ res.content == msg.content})
-let finish_authenticate_commit #bytes #cb msg confirmation_key confirmed_transcript_hash  =
-  let? confirmation_tag = compute_message_confirmation_tag confirmation_key confirmed_transcript_hash in
-  let? confirmation_tag = mk_mls_bytes (confirmation_tag <: bytes) "finish_authenticate_commit" "confirmation_tag" in
-  return ({
-    wire_format = msg.wire_format;
-    content = msg.content;
-    auth = {
-      signature = msg.signature;
-      confirmation_tag;
-    }
-  } <: res:authenticated_content_nt bytes{res.wire_format == msg.wire_format /\ res.content == msg.content})
+let finish_authenticate_commit #bytes #cb msg confirmation_tag  =
+  if not (length confirmation_tag < pow2 30) then error "finish_authenticate_commit: confirmation_tag too long"
+  else (
+    return ({
+      wire_format = msg.wire_format;
+      content = msg.content;
+      auth = {
+        signature = msg.signature;
+        confirmation_tag;
+      }
+    } <: res:authenticated_content_nt bytes{res.wire_format == msg.wire_format /\ res.content == msg.content})
+  )
 
 /// Functions to verify the authentication.
 
@@ -142,12 +143,13 @@ val verify_confirmation_tag:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
   treedem_state bytes ->
   authenticated_content_nt bytes ->
-  bytes -> bytes ->
+  bytes ->
   result bool
-let verify_confirmation_tag #bytes #cb st msg confirmation_key confirmed_transcript_hash =
+let verify_confirmation_tag #bytes #cb st msg confirmation_tag =
+  bytes_hasEq #bytes;
   match msg.content.content.content_type with
   | CT_commit ->
-    check_authenticated_content_confirmation_tag msg confirmation_key confirmed_transcript_hash
+    return (msg.auth.confirmation_tag = confirmation_tag)
   | _ -> internal_failure "verify_confirmation_tag: not a commit"
 
 (*** Protection ***)

fstar/treedem/MLS.TreeDEM.Message.Framing.fst

@@ -9,13 +9,6 @@ open MLS.Result
 
 (*** Authentication ***)
 
-val compute_message_confirmation_tag:
-  #bytes:Type0 -> {|crypto_bytes bytes|} ->
-  bytes -> bytes ->
-  result (lbytes bytes (hmac_length #bytes))
-let compute_message_confirmation_tag #bytes #cb confirmation_key confirmed_transcript_hash =
-  hmac_hmac confirmation_key confirmed_transcript_hash
-
 val knows_group_context:
   #bytes:Type0 -> {|bytes_like bytes|} ->
   sender_nt bytes ->
@@ -82,14 +75,6 @@ val check_authenticated_content_signature:
 let check_authenticated_content_signature #bytes #cb msg vk group_context =
   check_message_signature vk msg.auth.signature msg.wire_format msg.content group_context
 
-val check_authenticated_content_confirmation_tag:
-  #bytes:Type0 -> {|crypto_bytes bytes|} ->
-  msg:authenticated_content_nt bytes{msg.content.content.content_type == CT_commit} -> bytes -> bytes ->
-  result bool
-let check_authenticated_content_confirmation_tag #bytes #bl msg confirmation_key confirmed_transcript_hash =
-  let? expected_confirmation_tag = compute_message_confirmation_tag confirmation_key confirmed_transcript_hash in
-  return ((expected_confirmation_tag <: bytes) = (msg.auth.confirmation_tag <: bytes))
-
 (*** From/to public message ***)
 
 val public_message_to_authenticated_content:

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

@@ -8,10 +8,10 @@ type epoch_keys (bytes:Type0) = {
   sender_data_secret: bytes;
   exporter_secret: bytes;
   external_secret: bytes;
-  confirmation_key: bytes;
   membership_key: bytes;
   resumption_psk: bytes;
   epoch_authenticator: bytes;
+  confirmation_tag: bytes;
 }
 
 type treekem_keyschedule_state (bytes:Type0) = {

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

@@ -10,14 +10,15 @@ open MLS.Result
 
 val create_from_epoch_secret:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
-  bytes ->
+  bytes -> group_context_nt bytes ->
   result (treekem_keyschedule_state bytes & bytes)
-let create_from_epoch_secret #bytes #cb epoch_secret =
+let create_from_epoch_secret #bytes #cb epoch_secret group_context =
   let? sender_data_secret = secret_epoch_to_sender_data epoch_secret in
   let? encryption_secret = secret_epoch_to_encryption epoch_secret in
   let? exporter_secret = secret_epoch_to_exporter epoch_secret in
   let? external_secret = secret_epoch_to_external epoch_secret in
   let? confirmation_key = secret_epoch_to_confirmation epoch_secret in
+  let? confirmation_tag = compute_confirmation_tag (confirmation_key <: bytes) group_context.confirmed_transcript_hash in
   let? membership_key = secret_epoch_to_membership epoch_secret in
   let? resumption_psk = secret_epoch_to_resumption epoch_secret in
   let? epoch_authenticator = secret_epoch_to_authentication epoch_secret in
@@ -27,10 +28,10 @@ let create_from_epoch_secret #bytes #cb epoch_secret =
       sender_data_secret;
       exporter_secret;
       external_secret;
-      confirmation_key;
       membership_key;
       resumption_psk;
       epoch_authenticator;
+      confirmation_tag;
     };
     init_secret;
   } <: treekem_keyschedule_state bytes), (encryption_secret <: bytes))
@@ -41,7 +42,7 @@ val create_from_joiner_secret:
   result (treekem_keyschedule_state bytes & bytes)
 let create_from_joiner_secret #bytes #cb joiner_secret psks group_context =
   let? epoch_secret = secret_joiner_to_epoch joiner_secret psks group_context in
-  create_from_epoch_secret (epoch_secret <: bytes)
+  create_from_epoch_secret (epoch_secret <: bytes) group_context
 
 type secrets_for_welcome (bytes:Type0) = {
   joiner_secret: bytes;
@@ -59,7 +60,7 @@ let commit #bytes #cb st opt_commit_secret psks new_group_context =
   let? joiner_secret: bytes = secret_init_to_joiner st.init_secret opt_commit_secret new_group_context in
   let? epoch_secret: bytes = secret_joiner_to_epoch joiner_secret psks new_group_context in
   let? welcome_secret: bytes = secret_joiner_to_welcome joiner_secret psks in
-  let? (new_st, encryption_secret) = create_from_epoch_secret epoch_secret in
+  let? (new_st, encryption_secret) = create_from_epoch_secret epoch_secret new_group_context in
   return (new_st, encryption_secret, {
     joiner_secret;
     welcome_secret;

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

@@ -25,11 +25,11 @@ module KS = MLS.TreeKEM.API.KeySchedule
 val create:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
   hpke_private_key bytes -> bytes ->
-  bytes ->
+  bytes -> group_context_nt bytes ->
   result (treekem_state bytes 0 & bytes)
-let create #bytes #cb dec_key enc_key epoch_secret =
+let create #bytes #cb dec_key enc_key epoch_secret group_context =
   let tree_state = T.create dec_key enc_key in
-  let? (keyschedule_state, encryption_secret) = KS.create_from_epoch_secret epoch_secret in
+  let? (keyschedule_state, encryption_secret) = KS.create_from_epoch_secret epoch_secret group_context in
   return ({
     tree_state;
     keyschedule_state;

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

@@ -132,3 +132,10 @@ let mls_exporter #bytes #cb exporter_secret label context len =
   let? derived_secret: bytes = derive_secret exporter_secret label in
   let? hashed_context = hash_hash context in
   expand_with_label #bytes derived_secret "exported" hashed_context len
+
+val compute_confirmation_tag:
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  bytes -> bytes ->
+  result (lbytes bytes (hmac_length #bytes))
+let compute_confirmation_tag #bytes #cb confirmation_key confirmed_transcript_hash =
+  hmac_hmac confirmation_key confirmed_transcript_hash