On Sat, Jun 6, 2026 at 4:36 PM Eric Rescorla <[email protected]> wrote:
> > > On Sat, Jun 6, 2026 at 7:44 AM Nadim Kobeissi <[email protected]> > wrote: > >> Hi Usama, >> >> Thanks, I wholly agree with your message. >> >> Nadim, perhaps you could propose a PR [2] summarizing your analysis in >> something like one paragraph? >> >> Done: https://github.com/tlswg/draft-ietf-tls-mlkem/pull/20 >> > > Unless I misunderstand what Nadim says his analysis has shown, it mostly > confirms the intuitive analysis that hybrids are secure in the case of > failure of either individual component. I think the previous text captures > this effectively in terms of failure of the PQ component and wouldn't > oppose changing the text state that it applied to failure of the > traditional component as well, but I think this text implies a much > stronger conclusion than is supported by the analysis. > > I wouldn't oppose a factual statement, such as "Machine-checked symbolic > analysis [REF] confirms that PQ/T key establishment is secure [potentially > this could be made more precise] even if either of the components is > compromised." > -Ekr > The formal analysis establishes that hybrid is strictly more robust than standalone. The decision about what type of primitive to fit into their respective “slots” seems like a more open question. To also support John Mattsson’s point regarding the anticipated security collapse of traditional DHE to CRQCs, while acknowledging the risks of the unknown regarding ML-KEM’s longer term resilience, perhaps the text could be word-smithed this way? “Machine-checked symbolic analysis [REF] supports preferring hybrid deployment over standalone key establishment, confirming that hybrid key establishment remains secure under compromise of either individual component.” Cheers, Nathanael
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
