Re: [TLS] ML-KEM key agreement for TLS 1.3

2024-03-05 Thread Andrey Jivsov
> > I would treat non-hybrid drafts in IETF the same way > as "export" options in code: they're security risks. I would encourage > explicit withdrawal of any such drafts. Does this point apply in your opinion to hash-based signatures? ___ TLS mailing

Re: [TLS] ML-KEM key agreement for TLS 1.3

2024-03-05 Thread D. J. Bernstein
The security analysis of post-quantum crypto is far less mature than the security analysis of ECC was when the Internet moved to ECC: * 48% of the 69 round-1 submissions to the NIST post-quantum competition in 2017 have been broken by now. * 25% of the 48 submissions unbroken during

Re: [TLS] Proposal: a TLS formal analysis triage panel

2024-03-05 Thread Deirdre Connolly
> it's unclear to me whether this review would be a hard requirement to pass WGLC. Let's say a document makes it to that stage, and it is sent to the triage panel, but the panel never produces a formal analysis of it. (This could happen for example if the researchers don't find the extension at

[TLS] ML-KEM key agreement for TLS 1.3

2024-03-05 Thread Deirdre Connolly
I have uploaded a preliminary version of ML-KEM for TLS 1.3 and have a more fleshed out version to be uploaded when datatracker opens. It is a straightforward new

Re: [TLS] Proposal: a TLS formal analysis triage panel

2024-03-05 Thread David Schinazi
Hi Deirdre, Thanks for this, I think this is a great plan. From the perspective of standards work, more formal analysis is always better, and this seems like a great way to motivate such work. That said, it's unclear to me whether this review would be a hard requirement to pass WGLC. Let's say a

[TLS] Proposal: a TLS formal analysis triage panel

2024-03-05 Thread Deirdre Connolly
A few weeks ago, we ran a WGLC on 8773bis, but it basically came up blocked because of a lack of formal analysis of the proposed changes. The working group seems to be in general agreement that any changes to TLS 1.3 should not degrade or violate the existing formal analyses and proven security