Enhancing Security for XMSS and SPHINCS+ Using Machine-Checked Methods
Advanced cryptographic techniques such as XMSS and SPHINCS+ are critical for ensuring secure digital signatures in a post-quantum world. This project focuses on improving the security and verification processes of XMSS and SPHINCS+ using machine-checked methods, aiming to enhance trust in these crucial cryptographic schemes while facilitating future formal verifications. The research addresses issues such as security proofs, hash function properties, and the setup of verification mechanisms. The use of computer-aided cryptography and formal verification techniques plays a key role in this endeavor.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ Manuel Barbosa / Fran ois Dupressoir / Benjamin Gr goire / Andreas H lsing / Matthias Meijers / Pierre-Yves Strub
Context Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Context 2
XMSS (eXtended Merkle Signature Scheme) Stateful hash-based digital signature scheme Fixed length Building block (SPHINCS+) Arbitrary length Standalone (RFC 8391) First standardized post-quantum signature scheme (NIST SP 800-208) Mistake in security proof for SPHINCS+, also affects XMSS 4 years until discovery Fix for SPHINCS+, not for XMSS Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Context | XMSS (eXtended Merkle Signature Scheme) 3
Computer-Aided Cryptography Cryptographic constructions and proofs are complex Broken designs, proofs, and implementations Alleviate through computers Reduce complexity Enforce rigor Shift trust EasyCrypt Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Context | Computer-Aided Cryptography 4
Purpose and Contribution Increase confidence in security of XMSS and SPHINCS+ Fix and verify security proof for XMSS Verify fix and setup verification of security proof for SPHINCS+ Facilitate future formal verification of cryptography Digital signature schemes Hash functions Hash-then-sign paradigm Merkle trees Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Context | Purpose and Contribution 5
Process Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Process 6
Objectives Fix and verify security proof for XMSS EUF-CMA Hash function properties Verify fix and setup verification of security proof for SPHINCS+ Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Process | Objectives 7
Approach Formalize Context and Proof Steps Formally Verify Proof Devise Proof = Without Tool = With Tool Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Process | Approach 8
Devise Proof Scheme (Key Generation) Combine OTS and Merkle tree Public key = Combineand Hash Secret key = Key Compression State = 0 WOTS Public Key Hash Chains WOTS Secret Key Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Process | Devise Proof Scheme (Key Generation) 9
Devise Proof Scheme (Signing and Verification) Message compression Sig = (state, , ) Authentication Path Increment state Verification by reconstruction and comparison of public key WOTS Signature Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Process | Devise Proof Scheme (Signing and Verification) 10
Devise Proof Proof Structure Setup SPHINCS+ Fix SPHINCS+ Nonce Generation PRF Key Compression TCR Chain Hash TCR Fixed-length XMSS EUF-RMA XMSS EUF-CMA WOTS Chain Hash UD M-EUF-GCMA ROM Message Compression CR Tree Hash TCR Chain Hash PRE Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Process | Devise Proof Proof Structure 11
Formalize Context and Proof Steps Context Parameters Types, functions, and distributions (Merkle trees) Schemes (hash-then-sign) Proof steps (and corresponding artifacts) Security notions (digital signatures) and hardness properties (hash functions) Adversary classes and reduction adversaries Games Proof steps Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Process | Formalize Context and Proof Steps 12
Formally Verify Proof M-EUF-GCMA of WOTS Hybrid argument XMSS EUF-CMA Nonce Generation PRF Fixed-length XMSS EUF-RMA Message Compression CR EUF-RMA of fixed-length XMSS Authentication path collision Key Compression TCR WOTS Tree Hash TCR EUF-CMA of XMSS Hash-then-sign Random oracle reprogramming M-EUF-GCMA Chain Hash TCR Chain Hash UD Chain Hash PRE Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Process | Formally Verify Proof 13
Future Work and Summary Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Future Work and Summary 14
Future Work Quantum-accessible Random Oracle Model (QROM) SPHINCS+ Hash function instantiations/properties Formally verified implementations EasyCrypt (Formosa Crypto project*) *For more information, see formosa-crypto.org Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Future Work and Summary | Future Work 15
Summary and Statistics Fix and verify security proof for XMSS Verify fix and setup verification of security proof for SPHINCS+ New EasyCrypt libraries Effort 1 intermediate (developing), 5 advanced (guiding), part-time, for 1 year Output ~19000 lines of EasyCrypt code Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+ | Future Work and Summary | Summary and Statistics 16
