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

[Peter C <[e-mail]>]

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