Logical Relations for Formally Verified Authenticated Data Structures

This repository contains the Rocq and OCaml development accompanying the CCS 2025 submission Logical Relations for Formally Verified Authenticated Data Structures by Simon Oddershede Gregersen, Chaitanya Agarwal, and Joseph Tassarotti.

A high-level overview of the repository and build instructions are found below. PAPER.md provides a detailed mapping from the paper to the OCaml and Rocq developments.

The design of the Authentikit OCaml library is due to Bob Atkey. Our approach to (type) binding found in theories/binding is due to Filip Sieczkowski and Piotr Polesiuk.

Overview

Below is an overview of the most relevant folders and files.

• theories/: Rocq development
  • examples/
    • authentikit.v: the Authentikit interface
    • authentikit_base_security.v: shared aux. results and definitions for the security proofs.
    • authentikit_base_correctness.v: shared aux. results and definitions for the correctness proofs.
    • authentikit_list.v: naive Authentikit implementation
    • authentikit_list_security.v: security of the naive Authentikit implementation
    • authentikit_list_correctness.v: correctness of the naive Authentikit implementation
    • authentikit_rev_list.v: list-reverse optimization
    • authentikit_rev_list_correctness.v: correctness
    • authentikit_buf.v: proof-buffering optimization
    • authentikit_buf_security.v: security
    • authentikit_buf_correctness.v: correctness
    • authentikit_buf_magic.v: proof buffering and hetereogenous cache optimization
    • authentikit_buf_magic_security.v: security
    • authentikit_buf_magic_correctness.v: correctness
    • authentikit_buf_magic_state.v: stateful optimization
    • authentikit_buf_magic_state_security.v: security
    • authentikit_buf_magic_state_correctness.v: correctness
    • pair.v: minimal example of manual security/correctness proof
    • merkle.v: optimized Merkle retrieve, implementation
    • merkle_retrieve_security.v: security
    • merkle_retrieve_correctness.v: correctness
  • heap_lang/:
    • lang.v: the definition of untyped $F_{\omega, \mu}^{ref}$
    • adequacy_upto_bad.v: soundness of CF-SL
  • program_logic_upto_bad/: generic up-to-bad logic, specialized to obtain CF-SL
  • rel_logic_bin/: binary logical relation
  • rel_logic_tern/: ternary logical relation
  • typing/: types and syntactic type system for $F_{\omega, \mu}^{ref}$
• src/: OCaml development
  • basic/: this matches the Rocq development
    • auth.ml: the Authentikit interface
    • authenticatable_base.ml: serialization/deserialization library
    • prover.ml: prover's naive Authentikit implementation
    • prover_rev.ml: prover's list-reverse optimization
    • prover_buf.ml: prover's proof-buffering optimization
    • prover_buf_magic_state.ml: prover's stateful optimization
    • verifier.ml: verifier's naive Authentikit implementation
    • verifier_buf.ml: verifier's proof-buffer optimization
    • verifier_buf_magic.ml: verifier's heterogenous-caching optimization
    • verifier_buf_magic_state.ml: verifier's stateful optimization
    • merkle.ml: merkle tree functor that uses Authentikit and an optimized retrieve function
    • redblack.ml: redblack functor
    • trimerkle.ml: ternary rose-merkle tree functor
  • opt/: optimized development
    • authenticatable_marshal.ml: optimized serialization library
    • prover_rev.ml: prover's optimized list-reverse implementation using forced-inlining
    • prover_io.ml: prover's implementation that writes proof stream to a file.
    • verifier.ml: verifier's optimized implementation using forced-inlining
    • verifier_io.ml: verifier's implementation that reads proof stream from a file.

Building the Rocq development

The project is known to compile with

• Rocq 8.19.2
• std++ 1.11.0
• Iris 4.3.0

The recommended way to install the dependencies is through opam.

1. Install opam if not already installed (a version greater than 2.0 is required).
2. Install a new switch and link it to the project.

opam switch create auth 4.14.2
opam switch link auth .

3. Add the Rocq opam repository.

opam repo add rocq-released https://rocq-prover.org/opam/released
opam update

4. Install the right version of the dependencies as specified in the auth.opam file.

opam install . --deps-only

You should now be able to build the development by using make -j N where N is the number of cores available on your machine.

Building the OCaml development

The project is known to compile with

• OCaml 4.14.2

The instructions for building the Rocq development will also install OCaml at this version. You should be able to build the development and run the test suite by running make in the src/basic/ folder.

Docker

The development can be build and run using Docker. Suggested commands for building, interacting with, saving, and loading an image are shown below. Note that building the Dockerfile requires the development to be available in the same folder.

Build image

make tar
docker build -t auth .

The build command may need a --platform linux/amd64 option if run on Apple Silicon.

Interactive shell

docker run -i --name auth -t auth

Save image

docker save auth:latest | gzip > docker-auth.tar.gz

Load pre-built image

docker load < docker-auth.tar.gz

Using Authentikit

We provide a few examples of authenticated data structures implemented using Authentikit: merkle.ml, redblack.ml, and trimerkle.ml. Further, we show the usage of the Merkle tree in test.ml.

Running make in the src/basic/ folder generates a binary file test and running ./test will execute the test suite.