cleanup: rework AuthService around credential_to_principal

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst

@@ -59,8 +59,8 @@ 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; time; } = find_verified_credential p as_session ({ verification_key; credential; }) in
-  return (Some ({ who; time; } <: dy_as_token))
+  let*? { token } = find_verified_credential p as_session ({ verification_key; credential; }) in
+  return (Some token)
 
 val get_token_for_proof:
   {|protocol_invariants|} ->

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.CredentialInterpretation.fst

@@ -0,0 +1,9 @@
+module MLS.TreeSync.Symbolic.AuthService.CredentialInterpretation
+
+open Comparse
+
+let credential_to_principal cred =
+  match cred with
+  | C_basic identity ->
+    (ps_prefix_to_ps_whole ps_principal).parse (identity <: bytes)
+  | _ -> None

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.CredentialInterpretation.fsti

@@ -0,0 +1,10 @@
+module MLS.TreeSync.Symbolic.AuthService.CredentialInterpretation
+
+open DY.Core
+open DY.Lib
+open MLS.NetworkTypes
+
+val credential_to_principal:
+  credential_nt bytes ->
+  option principal
+

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst

@@ -5,32 +5,52 @@ open DY.Core
 open DY.Lib
 open MLS.TreeSync.NetworkTypes
 open MLS.TreeSync.Invariants.AuthService
+open MLS.TreeSync.Symbolic.AuthService.CredentialInterpretation
 open MLS.Symbolic
 
 #set-options "--fuel 0 --ifuel 0"
 
 [@@ with_bytes dy_bytes]
 type dy_as_token = {
-  who: principal;
   time: nat;
 }
 
 %splice [ps_dy_as_token] (gen_parser (`dy_as_token))
 %splice [ps_dy_as_token_is_well_formed] (gen_is_well_formed_lemma (`dy_as_token))
 
 /// Instantiation of the abstract "Authentication Service" for DY*.
-/// The token is a a principal and a timestamp,
+/// The token is a a timestamp,
 /// and the AS attests that the signature verification key belonged to that principal at that time.
 val dy_asp: {|crypto_invariants|} -> trace -> as_parameters dy_bytes
 let dy_asp #ci tr = {
   token_t = dy_as_token;
   credential_ok = (fun (vk, cred) token ->
-    token.time <= (DY.Core.Trace.Base.length tr) /\
-    bytes_invariant (prefix tr token.time) vk /\
-    vk `has_signkey_usage tr` mk_mls_sigkey_usage token.who /\
-    get_signkey_label tr vk == principal_label token.who
+    match credential_to_principal cred with
+    | None -> False
+    | Some who ->
+      token.time <= (DY.Core.Trace.Base.length tr) /\
+      bytes_invariant (prefix tr token.time) vk /\
+      vk `has_signkey_usage (prefix tr token.time)` mk_mls_sigkey_usage who /\
+      get_signkey_label (prefix tr token.time) vk == principal_label who
   );
   valid_successor = (fun (vk_old, cred_old) (vk_new, cred_new) ->
     True
   );
 }
+
+val dy_asp_later:
+  {|crypto_invariants|} ->
+  tr1:trace -> tr2:trace ->
+  inp:as_input bytes -> token:dy_as_token ->
+  Lemma
+  (requires
+    (dy_asp tr1).credential_ok inp token /\
+    tr1 <$ tr2
+  )
+  (ensures (dy_asp tr2).credential_ok inp token)
+  [SMTPat ((dy_asp tr1).credential_ok inp token);
+   SMTPat (tr1 <$ tr2)]
+let dy_asp_later #cinvs tr1 tr2 (vk, cred) token =
+  match credential_to_principal cred with
+  | None -> ()
+  | Some who -> ()

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst

@@ -5,6 +5,7 @@ open DY.Core
 open DY.Lib
 open MLS.NetworkTypes
 open MLS.TreeSync.NetworkTypes
+open MLS.TreeSync.Symbolic.AuthService
 open MLS.Symbolic
 
 #set-options "--fuel 0 --ifuel 0"
@@ -22,8 +23,7 @@ type as_cache_key = {
 
 [@@ with_bytes dy_bytes]
 type as_cache_value = {
-  who: principal;
-  time: nat;
+  token: dy_as_token;
 }
 
 %splice [ps_as_cache_value] (gen_parser (`as_cache_value))
@@ -38,11 +38,9 @@ instance as_cache_types: map_types as_cache_key as_cache_value = {
 val as_cache_pred: {|crypto_invariants|} -> map_predicate as_cache_key as_cache_value #_
 let as_cache_pred #ci = {
   pred = (fun tr prin state_id key value ->
-    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 /\
-    key.verification_key `has_signkey_usage tr` 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
+    (dy_asp tr).credential_ok (key.verification_key, key.credential) value.token /\
+    is_publishable tr key.verification_key /\
+    is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_publishable tr) key.credential
   );
   pred_later = (fun tr1 tr2 prin state_id key value -> ());
   pred_knowable = (fun tr prin state_id key value ->

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst

@@ -22,6 +22,7 @@ open MLS.TreeSync.API.Types
 open MLS.TreeSync.Symbolic.IsWellFormed
 open MLS.TreeSync.Symbolic.Parsers
 open MLS.TreeSync.Symbolic.AuthService
+open MLS.TreeSync.Symbolic.AuthService.CredentialInterpretation
 open MLS.Crypto.Derived.Symbolic.SignWithLabel
 open MLS.Symbolic
 open MLS.Result
@@ -298,7 +299,7 @@ val parent_hash_implies_event:
   )
   (ensures (
     let authentifier_li = get_authentifier_index t in
-    let authentifier = (Some?.v (leaf_at ast authentifier_li)).who in
+    let authentifier = (Some?.v (credential_to_principal (Some?.v (leaf_at t authentifier_li)).data.credential)) in
     (
       tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|)
     ) \/ (
@@ -320,9 +321,9 @@ let parent_hash_implies_event #ci #tkt #l #i tr group_id t ast =
   } in
   let ln_tbs_bytes = get_leaf_tbs ln group_id leaf_i in
   let leaf_token = Some?.v (leaf_at ast leaf_i) in
-  let authentifier = leaf_token.who in
   let authentifier_li = leaf_i in
-  let leaf_sk_label = principal_label leaf_token.who in
+  let authentifier = (Some?.v (credential_to_principal (Some?.v (leaf_at t authentifier_li)).data.credential)) in
+  let leaf_sk_label = principal_label authentifier 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 authentifier ln.data.signature_key "LeafNodeTBS" ln_tbs_bytes ln.signature;
 
@@ -351,7 +352,7 @@ let parent_hash_implies_event #ci #tkt #l #i tr group_id t ast =
     )
   );
 
-  introduce (can_flow tr leaf_sk_label public) ==> is_corrupt tr (principal_label ((Some?.v (leaf_at ast (get_authentifier_index t))).who))
+  introduce (can_flow tr leaf_sk_label public) ==> is_corrupt tr (principal_label authentifier)
   with _. ()
 #pop-options
 
@@ -432,7 +433,7 @@ val state_implies_event:
     // The following line is only there as precondition for the rest of the theorem
     unmerged_leaves_ok t /\ parent_hash_invariant t /\ all_credentials_ok t ast /\ (
       let authentifier_li = get_authentifier_index t in
-      let authentifier = (Some?.v (leaf_at ast authentifier_li)).who in
+      let authentifier = (Some?.v (credential_to_principal (Some?.v (leaf_at t authentifier_li)).data.credential)) in
       (
         tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|)
       ) \/ (