MIME-Version: 1.0
References: <E3248C6C-F41D-4697-B484-5DD3B3F03893@symbolic.software>
 <cec4e220-0842-486d-9c69-ddaf37260da4@tu-dresden.de>
 <CAK08nYaa4+dTkuyeBK8648nV=VFTt=AbdKbAbz4xR3X_MnssnA@mail.gmail.com>
In-Reply-To: 
 <CAK08nYaa4+dTkuyeBK8648nV=VFTt=AbdKbAbz4xR3X_MnssnA@mail.gmail.com>
From: Songbo Bu <king347608@gmail.com>
Date: Sat, 6 Jun 2026 15:22:59 +0800
Message-ID: 
 <CAK08nYbYvW7rWWzkJaq7uKNfUjUniOjB0eGAX1euUHumRpC4kg@mail.gmail.com>
To: tls@ietf.org
Content-Type: multipart/alternative; boundary="00000000000048ed2d065390a6a2"
Message-ID-Hash: PYS6YLRMDXPKKQ7TK4RUD7FZIB3IJYXG
Precedence: list
Subject: =?utf-8?q?=5BTLS=5D_Re=3A_FATT_Chance=3A_On_the_Robustness_of_Standalone_and?=
 =?utf-8?q?_Hybrid_ML-KEM_Key_Exchange_in_TLS_1=2E3?=
Archived-At: 
 <https://mailarchive.ietf.org/arch/msg/tls/Rbd-GNSgvY0w3SyIGdY2Z0aU93s>

--00000000000048ed2d065390a6a2
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Hi all,

Following up on the implementation-test point, I think the artifact would
be most useful if kept small and explicitly non-blocking: a list of
negative cases implementers can run against hybrid key exchange code, not a
condition for progressing the draft.

The cases I would start with are:

   - the negotiated group is hybrid, but one component is missing,
   malformed, or associated with a different group;
   - ECDHE and KEM values are individually valid, but assembled from
   different handshakes or transcript contexts;
   - a peer attempts to continue as standalone ECDHE or standalone ML-KEM
   after a hybrid group was negotiated;
   - the implementation derives application traffic secrets before both
   components have been validated and accepted under the negotiated hybrid
   group;
   - the implementation accepts a hybrid share while logging or exporting
   enough state to make it look like only one component was used.

This would not be a formal analysis result. It is just a practical bridge
from the model=E2=80=99s intended binding property to things that are easy =
for
implementations to accidentally get wrong.

If others think this is worth capturing, I=E2=80=99d be happy to help turn =
the list
into a GitHub issue or small PR once the cases are clearer.

Best,
Songbo Bu

On Fri, 5 Jun 2026 09:31:27 +0800, Songbo Bu king347608@gmail.com wrote:

Hi Usama, all,

Thanks. I agree this should not make the draft depend on a full new test
suite before progressing. The useful near-term thing may just be to collect
a small set of negative cases that implementers can run against the
existing artifacts.

The cases I would start with are roughly:

   -

   negotiated hybrid group differs from the group encoded/bound in either
   component;
   -

   one component is omitted, malformed, or fails decapsulation/validation;
   -

   KEM and ECDHE values are individually valid but assembled from different
   handshakes/transcripts;
   -

   a peer attempts to continue as standalone ML-KEM or standalone ECDHE
   after a hybrid group was negotiated;
   -

   application traffic secrets are derived only after both components have
   been accepted under the negotiated hybrid group.

That is not a formal proof obligation, but it would make the intended =E2=
=80=9Cboth
components are bound and accepted=E2=80=9D property easier to check in
implementations. If there is a preferred place for such cases =E2=80=93 dra=
ft text,
a GitHub issue, or a separate test-artifact note =E2=80=93 I can help shape=
 it
there.

Best,

Songbo Bu

On Thu, 4 Jun 2026 21:48:32 +0200, Muhammad Usama Sardar
muhammad_usama.sardar@tu-dresden.de wrote:

Hi Nadim,

Awesome work. Thanks a lot. That resolves my concern.

Before we put this discussion behind us, I would like to suggest

that:

-

we put artifacts in front of FATT for evaluation: It would be

good to have the artifacts evaluated once, so that we can keep

using them in the future for all PQ extensions.

-

we add a statement on preference of hybrids and refer to the

paper in the security considerations of draft-ietf-tls-mlkem.

1 would be nice =E2=80=93 the earlier the better. But IMHO 2 is

essential.

One small note: I noticed that in your paper, you cite link to

editor=E2=80=99s copy [0]. I have published -02 [1] =E2=80=93 in the state =
it was

=E2=80=93 for you to have a permanent citation, because the editor=E2=80=99=
s copy

will keep changing =E2=80=93 and has already moved to the next steps =E2=80=
=93

and it might be confusing for the reviewers/readers to find a

mismatch in the paper and the reference. -02 is just for you;

others don=E2=80=99t need to worry about it and there is nothing new to

read in it.

One implementation-facing angle that may

be worth spelling out, even if it is outside what the symbolic

model can prove, is which negative tests would best catch

hybrid-specific integration mistakes.

I think this is very valuable and practically useful suggestion to

craft tests and folks are welcome to work on it. But I am more

than happy with what has been achieved. Thanks Nadim.

Any kind of Undefined Behavior in implementation would compromise both.

I believe one can actually do formal verification on the real code

to have high assurance that there is no Undefined Behavior.

I think some of the informal claims are stronger than what

this paper proves. This does not matter for ML-KEM or ECC hybrids

thereof =E2=80=94 but could matter for another KEM.

Could you please explicitly share those differences?

Note that once a CRQC emerges, which some people say may

happen very soon, [=E2=80=A6]

and some people have argued it may never occur [2]

I think formal analysis in the not so distant future should

focus on quantum attackers and treat ECC and RSA as not

providing any security.

Once the WG agrees on setting them to =E2=80=98N=E2=80=99 or =E2=80=98D=E2=
=80=99 probably that

will be the appropriate time to update the formal models.

Many TLS libraries enforce handshake timeouts, so unless the

key exchange algorithm is completely broken, an attacker

cannot practically keep a connection open long enough to forge

the Finished message.

Is the handshake timeout typically pre-configured or dynamically

selected? Does anyone have datapoints on handshake timeout in

common TLS libraries?

Actually, some people propose remote attestation within the

handshake, which requires significantly increasing the timeout. In

particular, it adds the time for generation and appraisal of

Evidence within the handshake, which gives the adversary plenty of

time to do a lot of interesting things.

It is great that TLS WG have clarified that static keys MUST

NOT be used for key exchange. This significantly lower the

risk for these kind of attacks.

Agree. It would have been beneficial to do it long time ago, but

better late than never.

Best regards,

-Usama

[0]

https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risk=
s-of-mlkem.html

[1]

https://datatracker.ietf.org/doc/draft-usama-tls-risks-of-mlkem/02/

[2]

https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-02.html#sect=
ion-6.4

--00000000000048ed2d065390a6a2
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><p>Hi all,</p>
<p>Following up on the implementation-test point, I think the artifact woul=
d be most useful if kept small and explicitly non-blocking: a list of negat=
ive cases implementers can run against hybrid key exchange code, not a cond=
ition for progressing the draft.</p>
<p>The cases I would start with are:</p>
<ul>
<li>the negotiated group is hybrid, but one component is missing, malformed=
, or associated with a different group;</li>
<li>ECDHE and KEM values are individually valid, but assembled from differe=
nt handshakes or transcript contexts;</li>
<li>a peer attempts to continue as standalone ECDHE or standalone ML-KEM af=
ter a hybrid group was negotiated;</li>
<li>the implementation derives application traffic secrets before both comp=
onents have been validated and accepted under the negotiated hybrid group;<=
/li>
<li>the implementation accepts a hybrid share while logging or exporting en=
ough state to make it look like only one component was used.</li>
</ul>
<p>This would not be a formal analysis result. It is just a practical bridg=
e from the model=E2=80=99s intended binding property to things that are eas=
y for implementations to accidentally get wrong.</p>
<p>If others think this is worth capturing, I=E2=80=99d be happy to help tu=
rn the list into a GitHub issue or small PR once the cases are clearer.</p>
<p>Best,<br>
Songbo Bu</p>
<p>On Fri, 5 Jun 2026 09:31:27 +0800, Songbo Bu <a href=3D"mailto:king34760=
8@gmail.com" target=3D"_blank">king347608@gmail.com</a> wrote:</p>
<blockquote>
<p>Hi Usama, all,</p>
<p>Thanks. I agree this should not make the draft depend on a full new test=
 suite before progressing. The useful near-term thing may just be to collec=
t a small set of negative cases that implementers can run against the exist=
ing artifacts.</p>
<p>The cases I would start with are roughly:</p>
<ul>
<li>
<p>negotiated hybrid group differs from the group encoded/bound in either c=
omponent;</p>
</li>
<li>
<p>one component is omitted, malformed, or fails decapsulation/validation;<=
/p>
</li>
<li>
<p>KEM and ECDHE values are individually valid but assembled from different=
 handshakes/transcripts;</p>
</li>
<li>
<p>a peer attempts to continue as standalone ML-KEM or standalone ECDHE aft=
er a hybrid group was negotiated;</p>
</li>
<li>
<p>application traffic secrets are derived only after both components have =
been accepted under the negotiated hybrid group.</p>
</li>
</ul>
<p>That is not a formal proof obligation, but it would make the intended =
=E2=80=9Cboth components are bound and accepted=E2=80=9D property easier to=
 check in implementations. If there is a preferred place for such cases =E2=
=80=93 draft text, a GitHub issue, or a separate test-artifact note =E2=80=
=93 I can help shape it there.</p>
<p>Best,</p>
<p>Songbo Bu</p>
<p>On Thu, 4 Jun 2026 21:48:32 +0200, Muhammad Usama Sardar <a href=3D"mail=
to:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_usama.sa=
rdar@tu-dresden.de</a> wrote:</p>
<p>Hi Nadim,</p>
<p>Awesome work. Thanks a lot. That resolves my concern.</p>
<p>Before we put this discussion behind us, I would like to suggest</p>
<p>that:</p>
<p>-</p>
<p>we put artifacts in front of FATT for evaluation: It would be</p>
<p>good to have the artifacts evaluated once, so that we can keep</p>
<p>using them in the future for all PQ extensions.</p>
<p>-</p>
<p>we add a statement on preference of hybrids and refer to the</p>
<p>paper in the security considerations of draft-ietf-tls-mlkem.</p>
<p>1 would be nice =E2=80=93 the earlier the better. But IMHO 2 is</p>
<p>essential.</p>
<p>One small note: I noticed that in your paper, you cite link to</p>
<p>editor=E2=80=99s copy [0]. I have published -02 [1] =E2=80=93 in the sta=
te it was</p>
<p>=E2=80=93 for you to have a permanent citation, because the editor=E2=80=
=99s copy</p>
<p>will keep changing =E2=80=93 and has already moved to the next steps =E2=
=80=93</p>
<p>and it might be confusing for the reviewers/readers to find a</p>
<p>mismatch in the paper and the reference. -02 is just for you;</p>
<p>others don=E2=80=99t need to worry about it and there is nothing new to<=
/p>
<p>read in it.</p>
<p>One implementation-facing angle that may</p>
<p>be worth spelling out, even if it is outside what the symbolic</p>
<p>model can prove, is which negative tests would best catch</p>
<p>hybrid-specific integration mistakes.</p>
<p>I think this is very valuable and practically useful suggestion to</p>
<p>craft tests and folks are welcome to work on it. But I am more</p>
<p>than happy with what has been achieved. Thanks Nadim.</p>
<p>Any kind of Undefined Behavior in implementation would compromise both.<=
/p>
<p>I believe one can actually do formal verification on the real code</p>
<p>to have high assurance that there is no Undefined Behavior.</p>
<p>I think some of the informal claims are stronger than what</p>
<p>this paper proves. This does not matter for ML-KEM or ECC hybrids</p>
<p>thereof =E2=80=94 but could matter for another KEM.</p>
<p>Could you please explicitly share those differences?</p>
<p>Note that once a CRQC emerges, which some people say may</p>
<p>happen very soon, [=E2=80=A6]</p>
<p>and some people have argued it may never occur [2]</p>
<p>I think formal analysis in the not so distant future should</p>
<p>focus on quantum attackers and treat ECC and RSA as not</p>
<p>providing any security.</p>
<p>Once the WG agrees on setting them to =E2=80=98N=E2=80=99 or =E2=80=98D=
=E2=80=99 probably that</p>
<p>will be the appropriate time to update the formal models.</p>
<p>Many TLS libraries enforce handshake timeouts, so unless the</p>
<p>key exchange algorithm is completely broken, an attacker</p>
<p>cannot practically keep a connection open long enough to forge</p>
<p>the Finished message.</p>
<p>Is the handshake timeout typically pre-configured or dynamically</p>
<p>selected? Does anyone have datapoints on handshake timeout in</p>
<p>common TLS libraries?</p>
<p>Actually, some people propose remote attestation within the</p>
<p>handshake, which requires significantly increasing the timeout. In</p>
<p>particular, it adds the time for generation and appraisal of</p>
<p>Evidence within the handshake, which gives the adversary plenty of</p>
<p>time to do a lot of interesting things.</p>
<p>It is great that TLS WG have clarified that static keys MUST</p>
<p>NOT be used for key exchange. This significantly lower the</p>
<p>risk for these kind of attacks.</p>
<p>Agree. It would have been beneficial to do it long time ago, but</p>
<p>better late than never.</p>
<p>Best regards,</p>
<p>-Usama</p>
<p>[0]</p>
<p><a href=3D"https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-=
usama-tls-risks-of-mlkem.html" target=3D"_blank">https://muhammad-usama-sar=
dar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html</a></p>
<p>[1]</p>
<p><a href=3D"https://datatracker.ietf.org/doc/draft-usama-tls-risks-of-mlk=
em/02/" target=3D"_blank">https://datatracker.ietf.org/doc/draft-usama-tls-=
risks-of-mlkem/02/</a></p>
<p>[2]</p>
<p><a href=3D"https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlke=
m-02.html#section-6.4" target=3D"_blank">https://www.ietf.org/archive/id/dr=
aft-usama-tls-risks-of-mlkem-02.html#section-6.4</a></p>
</blockquote>
</div>

--00000000000048ed2d065390a6a2--