Lune

CCS2026

A Formal Analysis of Signal’s Sparse Post-Quantum Ratchet Protocol and its Implementation

Karthikeyan Bhargavan, Maxime Buyse, Graeme Connell, Franziskus Kiefer, Rolfe Schmidt

出版方

摘要

This is an artifact for reproducing the results presented in the ACM CCS 2026 paper "A Formal Analysis of Signal’s Sparse Post-Quantum Ratchet Protocol and its Implementation". The artifact includes simulations for various candidate protocols described in the paper, hand-written ProVerif models for SPQR, and instructions for formally analyzing SPQR source code for runtime safety (using F*) and protocol security (using ProVerif). The README describes the artifact in more detail, and provides instructions on how to reproduce the results in the paper.