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

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^MT written in Jasmin, targeting the AMD64 architecture. Beyond the implementations, we provide formal EasyCrypt specifications of XMSS and XMSS ^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.