Secrecy in Squirrel and the Post-Compromise Security of a Ratchet

This repository contains the additional material for the paper"Secrecy in Squirrel and the Post-Compromise Security of a Ratchet",Clément Hérouard, Charlie Jacomme, Adrien Koutsos, Joseph Lallemand, CCS 2026. ## Organization The artifacts include:- case-studies/: the Squirrel developments (see below for details);- squirrel-prover/: our secrecy logic extension of Squirrel;- docker/: configuration and script to build the Docker image;- squirrel-secrecy.tar: pre-built Docker image. ## HTML Files The case studies can be browsed through without installing anyadditional software using the HTML proof exports incase-studies/html_reports/. For each case study, this directorycontains a corresponding HTML file that allows to interactivelyre-execute the proofs step by step by clicking on the proof lines toexecute. These files only display in an interactive way the output previouslyproduced by Squirrel on a given Squirrel input file, but do not re-checkthat the proofs are correct -- they are provided for convenience, but do notconstitute a proof in themselves.These exports are static and do not allow to interactively modify the proofs. ## Case Studies The main claims of the papers can be found in the following places: - case-studies/asym-ratchet/ contains the asymmetric ratchet case study of Section 5 (cf. corresponding README). - case-studies also contains the Squirrel model and proof for the motivating example of Section 2 (motivating-example.sp), as well as a small introductory tutorial teaching basic manipulations of the secrecy predicate (weak_secrecy_tuto.sp); - squirrel-prover/theories/WeakSecrecy.sp, which has been integrated inside Squirrel's standard library, notably contains proofs for some soundness rules (Theorem C.2 and C.3). ## Reproduction with Docker Provided that docker isinstalled, the followinginstructions allow to reproduce our results: 1 - Load the docker image squirrel-secrecy.tar using docker load --input squirrel-secrecy.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-secrecy:latest bash. 3 - Run all our examples by executing make in the case-studies/ directory. Depending on the available ressources and currentdocker configuration,some case-studies may fail due to a timeout. If such a timeout occurs,one may go into the case-studies/asym-ratchet folder and then run sed -i '1s/^/set smtSteps=10000000./' model.sp which adds a special configuration line in the model file. Re-runningmake should then succeed. ## Reproduction from Sources 1 - 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/squirrel 3 - Run examples. To run all our examples, execute make in the case-studies/ directory.