From c397e2475e417d2eeb82616099a982b1a187e538 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Fri, 28 Jun 2024 17:57:50 +0200 Subject: [PATCH] only transmit MLSMessage on the network --- fstar/api/MLS.API.fst | 32 +++++++++++++++++++++++--------- fstar/api/MLS.fst | 6 +++--- 2 files changed, 26 insertions(+), 12 deletions(-) diff --git a/fstar/api/MLS.API.fst b/fstar/api/MLS.API.fst index 714e10d..eac7eb7 100644 --- a/fstar/api/MLS.API.fst +++ b/fstar/api/MLS.API.fst @@ -67,7 +67,7 @@ let get_public_credential #bytes #cb cred_pair = let create_key_package #bytes #cb #entropy #entropy_t cred_pair = let*? res = MLS.API.High.create_key_package cred_pair in MLS.API.High.return_prob (return ({ - key_package = serialize _ res.key_package; + key_package = serialize _ (M_mls10 (M_key_package res.key_package)); keystore_key = res.keystore_key; keystore_value = serialize _ res.keystore_value; } <: create_key_package_result bytes)) @@ -87,7 +87,12 @@ let lift_key_lookup #bytes #cb key_lookup b = | Some k -> parse _ k let start_join_group #bytes #cb welcome_bytes key_lookup = - let? welcome = from_option "start_join_group: malformed welcome" (parse _ welcome_bytes) in + let? welcome_message = from_option "start_join_group: malformed welcome" (parse _ welcome_bytes) in + let? welcome = ( + match welcome_message with + | M_mls10 (M_welcome welcome) -> return welcome + | _ -> error "start_join_group: not a welcome" + ) in MLS.API.High.start_join_group welcome (lift_key_lookup key_lookup) let continue_join_group_output bytes #cb = MLS.API.High.continue_join_group_output bytes @@ -214,7 +219,12 @@ let send_application_message #bytes #cb #entropy_t #entropy_tc st fparams messag MLS.API.High.return_prob (return (serialize _ msg, st)) let propose_add_member #bytes #cb #entropy_t #entropy_tc st fparams key_package_bytes = - let*? key_package = MLS.API.High.return_prob (from_option "propose_add_member: malformed key package" (parse _ key_package_bytes)) in + let*? key_package_message = MLS.API.High.return_prob (from_option "propose_add_member: malformed key package" (parse _ key_package_bytes)) in + let*? key_package = MLS.API.High.return_prob ( + match key_package_message with + | M_mls10 (M_key_package key_package) -> return key_package + | _ -> error "propose_add_member: not a keypackage" + ) in let*? (msg, st) = MLS.API.High.propose_add_member st (translate_framing_params fparams) key_package in MLS.API.High.return_prob (return (serialize _ msg, st)) @@ -254,15 +264,19 @@ let create_commit #bytes #cb st fparams cparams = welcome = ( match opt_welcome with | None -> None - | Some welcome -> Some (serialize _ welcome) + | Some welcome -> Some (serialize _ (M_mls10 (M_welcome welcome))) ); - group_info = serialize _ group_info; + group_info = serialize _ (M_mls10 (M_group_info group_info)); }, st)) -let create_add_proposal #bytes #cb key_package = - match Comparse.parse (MLS.Bootstrap.NetworkTypes.key_package_nt bytes MLS.TreeKEM.NetworkTypes.tkt) key_package with - | Some key_package -> return (MLS.TreeDEM.NetworkTypes.P_add { key_package }) - | None -> error "create_add_proposal: malformed key package" +let create_add_proposal #bytes #cb key_package_bytes = + let? key_package_message = from_option "create_add_member: malformed key package" (parse _ key_package_bytes) in + let? key_package = ( + match key_package_message with + | M_mls10 (M_key_package key_package) -> return key_package + | _ -> error "create_add_member: not a keypackage" + ) in + return (MLS.TreeDEM.NetworkTypes.P_add { key_package }) let create_remove_proposal #bytes #cb st removed_cred = let? removed = MLS.API.High.find_credential removed_cred.cred (MLS.Tree.get_leaf_list st.treesync.tree) in diff --git a/fstar/api/MLS.fst b/fstar/api/MLS.fst index c22121d..cd6c1e7 100644 --- a/fstar/api/MLS.fst +++ b/fstar/api/MLS.fst @@ -67,13 +67,13 @@ let add state key_package e = let (commit_result, e) = MLS.API.create_commit state fparams cparams e in let? (commit_result, st) = commit_result in let? identity = - match Comparse.parse (MLS.Bootstrap.NetworkTypes.key_package_nt bytes MLS.TreeKEM.NetworkTypes.tkt) key_package with - | None -> error "add: not a key package" - | Some kp -> ( + match Comparse.parse (MLS.TreeDEM.NetworkTypes.mls_message_nt bytes) key_package with + | Some (MLS.TreeDEM.NetworkTypes.M_mls10 (MLS.TreeDEM.NetworkTypes.M_key_package kp)) -> ( match kp.tbs.leaf_node.data.credential with | MLS.NetworkTypes.C_basic identity -> return identity | _ -> error "add: bad credential type" ) + | _ -> error "add: not a key package" in let? welcome = from_option "expected a welcome" (commit_result.welcome) in return (st, ((MLS.API.group_id state, commit_result.commit), (identity, welcome)))