Skip to content

Inria-Prosecco/treesync

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

2 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Artifact for "TreeSync: Authenticated Group Management for Messaging Layer Security"

Link to the paper

Cryptology ePrint Archive

Structure of the repository

  • 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

Functions, types, and theorems from the paper

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

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

Build

There are three ways to build MLS*.

Using nix (recommended)

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

Using docker (recommended)

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

Using a locally-installed F* (not recommended)

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

Tour of the code

All of the MLS* code is located inside the directory mls-star/fstar.

Specification

The common directory contains code and proofs shared between the different components of MLS*, with:

The treesync/code directory contains the TreeSync component code, with:

The treekem directory contains the TreeKEM component code, with:

The treedem directory contains the TreeDEM component code, with:

The glue directory contains glue code, with:

The api directory contains a simplified high-level API combining everything, with:

Proofs

The treesync/proofs directory contains invariant proofs and all various hash integrity theorems, with:

The treesync/symbolic directory contains all the symbolic proofs and API, with:

What is tested with make check?

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_Ed25519
  • MLS_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.

About

No description, website, or topics provided.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published