- comparse: external support library for parsers and serializers, imported, not part of this work
- dolev-yao-star: external support library for Dolev-Yao reasoning in F*, imported, not part of this work
- mls-star: this work
Section 3.1: TreeSync data structures
Section 3.2: TreeSync operations
Section 3.3: Tree Hash
Section 3.4: Parent Hash
Section 4.1: TreeSync State Invariants
- unmerged leaves invariant
- leaf signature valid and verified by authentication service invariants
- parent hash link
- parent hash invariant
- refined type for treesync
Section 4.2: Verified Parsing and Serialization
Section 4.3: Tree Hash Integrity Lemma
Section 4.4: Parent Hash Integrity Lemma
Section 4.5: TreeSync Authentication Theorem
There are three ways to build MLS*.
This artifact is reproducible thanks to nix. It uses the flakes feature, make sure to enable it.
# This command will compile Z3, F*,
# and the other dependencies to the correct version
nix develop
cd mls-star
# This command will verify MLS*
make
# This command will run tests of MLS*, see last section of this README
make check
If nix is not installed on the system, it can be used through a docker image we provide.
# Build the docker image. This will compile Z3 and F* to the correct version.
docker build . -t treesync_artifact
# Start the image and start a shell with correct environment
docker run -it treesync_artifact
cd mls-star
# This command will verify MLS*
make
# This command will run tests of MLS*, see last section of this README
make check
This artifact can also be built directly, assuming the host system has the correct dependencies.
This artifact is compatible with:
- F* commit eb911fc41d5ba730c15f2ac296ffc5ebf7b46560
- Z3 version 4.8.5
- OCaml version 4.14
However we can't guarantee everything will go smoothly with this method.
# Change the PATH to have z3 and fstar.exe
export PATH=$PATH:/path/to/z3/directory/bin:/path/to/fstar/directory/bin
# Setup the environment
export FSTAR_HOME=/path/to/fstar/directory
eval $(opam env)
cd mls-star
# This command will verify MLS*
make
# This command will run tests of MLS*, see last section of this README
make check
All of the MLS* code is located inside the directory mls-star/fstar.
The common directory contains code and proofs shared between the different components of MLS*, with:
- Cryptography typeclass
- Common serializable types
- Result monad
- Generic type for trees and paths
- Common operations on trees
- And various associated lemmas
The treesync/code directory contains the TreeSync component code, with:
- Serializable types from the RFC
- TreeSync's tree definition
- Atomic operations on TreeSync's tree
- Tree hash computation
- Parent hash computation
- Invariant on unmerged leaves
- Invariant on parent hash
- Invariant on leaf signature validity
- Invariant on authentication service
- A refined type for TreeSync's tree, enforcing the invariants
- Atomic operations on the refined tree
- A type for TreeSync's state
- Operations on TreeSync's state
The treekem directory contains the TreeKEM component code, with:
- Serializable types from the RFC
- TreeKEM's tree definition
- Atomic operations on TreeKEM's tree
- A type for TreeKEM's state
- Operations on TreeKEM's state
The treedem directory contains the TreeDEM component code, with:
- Serializable types from the RFC
- Implementation of the key schedule
- Types for the message content
- Types for the message framing
- Functions for the message framing
- Computation of the transcript hash
- Implementation of PSKs
- Processing of the Welcome message
The glue directory contains glue code, with:
The api directory contains a simplified high-level API combining everything, with:
- glue code and alternative DY* interface
- generic code to make global predicates from local ones
- interface for sessions, using local predicates
- interface for typed sessions (not just bytes)
- generic session to implement a key/value dictionnary
- parser definitions useful for the symbolic proofs
The treesync/proofs directory contains invariant proofs and all various hash integrity theorems, with:
- Invariant proof for unmerged leaves
- Invariant proof for parent hash
- Invariant proof for leaf signature validity
- Invariant proof for authentication service
- Tree hash integrity proof
- Parent hash integrity proof
- Parent hash link integrity proof
The treesync/symbolic directory contains all the symbolic proofs and API, with:
- Leaf node signature guarantees
- State type and invariants
- API exposing state modification
- and various other boilerplate code, either for the API or for the proofs
There are four types of tests:
- internal tests of the high-level API, which sends messages within a small group
- tests for the RFC test vectors
- fuzzer for the correctness of TreeKEM
- benchmarks
We pass all test vectors for the following ciphersuites:
MLS_128_DHKEMX25519_AES128GCM_SHA256_Ed25519MLS_128_DHKEMX25519_CHACHA20POLY1305_SHA256_Ed25519
If any of the test, fuzz or benchmark fails, the make check command will fail and the corresponding error is printed.
The test vectors comes from the official repository, with the commit revision present in this file.