Robust Logical Foundations for Mechanizing Post-Quantum Cryptography in Squirrel

This repository contains the artifacts for the paper David Baelde, Antoine Dallon, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos: Robust Logical Foundations for Mechanizing Post-Quantum Cryptography in Squirrel CCS 2026## OrganizationThe artifacts include:- artifact-appendix.pdf: the artifact appendix of the paper;- case-studies/: the Squirrel developments (see case-studies/README.md for more details);- squirrel/: our post-quantum extension of Squirrel;- docker/: configuration and script to build the Docker image;- squirrel.tar: pre-built Docker image.## HTML FilesThe case-studies/html/ sub-directory contains HTML versions of theSquirrel developments that can be consulted from a web browser,without installing Squirrel.## Reproduction with DockerProvided that docker isinstalled, the followinginstructions allow to reproduce our results:1 - Load the docker image squirrel.tar using docker load --input squirrel.tar. Alternatively, the docker image may be built from scratch by running ./docker/build.sh.2 - Once the docker image is loaded, run docker run -it sp/squirrel-prover:latest bash.3 - Run all our examples by executing make in the case-studies/ directory.## Reproduction from Sources1 - Build Squirrel. First build the squirrel prover, whose source code is in squirrel/. See squirrel/README.md for dependencies and build instructions. Note that building with SMT support is mandatory for some of our examples. These developments were checked using CVC5 (version 1.0.8) and Z3 (version 4.13.2). 2 - Add Squirrel to the PATH. export PATH=$PATH:/path/to/squirrel3 - Run examples. To run all our examples, execute make in the case-studies/ directory.