Skip to content

Commit

Permalink
chore: update DY* and F*
Browse files Browse the repository at this point in the history
  • Loading branch information
@TWal
TWal committed Oct 15, 2024
1 parent 831affa commit 10b45f9
Show file tree
Hide file tree
Showing 7 changed files with 45 additions and 34 deletions.
12 changes: 6 additions & 6 deletions flake.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

14 changes: 8 additions & 6 deletions fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -171,14 +171,15 @@ let has_mls_signwithlabel_pred #cinvs tagged_local_pred =
(*** Lemmas on SignWithLabel and VerifyWithLabel ***)

val bytes_invariant_sign_with_label:
{|crypto_invariants|} -> spred:signwithlabel_crypto_pred -> tr:trace ->
{|crypto_invariants|} -> spred:signwithlabel_crypto_pred ->
tr:trace -> prin:principal ->
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 /\
get_usage sk == mk_mls_sigkey_usage prin /\
SigNonce? (get_usage nonce) /\
(get_label tr sk) `can_flow tr` (get_label tr nonce) /\
spred.pred tr (vk sk) msg /\
Expand All @@ -188,7 +189,7 @@ val bytes_invariant_sign_with_label:
bytes_invariant tr (Success?.v (sign_with_label sk lab msg nonce)) /\
(get_label tr (Success?.v (sign_with_label sk lab msg nonce))) `can_flow tr` (get_label tr msg)
)
let bytes_invariant_sign_with_label #ci spred tr sk lab msg nonce =
let bytes_invariant_sign_with_label #ci spred tr prin sk lab msg nonce =
let sign_content: sign_content_nt bytes = {
label = get_mls_label lab;
content = msg;
Expand All @@ -197,7 +198,8 @@ let bytes_invariant_sign_with_label #ci spred tr sk lab msg nonce =
serialize_wf_lemma (sign_content_nt bytes) (is_knowable_by (get_label tr msg) tr) sign_content

val bytes_invariant_verify_with_label:
{|ci:crypto_invariants|} -> spred:signwithlabel_crypto_pred -> tr:trace ->
{|ci:crypto_invariants|} -> spred:signwithlabel_crypto_pred ->
tr:trace -> prin:principal ->
vk:bytes -> lab:valid_label -> content:mls_bytes bytes -> signature:bytes ->
Lemma
(requires
Expand All @@ -209,13 +211,13 @@ val bytes_invariant_verify_with_label:
)
(ensures
(
get_signkey_usage vk == SigKey "MLS.LeafSignKey" empty ==>
get_signkey_usage vk == mk_mls_sigkey_usage prin ==>
spred.pred tr vk content
) \/ (
(get_signkey_label tr vk) `can_flow tr` public
)
)
let bytes_invariant_verify_with_label #ci spred tr vk lab content signature =
let bytes_invariant_verify_with_label #ci spred tr prin vk lab content signature =
let sign_content: sign_content_nt bytes = {
label = get_mls_label lab;
content = content;
Expand Down
13 changes: 13 additions & 0 deletions fstar/symbolic/MLS.Symbolic.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,3 +97,16 @@ 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

type mls_principal = {
who: principal;
}

%splice [ps_mls_principal] (gen_parser (`mls_principal))

instance parseable_serializeable_bytes_mls_principal: parseable_serializeable bytes mls_principal =
mk_parseable_serializeable ps_mls_principal

val mk_mls_sigkey_usage: principal -> usage
let mk_mls_sigkey_usage who =
SigKey "MLS.LeafSignKey" (serialize _ { who })
8 changes: 4 additions & 4 deletions fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -222,7 +222,7 @@ instance parseable_serializeable_treesync_private_state: parseable_serializeable
val treesync_private_state_pred: {|crypto_invariants|} -> local_state_predicate treesync_private_state
let treesync_private_state_pred #ci = {
pred = (fun tr prin state_id st ->
is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key
is_signature_key (mk_mls_sigkey_usage prin) (principal_label prin) tr st.signature_key
);
pred_later = (fun tr1 tr2 prin state_id st -> ());
pred_knowable = (fun tr prin state_id st -> ());
Expand Down Expand Up @@ -254,7 +254,7 @@ val new_private_treesync_state_proof:
tr:trace ->
Lemma
(requires
is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key /\
is_signature_key (mk_mls_sigkey_usage prin) (principal_label prin) tr st.signature_key /\
trace_invariant tr /\
has_treesync_private_state_invariant
)
Expand All @@ -276,7 +276,7 @@ val set_private_treesync_state_proof:
tr:trace ->
Lemma
(requires
is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key /\
is_signature_key (mk_mls_sigkey_usage prin) (principal_label prin) tr st.signature_key /\
trace_invariant tr /\
has_treesync_private_state_invariant
)
Expand Down Expand Up @@ -307,7 +307,7 @@ val get_private_treesync_state_proof:
match opt_result with
| None -> True
| Some st ->
is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key
is_signature_key (mk_mls_sigkey_usage prin) (principal_label prin) tr st.signature_key
)
))
let get_private_treesync_state_proof #invs prin state_id tr = ()
7 changes: 3 additions & 4 deletions fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,7 @@ val get_token_for:
inp:as_input dy_bytes ->
traceful (option dy_as_token)
let get_token_for p as_session (verification_key, credential) =
let*? { who; usg; time; } = find_verified_credential p as_session ({ verification_key; credential; }) in
guard (usg = "MLS.LeafSignKey");*?
let*? { who; time; } = find_verified_credential p as_session ({ verification_key; credential; }) in
return (Some ({ who; time; } <: dy_as_token))

val get_token_for_proof:
Expand Down Expand Up @@ -494,7 +493,7 @@ val create_signature_keypair:
p:principal ->
traceful (option (state_id & signature_public_key_nt dy_bytes))
let create_signature_keypair p =
let* signature_key = mk_rand (SigKey "MLS.LeafSignKey" empty) (principal_label p) 32 in
let* signature_key = mk_rand (mk_mls_sigkey_usage p) (principal_label p) 32 in
let verification_key = vk signature_key in
guard (length (signature_key <: dy_bytes) < pow2 30);*?
guard (length (verification_key <: dy_bytes) < pow2 30);*?
Expand All @@ -517,7 +516,7 @@ val create_signature_keypair_proof:
match opt_res with
| None -> True
| Some (private_si, verification_key) ->
is_verification_key (SigKey "MLS.LeafSignKey" empty) (principal_label p) tr_out verification_key
is_verification_key (mk_mls_sigkey_usage p) (principal_label p) tr_out verification_key
)
))
let create_signature_keypair_proof #invs p tr = ()
Expand Down
4 changes: 1 addition & 3 deletions fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,6 @@ type as_cache_key = {
[@@ with_bytes dy_bytes]
type as_cache_value = {
who: principal;
[@@@ with_parser #bytes ps_string]
usg: string;
time: nat;
}

Expand All @@ -43,7 +41,7 @@ let as_cache_pred #ci = {
value.time <= DY.Core.Trace.Base.length tr /\
is_publishable (prefix tr value.time) key.verification_key /\
get_signkey_label tr key.verification_key == principal_label value.who /\
get_signkey_usage key.verification_key == SigKey value.usg empty /\
get_signkey_usage key.verification_key == mk_mls_sigkey_usage value.who /\
is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_publishable (prefix tr value.time)) key.credential
);
pred_later = (fun tr1 tr2 prin state_id key value -> ());
Expand Down
21 changes: 10 additions & 11 deletions fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ let dy_asp #ci tr = {
credential_ok = (fun (vk, cred) token ->
token.time <= (DY.Core.Trace.Base.length tr) /\
bytes_invariant (prefix tr token.time) vk /\
get_signkey_usage vk == SigKey "MLS.LeafSignKey" empty /\
get_signkey_usage vk == mk_mls_sigkey_usage token.who /\
get_signkey_label tr vk == principal_label token.who
);
valid_successor = (fun (vk_old, cred_old) (vk_new, cred_new) ->
Expand Down Expand Up @@ -142,19 +142,18 @@ let leaf_node_sign_pred #cu tkt = {
| None -> False
| Some ln_tbs -> (
exists prin.
get_signkey_usage vk == mk_mls_sigkey_usage prin /\
leaf_node_has_event prin tr ln_tbs /\ (
match ln_tbs.data.source with
| LNS_commit -> (
exists (tl: tree_list dy_bytes tkt).
get_signkey_label tr vk == principal_label prin /\
tree_list_starts_with_tbs tl ln_tbs_bytes /\
tree_list_is_parent_hash_linkedP tl /\
tree_list_ends_at_root tl /\
tree_list_is_canonicalized ln_tbs.leaf_index tl /\
tree_list_has_event prin tr ln_tbs.group_id tl
)
| LNS_update -> (
get_signkey_label tr vk == principal_label prin /\
tree_has_event prin tr ln_tbs.group_id (|0, ln_tbs.leaf_index, TLeaf (Some ({data = ln_tbs.data; signature = empty #dy_bytes;} <: leaf_node_nt dy_bytes tkt))|)
)
| LNS_key_package -> True
Expand Down Expand Up @@ -350,15 +349,15 @@ let parent_hash_implies_event #ci #tkt #l #i tr group_id t ast =
let authentifier_li = leaf_i in
let leaf_sk_label = principal_label leaf_token.who in
serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (bytes_invariant tr) ln_tbs;
bytes_invariant_verify_with_label (leaf_node_sign_pred tkt) tr ln.data.signature_key "LeafNodeTBS" ln_tbs_bytes ln.signature;
bytes_invariant_verify_with_label (leaf_node_sign_pred tkt) tr authentifier ln.data.signature_key "LeafNodeTBS" ln_tbs_bytes ln.signature;

introduce ((leaf_node_sign_pred tkt).pred tr ln.data.signature_key ln_tbs_bytes) ==> tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|)
with _. (
(
parse_serialize_inv_lemma #dy_bytes (leaf_node_tbs_nt dy_bytes tkt) ln_tbs;

eliminate exists (prin:principal) (leaf_tl: tree_list dy_bytes tkt).
get_signkey_label tr ln.data.signature_key == principal_label prin /\
get_signkey_usage ln.data.signature_key == mk_mls_sigkey_usage prin /\
tree_list_starts_with_tbs leaf_tl ln_tbs_bytes /\
tree_list_is_parent_hash_linkedP leaf_tl /\
tree_list_ends_at_root leaf_tl /\
Expand Down Expand Up @@ -659,7 +658,7 @@ val is_msg_external_path_to_path:
is_well_formed _ (is_knowable_by label tr) t /\
is_well_formed _ (is_knowable_by label tr) p /\
is_knowable_by label tr group_id /\
bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" empty /\
bytes_invariant tr sk /\ get_usage sk == mk_mls_sigkey_usage prin /\
bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\
get_label tr sk == principal_label prin /\
get_label tr nonce == principal_label prin /\
Expand Down Expand Up @@ -696,7 +695,7 @@ let is_msg_external_path_to_path #ci #tkt #l #li prin label tr t p group_id sk n
leaf_node_has_event prin tr new_ln_tbs
with prin tl and ();
parse_serialize_inv_lemma #dy_bytes (leaf_node_tbs_nt dy_bytes tkt) new_ln_tbs;
bytes_invariant_sign_with_label (leaf_node_sign_pred tkt) tr sk "LeafNodeTBS" new_ln_tbs_bytes nonce;
bytes_invariant_sign_with_label (leaf_node_sign_pred tkt) tr prin sk "LeafNodeTBS" new_ln_tbs_bytes nonce;
is_well_formed_set_path_leaf (is_knowable_by label tr) p new_ln
#pop-options

Expand All @@ -715,7 +714,7 @@ val is_msg_sign_leaf_node_data_key_package:
Success? (sign_leaf_node_data_key_package ln_data sk nonce) /\
leaf_node_has_event prin tr ({data = ln_data; group_id = (); leaf_index = ();}) /\
is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_knowable_by label tr) ln_data /\
bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" empty /\
bytes_invariant tr sk /\ get_usage sk == mk_mls_sigkey_usage prin /\
bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\
get_label tr sk == principal_label prin /\
get_label tr nonce == principal_label prin /\
Expand All @@ -727,7 +726,7 @@ let is_msg_sign_leaf_node_data_key_package #ci #tkt prin label tr ln_data sk non
let ln_tbs_bytes: dy_bytes = serialize _ ln_tbs in
parse_serialize_inv_lemma #dy_bytes (leaf_node_tbs_nt dy_bytes tkt) ln_tbs;
serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (is_knowable_by label tr) ln_tbs;
bytes_invariant_sign_with_label (leaf_node_sign_pred tkt) tr sk "LeafNodeTBS" ln_tbs_bytes nonce
bytes_invariant_sign_with_label (leaf_node_sign_pred tkt) tr prin sk "LeafNodeTBS" ln_tbs_bytes nonce
#pop-options

#push-options "--z3rlimit 25"
Expand All @@ -745,7 +744,7 @@ val is_msg_sign_leaf_node_data_update:
tree_has_event prin tr group_id (|0, (leaf_index <: nat), TLeaf (Some ({data = ln_data; signature = empty #dy_bytes;} <: leaf_node_nt dy_bytes tkt))|) /\
is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_knowable_by label tr) ln_data /\
is_knowable_by label tr group_id /\
bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" empty /\
bytes_invariant tr sk /\ get_usage sk == mk_mls_sigkey_usage prin /\
bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\
get_label tr sk == principal_label prin /\
get_label tr nonce == principal_label prin /\
Expand All @@ -757,5 +756,5 @@ let is_msg_sign_leaf_node_data_update #ci #tkt prin label tr ln_data group_id le
let ln_tbs_bytes: dy_bytes = serialize _ ln_tbs in
parse_serialize_inv_lemma #dy_bytes (leaf_node_tbs_nt dy_bytes tkt) ln_tbs;
serialize_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (is_knowable_by label tr) ln_tbs;
bytes_invariant_sign_with_label (leaf_node_sign_pred tkt) tr sk "LeafNodeTBS" ln_tbs_bytes nonce
bytes_invariant_sign_with_label (leaf_node_sign_pred tkt) tr prin sk "LeafNodeTBS" ln_tbs_bytes nonce
#pop-options

0 comments on commit 10b45f9

Please sign in to comment.