Skip to content

Commit

Permalink
docs: update DY* links
Browse files Browse the repository at this point in the history
  • Loading branch information
TWal committed May 22, 2024
1 parent 842b004 commit 3a504f4
Showing 1 changed file with 6 additions and 9 deletions.
15 changes: 6 additions & 9 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.

Expand All @@ -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
Expand Down

0 comments on commit 3a504f4

Please sign in to comment.