From f1603bea874ce9ae144cb47924c42cc511adabd2 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Wed, 22 Jul 2026 23:02:40 +0200 Subject: [PATCH] audit catch 2: the oracle boundary is FIVE, not six MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The skeleton-era docs said 'six hash oracles' including prf — written before the cone analysis showed prf/prf_msg are sign-side only. The extracted model and FunsExternal carry exactly FIVE oracle axioms (h_msg, f, h, t_l, t_len); the documented boundary now matches the real one in README, TRUSTED-BASE, and extract.sh. Caught by the post-flip drill's cross-consistency pass. Co-Authored-By: Claude Fable 5 --- README.md | 5 +++-- TRUSTED-BASE.md | 5 +++-- verification/extract.sh | 4 ++-- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 85d7435..aa80f4f 100644 --- a/README.md +++ b/README.md @@ -56,8 +56,9 @@ slh_verify -> slh_verify_internal ``` Key generation and signing are out of scope (trusted base), exactly as -ed25519 signing was. The six hash oracles (`h_msg, prf, f, h, t_l, -t_len` — SHA-2 instantiations) are opaque external models with written +ed25519 signing was. The five verify-path hash oracles (`h_msg, f, h, +t_l, t_len` — SHA-2 instantiations; `prf`/`prf_msg` are sign-side only +and never enter the cone) are opaque external models with written justifications, kept outside every certificate's dependency cone (honesty invariant H4); their semantics are the standing SHA-2 oracle boundary documented in [TRUSTED-BASE.md](TRUSTED-BASE.md). diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index da13d58..7fa7660 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -3,8 +3,9 @@ Initial statement, written at skeleton time (nothing proven yet); this file is maintained as the campaign proceeds and is part of every claim. -1. **The six hash oracles.** `h_msg, prf, f, h, t_l, t_len` - (SLH-DSA-SHA2-128s instantiations over SHA-256) are modeled as opaque +1. **The five verify-path hash oracles.** `h_msg, f, h, t_l, t_len` + (SLH-DSA-SHA2-128s instantiations over SHA-256; `prf`/`prf_msg` are + sign-side only and do not appear in the cone) are modeled as opaque functions with assumed functional behavior. Their correctness against FIPS 180-4 is NOT proven here — the same standing boundary as SHA-512 in the ed25519 apex. A collision or misimplementation inside the hash diff --git a/verification/extract.sh b/verification/extract.sh index 8f474a7..84b89cc 100755 --- a/verification/extract.sh +++ b/verification/extract.sh @@ -4,8 +4,8 @@ # SCOPE: the SLH-DSA verify path, parameter set SLH-DSA-SHA2-128s # roots: slh_verify(_internal), fors_pk_from_sig, ht_verify, # xmss_pk_from_sig, wots_pk_from_sig, chain -# (sign/keygen are out of scope; the six hash oracles are opaque — -# see TRUSTED-BASE.md.) +# (sign/keygen are out of scope; the five verify-path hash oracles +# (h_msg, f, h, t_l, t_len) are opaque — see TRUSTED-BASE.md.) # # Rust --charon--> SlhVerify.llbc --aeneas--> gen/SlhVerify/*.lean #