Formally Verified Tight Security Proof for SPHINCS+
Discover a formally verified security proof for the stateless hash-based digital signature scheme SPHINCS+, increasing confidence in its security and facilitating future formal verification with a modularized approach.
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. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
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.
E N D
Presentation Transcript
A Tight Security Proof for SPHINCS+, Formally Verified Manuel Barbosa (FCUP, INESC TEC & MPI-SP) Fran ois Dupressoir (University of Bristol) Andreas H lsing (TU/e & SandboxAQ) Matthias Meijers (TU/e & SandboxAQ) Pierre-Yves Strub (PQShield)
Context A Tight Security Proof for SPHINCS+, Formally Verified | Context 2
SPHINCS+ Stateless hash-based digital signature scheme Post-quantum Standardized as SLH-DSA (by NIST in FIPS 205) Mistake in security proof Discovery: ~3 years after publication Fix (on paper): ~2 years after discovery A Tight Security Proof for SPHINCS+, Formally Verified | Context | SPHINCS+ 3
Computer-Aided Cryptography Cryptography is (increasingly) complex Broken designs, proofs, and implementations Alleviate through computers Reduce complexity Enforce rigor Shift trust EasyCrypt A Tight Security Proof for SPHINCS+, Formally Verified | Context | Computer-Aided Cryptography 4
Purpose and Contribution Increase confidence in security of SPHINCS+ Modularize and granularize security proof Reuse existing artifacts Formally verify reconstructed security proof Generic relation between hash function properties (Bernstein and H lsing, 2019) Facilitate future formal verification Libraries: binary/Merkle trees and hash functions Other: novel proof technique (with reusable results) A Tight Security Proof for SPHINCS+, Formally Verified | Context | Purpose and Contribution 5
Process A Tight Security Proof for SPHINCS+, Formally Verified | Process 6
Objectives Formally verify security proof for SPHINCS+ EUF-CMA Hash function properties A Tight Security Proof for SPHINCS+, Formally Verified | Process | Objectives 7
Approach Formalize Context and Proof Steps Construct Proof Formally Verify Proof = Without Tool = With Tool A Tight Security Proof for SPHINCS+, Formally Verified | Process | Approach 8
Construct Proof Scheme Overview SPHINCS+: XMSSMT (one) + FORS (many) + message compression Fixed-length variant of XMSSMT XMSSMT: Tree of XMSS instances Hypertree structure (size/time trade-off) Used to sign public keys of FORS instances FORS: Forest (sequence) of Merkle trees One instance per leaf of XMSSMT Used to sign messages A Tight Security Proof for SPHINCS+, Formally Verified | Process | Construct Proof Scheme Overview 9
Construct Proof Scheme Overview (XMSS) Merkle tree + OTS (Winternitz) Signature (W)OTS signature Authentication path Combine and Hash Key Compression (W)OTS Public Key (W)OTS Secret Key A Tight Security Proof for SPHINCS+, Formally Verified | Process | Construct Proof Scheme Overview (XMSS) 10
Construct Proof Scheme Overview (XMSSMT) Tree of XMSS instances Bottom instances sign messages (SPHINCS+: FORS public keys) Intermediate instances sign roots of instances below Signature XMSS signatures from instances on path from signing instance to root instance A Tight Security Proof for SPHINCS+, Formally Verified | Process | Construct Proof Scheme Overview (XMSSMT) 11
Construct Proof Scheme Overview (SPHINCS+) XMSSMT + FORS (+ message compression) Message compression determines FORS instance FORS instance signs message XMSSMT signs FORS public key Sign Root Sign Public Key Signature FORS signature (on message) XMSSMT signature (on FORS public key) FORS Public Key FORS Secret Key A Tight Security Proof for SPHINCS+, Formally Verified | Process | Construct Proof Scheme Overview (SPHINCS+) 12
Construct Proof Modularization Multi-instance FORS (M-FORS) Includes message compression Manages all FORS instances SPHINCS+: XMSSMT + M-FORS XMSSMT M-FORS A Tight Security Proof for SPHINCS+, Formally Verified | Process | Construct Proof Modularization 13
Construct Proof Proof Structure SPHINCS+ EUF-CMA Fixed-Length XMSSMT EUF-NAGCMA Secret Key Generation PRF Nonce Generation PRF M-FORS EUF-CMA Key Message Compression ITSR Root WOTS Tree Hash TCR Leaf Hash OpenPRE Tree Hash TCR Compression TCR Compression TCR M-EUF-GCMA Previous Work Chain Hash UD Chain Hash PRE Chain Hash TCR Leaf Hash DSPR Leaf Hash TCR Generic Relation A Tight Security Proof for SPHINCS+, Formally Verified | Process | Construct Proof Proof Structure 14
Formalize Context and Proof Steps Context Parameters Types, functions, and distributions (binary/Merkle trees) Schemes Proof Steps Security notions and hardness assumptions (hash functions) Adversary classes and reduction adversaries Games Probability statements A Tight Security Proof for SPHINCS+, Formally Verified | Process | Formalize Context and Proof Steps 15
Formally Verify Proof Leaf hash Granular, multi-dimensional analysis Complex conditional probability Leaf Hash OpenPRE Leaf Hash DSPR Leaf Hash TCR (Fixed-length) XMSSMT and M-FORS Node-by-node construction of entire structure (through oracle calls) Authentication path collisions Fixed-Length XMSSMT EUF-NAGCMA M-FORS EUF-CMA A Tight Security Proof for SPHINCS+, Formally Verified | Process | Formally Verify Proof 16
Future Work and Summary A Tight Security Proof for SPHINCS+, Formally Verified | Process | Future Work and Summary 17
Future Work Hash function instantiations/properties Formally verified implementations EasyCrypt (Formosa Crypto project*) *For more information, see formosa-crypto.org A Tight Security Proof for SPHINCS+, Formally Verified | Process | Future Work and Summary | Future Work 18
Summary and Statistics Formally verified security proof for SPHINCS+ New/Improved EasyCrypt libraries and novel proof technique Effort 1 main and 4 support/guiding, part-time for about 7 months (excluding reused artifacts) Output ~17000 lines of EasyCrypt code (excluding reused artifacts) A Tight Security Proof for SPHINCS+, Formally Verified | Process | Future Work and Summary | Summary and Statistics 19
