From e9c228cd8df99cb89540d489df8315acc5330744 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Wed, 3 Apr 2024 00:08:01 +0200 Subject: [PATCH] docs: improve README --- README.md | 33 +++++++++++++++++++++++++++++++-- 1 file changed, 31 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 80f5317..3babfb6 100644 --- a/README.md +++ b/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\*