Paper 2026/1230
Formula Freshness for Staged Hybrid Authenticated Key Exchange
, IRT SystemXAbstract
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.
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Preprint.
- Keywords
- Authenticated Key ExchangeHybrid Key ExchangePost-Quantum CryptographyMulti-Stage Key Exchange
- Contact author(s)
-
anis bkakria @ irt-systemx fr
chadrel-chrislain bafouetila @ irt-systemx fr - History
- 2026-06-11: revised
- 2026-06-10: received
- See all versions
- Short URL
- https://ia.cr/2026/1230
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2026/1230,
author = {Anis Bkakria and Merland Chrislain Chadrel BAFOUETILA},
title = {Formula Freshness for Staged Hybrid Authenticated Key Exchange},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/1230},
year = {2026},
url = {https://eprint.iacr.org/2026/1230}
}
