This repository accompanies the paper "Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS⁺", authored by Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, and Pierre-Yves Strub. The original (proceeding's) version of the paper can be found here; the most recent version of the paper can be found here.
This repository comprises EasyCrypt scripts primarily aimed at the formal verification of the security of XMSS as a standalone construction — specified in RFC 8391. Due to the modular approach taken in the formal verification, the scripts contain an independent formal verification of the fix of the security proof of SPHINCS⁺ presented in Recovering the Tight Security Proof of SPHINCS⁺, validating the remediation of the flaw in the original proof and paving the way for a complete formal verification of SPHINCS⁺. Furthermore, again due to the modular approach, the scripts contain an independent formal verification of a security property of XMSS as a component of SPHINCS⁺.
Currently, the latest version of EasyCrypt that has been confirmed to verify the scripts in this repository corresponds to the following commit of the main branch of the EasyCrypt repository: commit eaba09c215c28b292259bd61aaf575bf7d21dbfe.
This repository is structured as follows.
proofs/: All scripts relevant to the formal verification of the security of XMSS (both as standalone and as a component of SPHINCS⁺) and the fix of the security proof of SPHINCS⁺.acai/(abstract context address indices): Scripts comprising a version of the proofs that completely abstracts away (the indices corresponding to) the part of the addresses that is not directly used/manipulated in the executed operations (i.e., the part that may be used to, for example, differentiate the context in an encompassing structure).DigitalSignatures.eca: (Library) Generically defines signature schemes (both stateless and key-updating) and their security notions.DigitalSignaturesROM.eca: (Library) Similar toDigitalSignatures.eca, except that it defines everything with respect to a random oracle (this is for proofs in the random oracle model).EUFRMA_Interactive_Equiv.ec: Demonstrates equivalence between the regular EUF-RMA property for digital signature schemes and its (auxiliary) interactive variant.FL_XMSS_TW.ec: Provides the context, specification, and proofs concerning fixed-length XMSS-TW.HashAddresses.eca: Generically defines hash addresses and some of their properties (not a proper library: relatively minimal and primarily designed for use in this and related projects).HashThenSign.eca: Demonstrates generic results concerning the hash-then-sign paradigm for digital signature schemes.KeyedHashFunctions.eca: (Library) Generically defines keyed hash functions and their properties.Reprogramming.ec: Demonstrates a generic bound for the reprogramming technique (for a random oracle).TweakableHashFunctions.eca: (Library) Generically defines tweakable hash functions and their properties.WOTS_TW.ec: Provides the context, specification, and proofs concerning WOTS-TW (with an abstract encoding).WOTS_TW_Checksum.ec: Defines the concrete encoding used in WOTS-TW and demonstrates that the proofs fromWOTS_TW.ecstill hold true when using this encoding.XMSS_TW.ec: Provides the context, specification, and proofs concerning XMSS-TW.
fsai/(fully specified address indices): Scripts comprising a version of the proofs that entirely specifies the (indices contained in the) addresses. More precisely, it considers the (relevant) indices used for the addresses in SPHINCS⁺. The files in this directory are identically named to those in theacai/directory (except that this directory does not contain theHashAddresses.ecfile); indeed, each of these files is analogous (in purpose) to its similarly-named counterpart in theacai\directory.