Merge branch 'main' into revised_api_please_rebase_before_merging

Makefile

@@ -3,12 +3,16 @@ FSTAR_HOME    ?= $(dir $(shell which fstar.exe))/..
 COMPARSE_HOME ?= $(MLS_HOME)/../comparse
 DY_HOME       ?= $(MLS_HOME)/../dolev-yao-star
 
-INNER_SOURCE_DIRS = api bootstrap common/code common/proofs glue/code glue/proofs symbolic test treedem treekem/code treekem/proofs treemath treesync/code treesync/proofs treesync/symbolic
+NO_DY ?=
+USE_DY = $(if $(NO_DY),, 1)
+
+INNER_SOURCE_DIRS = api bootstrap common/code common/proofs glue/code glue/proofs test treedem treekem/code treekem/proofs treemath treesync/code treesync/proofs $(if $(USE_DY), symbolic treesync/symbolic)
 
 HACL_SNAPSHOT_DIR = $(MLS_HOME)/hacl-star-snapshot
 SOURCE_DIRS = $(addprefix $(MLS_HOME)/fstar/, $(INNER_SOURCE_DIRS))
 
-INCLUDE_DIRS = $(SOURCE_DIRS) $(HACL_SNAPSHOT_DIR)/lib $(HACL_SNAPSHOT_DIR)/specs $(COMPARSE_HOME)/src $(DY_HOME) $(DY_HOME)/symbolic
+DY_INCLUDE_DIRS = core lib lib/comparse lib/event lib/state lib/utils
+INCLUDE_DIRS = $(SOURCE_DIRS) $(HACL_SNAPSHOT_DIR)/lib $(HACL_SNAPSHOT_DIR)/specs $(COMPARSE_HOME)/src $(if $(USE_DY), $(addprefix $(DY_HOME)/src/, $(DY_INCLUDE_DIRS)))
 FSTAR_INCLUDE_DIRS = $(addprefix --include , $(INCLUDE_DIRS))
 
 ADMIT ?=
@@ -17,8 +21,7 @@ MAYBE_ADMIT = $(if $(ADMIT),--admit_smt_queries true)
 FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe
 FSTAR = $(FSTAR_EXE) $(MAYBE_ADMIT)
 
-DY_EXTRACT = +CryptoLib +SecrecyLabels +ComparseGlue +LabeledCryptoAPI +CryptoEffect +GlobalRuntimeLib +LabeledRuntimeAPI +Ord +AttackerAPI
-FSTAR_EXTRACT = --extract '-* +MLS +Comparse $(DY_EXTRACT) -Comparse.Tactic'
+FSTAR_EXTRACT = --extract '-* +MLS +Comparse -Comparse.Tactic $(if $(USE_DY), +DY)'
 
 # Allowed warnings:
 # - (Warning 242) Definitions of inner let-rec ... and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types
@@ -68,7 +71,7 @@ obj:
 cache/MLS.Test.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+272'
 # Allow more warning in dependencies
 cache/Lib.IntTypes.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+288+349'
-cache/SecrecyLabels.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+337'
+cache/DY.Core.Bytes.Type.fst.checked: FSTAR_RULE_FLAGS = --warn_error '+290'
 
 %.checked: | hints obj
 	$(FSTAR) $(FSTAR_FLAGS) $(FSTAR_RULE_FLAGS) $< && touch -c $@

README.md

@@ -27,9 +27,7 @@ The next sections are devoted on how to setup MLS\* without Nix.
 MLS\* depends on the F\* proof-oriented programming language and the Z3 SMT solver,
 as well as two libraries:
 - [Comparse](https://github.com/TWal/comparse), for message formatting
-- [DY\*](https://github.com/REPROSEC/dolev-yao-star), for symbolic security proofs
-
-For DY\*, we rely on a version available in the [artifact for the TreeSync paper](https://github.com/Inria-Prosecco/treesync/tree/main/dolev-yao-star)
+- [DY\*](https://github.com/REPROSEC/dolev-yao-star-extrinsic), for symbolic security proofs
 
 The Javascript extraction of MLS\* furthermore rely on:
 - [HACL Packages](https://github.com/cryspen/hacl-packages), for the WASM build of HACL\* and its Javascript wrapper
@@ -63,10 +61,10 @@ export PATH=$PATH:$(cd directory/where/z3/4.8.5/lives; pwd)
 
 Two choices are possible:
 - either [Comparse](https://github.com/TWal/comparse) is cloned in `../comparse`,
-  [DY\*](https://github.com/Inria-Prosecco/treesync/tree/main/dolev-yao-star) is cloned in `../dolev-yao-star`,
+  [DY\*](https://github.com/REPROSEC/dolev-yao-star-extrinsic) is cloned in `../dolev-yao-star`,
   and `fstar.exe` is in the `PATH`
 - or [Comparse](https://github.com/TWal/comparse) is cloned in `COMPARSE_HOME`,
-  [DY\*](https://github.com/Inria-Prosecco/treesync/tree/main/dolev-yao-star) is cloned in `DY_HOME`,
+  [DY\*](https://github.com/REPROSEC/dolev-yao-star-extrinsic) is cloned in `DY_HOME`,
   and F\* in `FSTAR_HOME`,
   in that case using [direnv](https://direnv.net/) is a advisable.
 
@@ -75,17 +73,16 @@ When using relative path, the following commands will setup the dependencies.
 ```bash
 cd ..
 git clone [email protected]:TWal/comparse.git
-git clone [email protected]:Inria-Prosecco/treesync.git
-ln -s treesync/dolev-yao-star dolev-yao-star
+git clone [email protected]:REPROSEC/dolev-yao-star-extrinsic.git dolev-yao-star
 ```
 
 When using environement variables, the following commands will setup the dependencies.
 
 ```bash
 git clone [email protected]:TWal/comparse.git
 export COMPARSE_HOME=$(cd comparse; pwd)
-git clone [email protected]:Inria-Prosecco/treesync.git
-export DY_HOME=$(cd treesync/dolev-yao-star; pwd)
+git clone [email protected]:REPROSEC/dolev-yao-star-extrinsic.git dolev-yao-star
+export DY_HOME=$(cd dolev-yao-star; pwd)
 ```
 
 ### Installing the OCaml dependencies
@@ -121,3 +118,6 @@ export HACL_PACKAGES_HOME=$(cd hacl-packages; pwd)
 - `make js` will compile MLS\* to Javascript
 - `node js/test.js` will start the Javascript tests
 
+Some parts of the verification can be omitted if just the extracted code is useful:
+- `NO_DY=1 make ...` will omit all the symbolic security proofs verification (hence do not require DY\* as a dependency)
+- `ADMIT=1 make ...` will admit all SMT queries

flake.nix

@@ -9,9 +9,11 @@
       inputs.fstar-flake.follows = "fstar-flake";
     };
 
-    dolev-yao-star-src = {
-      url = "github:Inria-Prosecco/treesync";
-      flake = false;
+    dolev-yao-star-flake = {
+      url = "github:REPROSEC/dolev-yao-star-extrinsic";
+      inputs.nixpkgs.follows = "nixpkgs";
+      inputs.fstar-flake.follows = "fstar-flake";
+      inputs.comparse-flake.follows = "comparse-flake";
     };
 
     hacl-packages-src = {
@@ -20,28 +22,15 @@
     };
   };
 
-  outputs = {self, nixpkgs, fstar-flake, comparse-flake, dolev-yao-star-src, hacl-packages-src}:
+  outputs = {self, nixpkgs, fstar-flake, comparse-flake, dolev-yao-star-flake, hacl-packages-src}:
   let
     system = "x86_64-linux";
     pkgs = import nixpkgs { inherit system; };
     z3 = fstar-flake.packages.${system}.z3;
     fstar = fstar-flake.packages.${system}.fstar;
     fstar-dune = fstar-flake.packages.${system}.fstar-dune;
     comparse = comparse-flake.packages.${system}.comparse;
-    # The following is a hack, because nix is not able to fetch a subdirectory of a git repository
-    # (there is the "?dir=..." syntax, but it works only to point to the flake.nix!)
-    # There are two repositories where we may obtain dolev-yao-star
-    # - from the private dolev-yao-star repository
-    # - from the artifact of the TreeSync paper, that contains a recent public version of DY* in the dolev-yao-star subdirectory
-    # Hence, this little condition will check whether there exists a "dolev-yao-star" subdirectory
-    # (which only happens when dolev-yao-star-src points to the TreeSync artifact),
-    # and go into it when that is the case.
-    dolev-yao-star =
-      if (builtins.readDir dolev-yao-star-src)?"dolev-yao-star" then
-        "${dolev-yao-star-src}/dolev-yao-star"
-      else
-        dolev-yao-star-src
-    ;
+    dolev-yao-star = dolev-yao-star-flake.packages.${system}.dolev-yao-star;
     mls-star = pkgs.callPackage ./default.nix {inherit fstar fstar-dune z3 comparse dolev-yao-star hacl-packages-src; ocamlPackages = pkgs.ocaml-ng.ocamlPackages_4_14;};
   in {
     packages.${system} = {

fstar/api/MLS.fst

@@ -37,16 +37,10 @@ let universal_sign_nonce =
 
 let group_id = bytes
 
-let asp: as_parameters bytes = {
-  token_t = unit;
-  credential_ok = (fun _ _ -> True);
-  valid_successor = (fun _ _ -> True);
-}
-
 noeq type state = {
   group_id:mls_bytes bytes;
   leaf_index: nat;
-  treesync_state: MLS.TreeSync.API.Types.treesync_state bytes tkt asp group_id;
+  treesync_state: MLS.TreeSync.API.Types.treesync_state bytes tkt unit group_id;
   treekem_state: treekem_state bytes leaf_index;
   treedem_state: treedem_state bytes;
   epoch: nat;
@@ -219,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 ->
@@ -242,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)
@@ -452,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);