From 662c741efb47d568fbf00e5887126463f592add4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= <theophile@wallez.net>
Date: Tue, 2 Apr 2024 20:27:48 +0200
Subject: [PATCH] docs: improve README

---
 README.md | 55 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)

diff --git a/README.md b/README.md
index a8d42c5..80f5317 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,58 @@
 # mls-star
 
 A formal specification of IETF MLS in F*
+
+## Papers linked to this repository
+
+- TreeSync: Authenticated Group Management for Messaging Layer Security, USENIX Security '23 [usenix](https://www.usenix.org/conference/usenixsecurity23/presentation/wallez) [eprint](https://eprint.iacr.org/2022/1732)
+
+## What is verified?
+
+Currently, only the TreeSync sub-protocol is verified.
+Other components (such as TreeKEM, TreeDEM or the high-level API) are not yet verified.
+
+## How to build
+
+### The easy way
+
+Using the Nix package manager,
+we can install all dependencies using `nix develop`,
+or compile MLS* and run all its tests using `nix flake check`.
+
+To compile MLS* without Nix, see the next sections.
+
+### Dependencies
+
+MLS\* depends on the F\* proof-oriented programming language,
+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)
+
+### Installing F\*
+
+We use bleeding edge features of F\*, hence we recommend to use the latest commit of F\*'s master branch.
+
+MLS\* is actively maintained (at the time of writing) and will be updated quickly in case a new version of F\* breaks the build,
+however if this is not the case anymore,
+you can find the commit of F\* that was used for CI tests (hence should be compatible) with the following command:
+`jq -r '.nodes."fstar-flake".locked.rev' flake.lock`
+
+To actually see how to install F\*, we refer to the instructions in the F\* repository.
+
+### Installing Comparse and DY\*
+
+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`,
+  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`,
+  and F\* in `FSTAR_HOME`,
+  in that case using [direnv](https://direnv.net/) is a advisable.
+
+### Building
+
+- Running `make` will verify MLS\*
+- Running `make check` will run the tests of MLS\* (interoperability tests, and some light fuzzing)