Hi Peter, Your clarification is correct. One minor note: in this paper the written-out TLS theorem is the OW-CPA one; the IND-1CCA-suffices statement is a direct consequence of the Dowling et al. proof structure rather than a separately proved theorem here.
Nadim Kobeissi Symbolic Software • https://symbolic.software > On 28 May 2026, at 2:05 PM, Peter C <[email protected]> > wrote: > > OFFICIAL > > Nadim, > > > 1. Huguenin-Dumittan & Vaudenay (eprint 2021/844). This is a > > pen-and-paper game-based proof, not automated verification > > model, which I think is what the FATT is mainly concerned with. > > I'm not sure this characterisation of the FATT is correct. From > the "FATT process overview": > > [The] 'formal' is not limited to formal methods but to formal > security modeling generally. > > > The main theorem shows the TLS 1.3 handshake with the DH key > > exchange replaced by a KEM is secure in the Dowling et al. > > MultiStage model whenever the KEM is OW-CPA. ML-KEM, being > > IND-CCA, trivially satisfies this. The authors themselves note > > the resulting bound is "very much non-tight," and QROM is left > > as an open problem. Effectively, this is qualitative reassurance > > for pure-KEM TLS 1.3, not a tight practical bound. > > The lack of tightness is only due to the OW-CPA assumption. As the > authors note in their introduction: > > Similarly, in the security proof of TLS 1.3 handshake by Dowling > et al. [15], DH key-exchange can be replaced by an IND-1CCA KEM > and the proof would still go through. > > In other words, switching to an IND-CCA KEM is a very simple change > that does not affect the bound. > > Peter > > OFFICIAL > _______________________________________________ > TLS mailing list -- [email protected] <mailto:[email protected]> > To unsubscribe send an email to [email protected] <mailto:[email protected]>
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
