Paper 2026/134

Completing the Chain: Verified Implementations of Hash-Based Signatures and Their Security

François Dupressoir, University of Bristol

Rui Fernandes, Max Planck Institute for Security and Privacy

Andreas Hülsing, Eindhoven University of Technology, SandboxAQ

Matthias Meijers, Eindhoven University of Technology

Pierre-Yves Strub, PQShield

Abstract

We present the first formally verified implementation of a hash-based signature scheme that is linked to a machine-checked proof of security. Specifically, we provide reference implementations of XMSS and XMSS$^{\textrm{MT}}$ written in Jasmin, targeting the AMD64 architecture. Beyond the implementations, we provide formal EasyCrypt specifications of XMSS and XMSS$^{\textrm{MT}}$, transcribed from RFC~8391, and prove that our implementations adhere to these specifications. Furthermore, for XMSS, we give a machine-checked proof that our specification of RFC~8391 refines the abstract specification proven secure in EasyCrypt by Barbosa, Dupressoir, Grégoire, Hülsing, Meijers and Strub [CRYPTO'23]. In particular, we prove the security of our specification via a reduction, demonstrating that breaking our specification contradicts the [CRYPTO'23] result for our instantiation. Consequently, our implementation is not only functionally correct, but also adheres to a specification that is proven secure. The core technical challenge in our work resides in bridging low-level implementations of TreeHash algorithms with high-level functional specifications used in the pre-existing formalization.

@misc{cryptoeprint:2026/134,
      author = {Manuel Barbosa and François Dupressoir and Rui Fernandes and Andreas Hülsing and Matthias Meijers and Pierre-Yves Strub},
      title = {Completing the Chain: Verified Implementations  of Hash-Based Signatures and Their Security},
      howpublished = {Cryptology {ePrint} Archive, Paper 2026/134},
      year = {2026},
      url = {https://eprint.iacr.org/2026/134}
}