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] To unsubscribe send an email to [email protected]
