docs: improve README

README.md

@@ -1,10 +1,10 @@
 # mls-star
 
-A formal specification of IETF MLS in F*
+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)
+- 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?
 
@@ -41,6 +41,17 @@ you can find the commit of F\* that was used for CI tests (hence should be compa
 
 To actually see how to install F\*, we refer to the instructions in the F\* repository.
 
+The following commands should setup F\*.
+
+```bash
+# if you feel lucky, omit the --rev argument!
+git clone git@github.com:FStarLang/FStar.git --rev $(jq -r '.nodes."fstar-flake".locked.rev' path/to/mls-star/flake.lock)
+cd fstar
+# install F* dependencies with opam, see F*'s INSTALL.md
+make -j
+export FSTAR_HOME=$(pwd)
+```
+
 ### Installing Comparse and DY\*
 
 Two choices are possible:
@@ -52,6 +63,24 @@ Two choices are possible:
   and F\* in `FSTAR_HOME`,
   in that case using [direnv](https://direnv.net/) is a advisable.
 
+When using relative path, the following commands will setup the dependencies.
+
+```bash
+cd ..
+git clone git@github.com:TWal/comparse.git
+git clone git@github.com:Inria-Prosecco/treesync.git
+ln -s treesync/dolev-yao-star dolev-yao-star
+```
+
+When using environement variables, the following commands will setup the dependencies.
+
+```bash
+git clone git@github.com:TWal/comparse.git
+export COMPARSE_HOME=$(cd comparse; pwd)
+git clone git@github.com:Inria-Prosecco/treesync.git
+export DY_HOME=$(cd treesync/dolev-yao-star; pwd)
+```
+
 ### Building
 
 - Running `make` will verify MLS\*