Paper 2026/1230 Original: eprint.iacr.org/2026/1230 ↗

Formula Freshness for Staged Hybrid Authenticated Key Exchange

Abstract

Hybrid post-quantum migration is entering deployed handshake designs, but hybrid KEM security protects only one shared-secret input. It does not by itself say whether handshake, application, exporter, or resumption material remains pseudorandom after branch reveals, stage-key reveals, selective corruptions, or late corruptions. We characterize these staged claims through branch-formula freshness: each stage receives a monotone formula over branch exposure, authentication freshness, transcript binding, KDF ancestry, and explicit non-reveal atoms. Secrecy follows by replacing a surviving branch contribution and then using a labelled HKDF/PRF-style target-hiding argument along a fresh KDF cut; agreement follows separately from authentication binding and injective transcript representation. We also give selector-local accounting, where a fixed admissible witness selector determines which surviving branches and KDF cuts are charged. For scoped TLS 1.3 ECDHE--ML-KEM 1-RTT, we identify the branch-replacement, HKDF-path, and binding assumptions that imply concrete preservation bounds for handshake, application, exporter, and resumption targets.