[TLS] Re: New Version Notification for draft-usama-tls-risks-of-mlkem-00.txt

[Nadim Kobeissi <[e-mail]>]

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 <Peter.C=[e-mail]> 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 -- [e-mail] <mailto:[e-mail]>
> To unsubscribe send an email to [e-mail] <mailto:[e-mail]>