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

• common tree type
• parent node type
• leaf node type
• treesync type
• mls bytes

Section 3.2: TreeSync operations

• path update / apply path
• remove
• add
• parsing
• serialization

Section 3.3: Tree Hash

• tree hash

Section 3.4: Parent Hash

• apply path loop
• parent hash computation
• parent hash verification
• revert add

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

• correctness of serialization then parsing
• correctness of parsing then serialization

Section 4.3: Tree Hash Integrity Lemma

• tree hash integrity theorem
• tree hash input

Section 4.4: Parent Hash Integrity Lemma

• revert add
• canonicalize
• tree equivalence
• parent link integrity theorem

Section 4.5: TreeSync Authentication Theorem

• leaf node signature predicate
• 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:

• 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:

• glue between the network and TreeSync/TreeKEM types
• glue between TreeSync and TreeKEM

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

• a simplified interface
• the implementation of this interface

Proofs

• 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

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.