cleanup: move DY* AuthService in a separate file

Inria-Prosecco · Oct 17, 2024 · 213640b · 213640b
1 parent 7cb8c8a
commit 213640b
Show file tree

Hide file tree

Showing 4 changed files with 40 additions and 27 deletions.
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
@@ -15,6 +15,7 @@ open MLS.TreeSync.API.Types
 open MLS.Symbolic
 open MLS.TreeSync.Symbolic.Parsers
 open MLS.TreeSync.Symbolic.IsWellFormed
+open MLS.TreeSync.Symbolic.AuthService
 open MLS.TreeSync.Symbolic.LeafNodeSignature
 
 #set-options "--fuel 1 --ifuel 1"

diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
@@ -18,8 +18,9 @@ open MLS.TreeSync.Symbolic.API.GroupManager
 open MLS.TreeSync.Symbolic.API.KeyPackageManager
 open MLS.TreeSync.Symbolic.API.Sessions
 open MLS.TreeSync.Symbolic.API.IsWellFormedInvariant
-open MLS.TreeSync.Symbolic.LeafNodeSignature
+open MLS.TreeSync.Symbolic.AuthService
 open MLS.TreeSync.Symbolic.AuthServiceCache
+open MLS.TreeSync.Symbolic.LeafNodeSignature
 open MLS.TreeSync.Symbolic.IsWellFormed
 open DY.Core
 open DY.Lib

diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst
@@ -0,0 +1,36 @@
+module MLS.TreeSync.Symbolic.AuthService
+
+open Comparse
+open DY.Core
+open DY.Lib
+open MLS.TreeSync.NetworkTypes
+open MLS.TreeSync.Invariants.AuthService
+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,
+/// 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
+  );
+  valid_successor = (fun (vk_old, cred_old) (vk_new, cred_new) ->
+    True
+  );
+}
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
@@ -21,6 +21,7 @@ open MLS.TreeSync.Proofs.ParentHashGuarantees
 open MLS.TreeSync.API.Types
 open MLS.TreeSync.Symbolic.IsWellFormed
 open MLS.TreeSync.Symbolic.Parsers
+open MLS.TreeSync.Symbolic.AuthService
 open MLS.Crypto.Derived.Symbolic.SignWithLabel
 open MLS.Symbolic
 open MLS.Result
@@ -29,32 +30,6 @@ open MLS.Result
 
 (*** Predicates ***)
 
-[@@ 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,
-/// 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
-  );
-  valid_successor = (fun (vk_old, cred_old) (vk_new, cred_new) ->
-    True
-  );
-}
-
 instance event_leaf_node_event (tkt:treekem_types dy_bytes): event (leaf_node_tbs_nt dy_bytes tkt) =
   mk_event_instance "MLS.TreeSync.LeafNodeEvent"