Manuel Barbosa
University of Porto (FCUP) and INESC TEC, Porto, Portugal

François Dupressoir
University of Bristol, Bristol, United Kingdom

Rui Fernandes
Max Planck Institute for Security and Privacy, Bochum, Germany

Andreas Hülsing
Eindhoven University of Technology, Eindhoven, Netherlands; SandboxAQ, Palo Alto, USA

Matthias Meijers
Eindhoven University of Technology, Eindhoven, Netherlands

Pierre-Yves Strub
PQShield SAS, Paris, France

Keywords: XMSS, EasyCrypt, Jasmin, hash-based signatures, formal verification

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 XMSSMT written in Jasmin, targeting the amd64 architecture. Beyond the implementations, we provide formal EasyCrypt specifications of XMSS and XMSSMT, 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 preexisting formalization.