Artifact for "Comparse: Provably Secure Formats for Cryptographic Protocols"

Structure of the repository

• comparse: code for all the Comparse framework
• case_study: the case studies for Comparse (TLS 1.3, MLS and cTLS)
• dolev-yao-star: DY* with Comparse plugged around, and adapted NSL and ISO-DH examples.

Functions, types, and theorems from the paper

Section 2.1: Formally Defining Message Formats

• Message format
• Parser
• Serializer
• Induced message format

Section 2.2: Properties of Message Formats

• Non-ambiguity
• Non-ambiguity lemma
• Representation unicity
• Representation unicity lemma
• Non-extensibility
• Non-emptiness
• Non-emptiness lemma

Section 3.1: Defining Secure Message Formats in F*

• Type for secure formats
• Type for non-extensible secure formats
• Non-emptiness predicate

Section 3.2: The dependent pair combinator

• Definition on abstract formats
• Non-ambiguity theorem
• Representation unicity theorem
• Non-extensibility theorem
• Non-emptiness theorem
• F* combinator, non-extensible flavor
• F* combinator, extensible flavor

Section 3.3: The refinement combinator

• Definition on abstract formats
• Non-ambiguity theorem
• Representation unicity theorem
• Non-extensibility theorem
• Non-emptiness theorem
• RestrictLen non-extensibility theorem
• F* combinator, non-extensible flavor
• F* combinator, extensible flavor
• F* combinator, RestrictLen

Section 3.4: The list combinator

• Definition on abstract formats
• Non-ambiguity theorem
• Representation unicity theorem
• F* combinator

Section 3.5: The isomorphism combinator

• Definition on abstract formats
• Non-ambiguity theorem
• Representation unicity theorem
• Non-extensibility theorem
• Non-emptiness theorem
• F* function, non-extensible flavor
• F* function, extensible flavor

Section 3.6: Automating Combinator Synthesis

• ClientHello F* type
• Handshake F* type
• Meta-program entry point

Section 4.1: Format Confusion Attacks in TLS 1.0-1.2

• Signature for TLS 1.2

Section 4.2: Verified Formats for TLS 1.3

• Handshake format
• Transcript format
• Signatures
• Encryption
• Key Derivation
• Non-ambiguity with TLS 1.2 signatures

Section 4.3: Verified Formats for cTLS

• cTLS Template
• cTLS ClientHello
• Compression non-ambiguity
• Compression representation unicity
• Transcript non-ambiguity

Section 5.2: Plugging DY∗ and Comparse together

• Bytes typeclass

Section 5.3: Improving message formats in DY*

• NSL encryption input
• NSL state
• ISO-DH signature
• ISO-DH wire format
• ISO-DH state

Build

There are three ways to build Comparse.

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

pushd comparse
# This command will verify all Comparse
make
# This command will run unit tests of Comparse
make check
popd

pushd case_study
# This command will verify the case studies: TLS 1.3, MLS and cTLS
make
popd

pushd dolev-yao-star
# Verify the NSL example, modified to use Comparse
make -C nsl_pk
# Verify the ISO-DH example, modified to use Comparse
make -C iso-dh
popd

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 comparse_artifact
# Start the image and start a shell with correct environment
docker run -it comparse_artifact

pushd comparse
# This command will verify all Comparse
make
# This command will run tests of Comparse*, see last section of this README
make check
popd

pushd case_study
# This command will verify the case studies: TLS 1.3, MLS and cTLS
make
popd

pushd dolev-yao-star
# Verify the NSL example, modified to use Comparse
make -C nsl_pk
# Verify the ISO-DH example, modified to use Comparse
make -C iso-dh
popd

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 f020d2ac6e7d217d30f85e4361b2eb0b0dde7096
• 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)

pushd comparse
# This command will verify all Comparse
make
# This command will run tests of Comparse*, see last section of this README
make check
popd

pushd case_study
# This command will verify the case studies: TLS 1.3, MLS and cTLS
make
popd

pushd dolev-yao-star
# Verify the NSL example, modified to use Comparse
make -C nsl_pk
# Verify the ISO-DH example, modified to use Comparse
make -C iso-dh
popd