Signal just announced the deployment of their new post-quantum ratcheting protocol, called the Sparse Post-Quantum Ratchet (SPQR), and Cryspen is proud to have contributed to the formal analysis of the design and implementation of this new Signal feature.
The seeds of our collaboration with Signal reach back to 2023, when Signal first published PQXDH, the post-quantum key establishment protocol that marked the beginning of Signal’s post-quantum transition. We helped Signal to formally analyze and improve PQXDH, resulting in a paper at Usenix Security. This time, Cryspen and Signal agreed to collaborate from the very beginning of the design process for SPQR all the way through to its implementation.
The Signal blog post wonderfully describes SPQR and the role formal verification played in its design and implementation. Here, we will briefly note three contributions Cryspen had towards this effort, leaving deeper technical details to a future publication.
Analyzing the SPQR Protocol Design
In our previous analysis of PQXDH, Cryspen collaborated with Charlie Jacomme at Inria and Rolfe Schmidt at Signal to build formal models of the protocol that could be analyzed symbolically by ProVerif and verified computationally by CryptoVerif.
For SPQR, we decided to build models in ProVerif, because the protocol engineers found it easy to read and write ProVerif, and the fully automatic tool provided quick and reliable feedback on each design. We helped Signal engineers write the initial models, but they were able to modify and maintain these models as the protocol underwent a series of revisions until it reached its final form. Using formal verification in this organic way allows protocol designers to quickly try out new ideas, checking if a design change breaks a desired security property. When all the protocol details are settled, the final model can be comprehensively verified for all desired security goals.
The ProVerif models for SPQR are maintained in the SPQR repository and are verified as part of CI.
Providing Post-Quantum Cryptography
The SPQR implementation uses our libcrux implementation of the ML-KEM post-quantum key encapsulation mechanism. Our Rust implementation is formally verified for panic-freedom, functional correctness, and secret independence, and hence provides a high degree of assurance.
Interestingly, Signal’s SPQR design required a novel incremental API for ML-KEM, different from the ones usually provided by crypto libraries. At the request of the Signal developers, we implemented this new API in libcrux and helped them integrate it into the SPQR implementation. See our PR for details on the incremental API, and see this test to understand how to use the API.
Verifying the SPQR Implementation
As the design of SPQR matured, the Signal team started implementing it in Rust. At this stage, we collaborated with them to build a formal verification pipeline for their implementation using hax and its F* proof backend. We helped verify the new code for panic-freedom and some correctness goals.
The hax verification scripts are hosted on the SPQR repository. They run in CI and flag errors whenever a code change breaks some expected invariant and might (say) cause a panic at runtime. These proofs only cover the core of the new SPQR code, and formally verifying the full Signal codebase is still some distance away, but it is already exciting to see how formal proofs like these can be maintained and extended by Signal engineers in the normal course of their work.
This experience taught us a lot about real-world code verification and resulted in several improvements to hax and to our models of the Rust libraries. We are excited to continue collaborating with the Signal team to cover more of the Signal codebase and verify it for more ambitious correctness and security properties in the future.
To learn more about how Cryspen can help you with your cryptographic protocol design or software verification, email us.