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

[Muhammad Usama Sardar <[e-mail]>]

Hi,

Thank you David, Simon, Nadim, and Jacob for the attestations.

Thank you Ilari for the feedback. You are making good points which I 
have tried to address in the editor's copy.

In general, there seems to be high momentum right now with at least 2 
other WG participants conducting the formal analysis. Typically, finding 
volunteers is the hardest part of this process. Given the interest, 
initiating the FATT review feels like a constructive next step.

Could you also please share your perspective on why 8773bis needed to go 
to FATT but not a paradigm change like standalone ML-KEM?

It is worth noting that FATT review is harmless:

 1. 'Nothing required' is a perfectly valid outcome.
 2. WG is /not/ obliged to follow the recommendation of FATT.

I have added it in the draft [3] anyway for those who may be worried.

If there is any ambiguity, I can explain it further when I take the 
floor in Vienna.

> I do not think there is any justification for doing FATT process for
> stand-alone ML-KEM, but not for X25519MLKEM768.
I have added a few justifications [0] in the draft. Could you please 
share the specific issues you see in [0]? That may not be very 
satisfying for a cryptographer, but I don't see anything wrong from a 
/symbolic/ perspective. If we put in all details of cryptography in the 
model, the /symbolic/ analysis may become redundant with the 
/computational/ model, and hence may become a duplicate effort losing 
the real complementary benefit /symbolic/ analysis could bring.
>   Any flaw in integration
> of the former is highly likely to directly translate into a flaw in the
> latter — due to the hybrid property.
Sure, if we find a flaw which applies to hybrid, then [1] applies, e.g., 
chairs may do a quick WGLC and IETF LC requesting to keep its place in 
publication queue.
> However, I think it is extremely unlikely that any such flaws exist.
One of the motivations of formal analysis is to test things we assume to 
be highly likely. There are so many examples from history here.

>   The
> arguments about "some level of symmetry" are unsound.
You are right. That was admittedly very informal and with sincere 
apologies, I revoke the quoted attestation, and have tried to make it 
more precise. What I meant was DHKE part remains symmetric as before -- 
at least from symbolic analysis perspective, which is what I am 
currently interested in.

Additional PQ component is concatenated to it.

> Moreover, I do not think it is possible to prove soundness of
> X25519MLKEM768 without proving soundness of stand-alone ML-KEM — as
> soundness of X25519MLKEM768 includes it having hybrid property, meaning
> it is still secure if ML-KEM is secure, no matter how throughly X25519
> is destroyed.
 From such soundness, doesn't it naturally follow that hybrids are at 
least as strong as the stronger of the two components?If such a 
statement is added, I believe that addresses the concerns of some.

> And who in the IETF community do you trust to determine that?
Anyone in the IETF community -- and more broadly in the world -- who 
will do ProVerif confirmation for the minimal viable modeling [2] that 
we have collectively found on the list and will answer any questions I 
may have. IIUC, at least two other WG participants are already working 
on it.

> I support initiating the FATT process here, and I support the work 
> Usama is doing to use symbolic models to better understand the 
> protocol's security properties. Even where existing proofs give us 
> confidence, having an explicit symbolic analysis of the standalone-KEM 
> case is the kind of thing that's worth doing rather than assuming, and 
> there are clearly participants willing to do it.
>
> +1 from me.
Thank you for your attestation.

> +1
>
> The entire idea behindhttps://github.com/tlswg/tls-fatt  seems like a
> good thing, and I wonder what would warrant side-step it.
Thank you for your attestation.

> In particular, I am curious to see how the FATT process will reconcile 
> NIST's requirements with TLS's choices.
>
> For example, does TLS with ML-KEM now require a NIST certified DRBG?

I have added it in [2] for WG discussion. /Computational/ analysis may 
be helpful here. I think it will be good to state it clearly in the 
security considerations of draft-ietf-tls-mlkem.

> I don't see any mention of patents in your draft. This seems 
> concerning when the world-wide patent waiver license applies only to 
> the exact specification which I understand imposes using a NIST 
> certified DRBG.
>
> Hopefully you will also include at least a basic analysis of these 
> matters. 
It was unintentional miss as I am not a patent expert to do a proper 
analysis but I have mentioned it in [4].

Best regards,

-Usama


[0] 
https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-fatt-review-for-hybrid-key-

[1] 
https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-what-if-issue-is-found

[2] 
https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-minimum-viable-modeling

[3] 
https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-fatt-review-is-harmless

[4] 
https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-patents