diff --git a/flake.lock b/flake.lock
index c3713c2..0213d11 100644
--- a/flake.lock
+++ b/flake.lock
@@ -36,11 +36,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1728899672,
-        "narHash": "sha256-XeL8YO3sslhJ1+f7Ydxmp4p4j8ZrEmKlKbSvfAr39pg=",
+        "lastModified": 1728999480,
+        "narHash": "sha256-hdopgcd4utijr5j2vmXY164h/6cnf24QtK1RMAZjgVM=",
         "owner": "REPROSEC",
         "repo": "dolev-yao-star-extrinsic",
-        "rev": "4fe16e83dc70626200966322010cb7ad2fadf09a",
+        "rev": "92b62fb8c93cbed961e165c9da32c2d1fe34a373",
         "type": "github"
       },
       "original": {
diff --git a/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst b/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
index a07e947..6687f76 100644
--- a/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
+++ b/fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
@@ -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 /\
@@ -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;
@@ -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
@@ -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;
diff --git a/fstar/symbolic/MLS.Symbolic.fst b/fstar/symbolic/MLS.Symbolic.fst
index 6cf06f9..2decdc6 100644
--- a/fstar/symbolic/MLS.Symbolic.fst
+++ b/fstar/symbolic/MLS.Symbolic.fst
@@ -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 })
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
index 8c5d955..6623e57 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
@@ -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 -> ());
@@ -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
   )
@@ -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
   )
@@ -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 = ()
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
index 2e01233..9cdfde4 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
@@ -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:
@@ -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);*?
@@ -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 = ()
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
index ee862ec..6b84d93 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
@@ -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;
 }
 
@@ -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 -> ());
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
index a122d7c..f498f56 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
@@ -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) ->
@@ -142,11 +142,11 @@ 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 /\
@@ -154,7 +154,6 @@ let leaf_node_sign_pred #cu tkt = {
             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
@@ -350,7 +349,7 @@ 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 _. (
@@ -358,7 +357,7 @@ let parent_hash_implies_event #ci #tkt #l #i tr group_id t ast =
       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 /\
@@ -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 /\
@@ -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
 
@@ -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 /\
@@ -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"
@@ -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 /\
@@ -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