Skip to content

Commit

Permalink
refactor: split TreeKEM's process_commit in two functions
Browse files Browse the repository at this point in the history
  • Loading branch information
@TWal
TWal committed May 28, 2024
1 parent 6bfe6a9 commit 0bfd619
Show file tree
Hide file tree
Showing 2 changed files with 45 additions and 22 deletions.
11 changes: 7 additions & 4 deletions fstar/api/MLS.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,8 @@ let process_commit state wire_format message message_auth =
let? (state, encryption_secret) = (
match message_content.path with
| None -> (
let? (treekem_state, encryption_secret) = MLS.TreeKEM.API.commit state.treekem_state None None provisional_group_context new_group_context in
let? pend = MLS.TreeKEM.API.prepare_process_add_only_commit state.treekem_state in
let? (treekem_state, encryption_secret) = MLS.TreeKEM.API.finalize_process_commit pend None new_group_context in
return ({ state with treekem_state;}, encryption_secret)
)
| Some path ->
Expand All @@ -236,11 +237,13 @@ let process_commit state wire_format message message_auth =
assume(MLS.NetworkBinder.Properties.path_filtering_ok state.treekem_state.tree_state.tree treekem_path);
assume(~(List.Tot.memP state.leaf_index (List.Tot.map snd added_leaves)));
let open MLS.TreeKEM.API in
MLS.TreeKEM.API.commit state.treekem_state (Some {
let? pend = MLS.TreeKEM.API.prepare_process_full_commit state.treekem_state {
commit_leaf_ind = _;
path = treekem_path;
excluded_leaves = (List.Tot.map snd added_leaves);
}) None provisional_group_context new_group_context
provisional_group_context;
} in
MLS.TreeKEM.API.finalize_process_commit pend None new_group_context
)
in
return ({ state with treesync_state; treekem_state;}, encryption_secret)
Expand Down Expand Up @@ -446,7 +449,7 @@ let generate_welcome_message st ratchet_tree new_group_context confirmation_tag

type generate_update_path_result (leaf_index:nat) = {
update_path: update_path_nt bytes;
pending_commit: MLS.TreeKEM.API.pending_commit_2 bytes leaf_index;
pending_commit: MLS.TreeKEM.API.pending_create_commit_2 bytes leaf_index;
provisional_group_context: group_context_nt bytes;
ratchet_tree: ratchet_tree_nt bytes tkt;
path_secrets: list (key_package_nt bytes tkt & bytes);
Expand Down
56 changes: 38 additions & 18 deletions fstar/treekem/code/MLS.TreeKEM.API.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,23 +84,43 @@ type full_commit_args (#bytes:Type0) {|crypto_bytes bytes|} (#leaf_ind:nat) (st:
commit_leaf_ind: commit_leaf_ind:MLS.TreeKEM.API.Tree.Types.treekem_index st{commit_leaf_ind <> leaf_ind};
path: path:pathkem bytes st.levels 0 commit_leaf_ind{path_filtering_ok st.tree path};
excluded_leaves: excluded_leaves:list nat{~(List.Tot.memP leaf_ind excluded_leaves)};
provisional_group_context: group_context_nt bytes;
}

val commit:
type pending_process_commit (#bytes:Type0) {|crypto_bytes bytes|} (#leaf_ind:nat) (st:treekem_state bytes leaf_ind) = {
next_tree_state: treekem_tree_state bytes leaf_ind;
opt_commit_secret: option bytes;
}

val prepare_process_full_commit:
#bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat ->
st:treekem_state bytes leaf_ind -> full_commit_args st.tree_state ->
result (pending_process_commit st)
let prepare_process_full_commit #bytes #cb #leaf_ind st args =
let? (next_tree_state, commit_secret) = T.commit st.tree_state args.path args.excluded_leaves args.provisional_group_context in
return ({
next_tree_state;
opt_commit_secret = Some commit_secret;
})

val prepare_process_add_only_commit:
#bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat ->
st:treekem_state bytes leaf_ind -> option (full_commit_args st.tree_state) -> option bytes -> group_context_nt bytes -> group_context_nt bytes ->
st:treekem_state bytes leaf_ind ->
result (pending_process_commit st)
let prepare_process_add_only_commit #bytes #cb #leaf_ind st =
return ({
next_tree_state = st.tree_state;
opt_commit_secret = None;
})

val finalize_process_commit:
#bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat -> #st:treekem_state bytes leaf_ind ->
pending_process_commit st -> option bytes -> group_context_nt bytes ->
result (treekem_state bytes leaf_ind & bytes)
let commit #bytes #cb #leaf_ind st opt_full_commit_args opt_psk provisional_group_context new_group_context =
let? (tree_state, opt_commit_secret) =
match opt_full_commit_args with
| None -> return (st.tree_state, None)
| Some args ->
let? (new_tree_state, commit_secret) = T.commit st.tree_state args.path args.excluded_leaves provisional_group_context in
return (new_tree_state, Some commit_secret)
in
let? (keyschedule_state, encryption_secret, _) = KS.commit st.keyschedule_state opt_commit_secret opt_psk new_group_context in
let finalize_process_commit #bytes #cb #leaf_ind #st pend opt_psk new_group_context =
let? (keyschedule_state, encryption_secret, _) = KS.commit st.keyschedule_state pend.opt_commit_secret opt_psk new_group_context in
return ({
tree_state;
tree_state = pend.next_tree_state;
keyschedule_state;
}, encryption_secret)

Expand All @@ -112,15 +132,15 @@ val prepare_create_commit_entropy_lengths:
let prepare_create_commit_entropy_lengths bytes #cb =
T.prepare_create_commit_entropy_lengths bytes

type pending_commit (#bytes:Type0) {|crypto_bytes bytes|} (#leaf_ind:nat) (st:treekem_state bytes leaf_ind) = {
type pending_create_commit (#bytes:Type0) {|crypto_bytes bytes|} (#leaf_ind:nat) (st:treekem_state bytes leaf_ind) = {
pend: MLS.TreeKEM.API.Tree.pending_commit st.tree_state;
}

val prepare_create_commit:
#bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat ->
st:treekem_state bytes leaf_ind ->
randomness bytes (prepare_create_commit_entropy_lengths bytes) ->
result (pending_commit st & pre_pathkem bytes st.tree_state.levels 0 leaf_ind)
result (pending_create_commit st & pre_pathkem bytes st.tree_state.levels 0 leaf_ind)
let prepare_create_commit #bytes #cb #leaf_ind st rand =
let? (pend, path) = T.prepare_create_commit st.tree_state rand in
return ({pend}, path)
Expand All @@ -132,7 +152,7 @@ val continue_create_commit_entropy_lengths:
let continue_create_commit_entropy_lengths #bytes #cb #leaf_ind st added_leaves =
T.finalize_create_commit_entropy_lengths st.tree_state added_leaves

type pending_commit_2 (bytes:Type0) {|crypto_bytes bytes|} (leaf_ind:nat) = {
type pending_create_commit_2 (bytes:Type0) {|crypto_bytes bytes|} (leaf_ind:nat) = {
new_state: treekem_state bytes leaf_ind;
commit_secret: bytes;
}
Expand All @@ -145,10 +165,10 @@ type continue_create_commit_result (#bytes:Type0) {|crypto_bytes bytes|} (#leaf_
val continue_create_commit:
#bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat ->
#st:treekem_state bytes leaf_ind ->
pending_commit st ->
pending_create_commit st ->
added_leaves:list nat -> group_context_nt bytes ->
randomness bytes (continue_create_commit_entropy_lengths st added_leaves) ->
result (pending_commit_2 bytes leaf_ind & continue_create_commit_result st)
result (pending_create_commit_2 bytes leaf_ind & continue_create_commit_result st)
let continue_create_commit #bytes #cb #leaf_ind #st pending added_leaves provisional_group_context randomness =
let? tree_commit_result = T.finalize_create_commit #bytes pending.pend added_leaves provisional_group_context randomness in
let new_state = { st with
Expand All @@ -172,7 +192,7 @@ type create_commit_result (bytes:Type0) {|crypto_bytes bytes|} (leaf_ind: nat) =

val finalize_create_commit:
#bytes:Type0 -> {|crypto_bytes bytes|} -> #leaf_ind:nat ->
pending_commit_2 bytes leaf_ind ->
pending_create_commit_2 bytes leaf_ind ->
group_context_nt bytes -> option bytes ->
result (create_commit_result bytes leaf_ind)
let finalize_create_commit #bytes #cb #leaf_ind pending new_group_context opt_psk =
Expand Down

0 comments on commit 0bfd619

Please sign in to comment.