MIME-Version: 1.0
References: <5f361893-bc32-4737-9578-fdb3ad7be3f9@tu-dresden.de>
 <9F03163D-B0F9-40DD-A4AB-69C151B872D6@aiven.io>
 <c4a0c433-173d-44ac-bd48-eed642a674d3@tu-dresden.de>
 <CAHxYnaOBMnPp7EiRLNYWX8AQDc2zYoBL226nfeBiPXsyii7Now@mail.gmail.com>
 <CAHxYnaOFWQBLf0Pn8bY=CMx7ytSEkTbvj7xp-s0GCHJohRh5xg@mail.gmail.com>
 <MRWPR02MB1208667A0653CF2C6B141933DB7CD2@MRWPR02MB12086.eurprd02.prod.outlook.com>
 <76b504ae-5692-4f31-a9d2-025974b12339@tu-dresden.de>
 <MRWPR02MB1208652B214687BB93253F1D2B7CD2@MRWPR02MB12086.eurprd02.prod.outlook.com>
 <5fb42c5c-825b-472b-8455-ce893011ade5@tu-dresden.de>
 <MRWPR02MB12086E888B91ECDB72D4B230AB7CC2@MRWPR02MB12086.eurprd02.prod.outlook.com>
 <CAHxYnaPYKJ_jdbVXraoXQootU4KeaSsmE8Dh0r=RLkZUqcaFqg@mail.gmail.com>
 <CAHxYnaOovbOJkp_og6rzs05hw_3zUKPWaufr5tukCaxizQY7FA@mail.gmail.com>
In-Reply-To: 
 <CAHxYnaOovbOJkp_og6rzs05hw_3zUKPWaufr5tukCaxizQY7FA@mail.gmail.com>
From: Nathanael Ritz <nathanritz@gmail.com>
Date: Tue, 28 Jul 2026 12:51:30 -0600
Message-ID: 
 <CAHxYnaNtzCqEm19r+0pwRZCWKykXHiWLXK_DsaSU9D+mqkf3sw@mail.gmail.com>
To: "seat@ietf.org" <seat@ietf.org>
Content-Type: multipart/alternative; boundary="000000000000701e830657b05409"
Message-ID-Hash: TFNKBXEANK33Z3UZ7XEYOVSGZDXNOA46
CC: "ufmrg@irtf.org" <ufmrg@irtf.org>,
 Muhammad Usama Sardar <muhammad_usama.sardar@tu-dresden.de>
Precedence: list
Subject: =?utf-8?q?=5BUfmrg=5D_Re=3A_=5BSeat=5D_Re=3A_Comments_on_formal_analysis_of_?=
 =?utf-8?q?relay_attacks_in_attested_TLS_=28CVE-2026-33697=29?=
Archived-At: 
 <https://mailarchive.ietf.org/arch/msg/ufmrg/Iv4vGTStFDgchtxoMdxvzEQAZio>

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

Hello,

I have additional comments to offer to this thread.

Comments are offered below with [NR]:

On Tue, 28 Jul 2026 at 10:00, Muhammad Usama Sardar <
muhammad_usama.sardar@tu-dresden.de> wrote:

> Hi Nathanael,
>
> This does not address any of the questions in [5] where your working was
> shown to be not correct, and these inaccuracies still remain here too.
>
[NR}: I disagree, but the authors are welcome to cite my work and my words
directly in relationship to any questions that are, in their opinion, left
unanswered so that I can address them directly rather than guessing.

> For clarity, nothing has changed in the key schedule of TLS 1.3 for quite
> long time (I think draft-20 which became RFC8446). Saying that RFC9846 is
> "new work" for key schedule is almost surely wrong. Maybe Ekr can confirm=
.
>
[NR]: If it is being stated that I am suggesting RFC9846 includes 'new work
for key schedule', please quote me directly, as I am currently unclear to
what context and statements are being referenced to right now.

> On 28.07.26 16:48, Nathanael Ritz wrote:
>
> In Usama's July 6 email [0], I was invited to present a formal
> counter-example to Section 9 of the paper. The `binder6` model
> (`tls-lib-simple.pvl`) provides that exact counter-example by addressing
> the core architectural requirements:
>
> Following the requests of many other WG/RG participants (e.g., [7]), the
> email [0] clearly asks for a *property* that:
>
>    1. the hybrid construction (intra- + post-handshake attestation) *can*=
 satisfy,
>    but
>    2. post-handshake attestation alone *cannot* satisfy
>
> What you are changing is the model and not presenting a property.
>
[NR]: It's fine to suggest such specificy, but it is plainly not possible
to present a property demonstrating what post-handshake attestation alone
cannot satisfy without either A) changing the model to demonstrate
post-handshake or B) moving to a seperate model altogether. Therefore, I do
not believe it is reasonable to suggest that my simple changes to the
existing model are somehow out of scope for demonstrating a direct
counter-example to the paper's otherwise unfalsifiable claim that "it may
not be possible to achieve strong application-traffic (level 3) binding
using intra-handshake attestation alone."

> So either the link [0] is wrong or else this needs a clarification. So is
> your claim that the three binding properties *cannot* be achieved by
> post-handshake attestation alone?
>
I think that claim is very easily falsifiable. So I am not sure what new
> information you are bringing on the table.
>
> Which specific statement in Sec. 9 of the paper [6] do you claim to have
> found a counter-example?
>
[NR]: Once again, *this model demonstrates that it is possible to achieve
strong application-traffic (level 3) binding using intra-handshake
attestation alone.* This is why I supplied the full verification run, which
includes the optional properties demonstrating that they also return true
where the previous models returned false.

> 2. Infrastructure identity is preserved in `rdata`: Binding `pubLTK` and
> `ID_S` directly inside the hardware-signed quote payload (`rdata`) anchor=
s
> infrastructure identity through the Attestation Key (`privAK`) itself. Th=
is
> secures identity without altering `CertificateVerify` or modifying the TL=
S
> 1.3 state machine.
>
> The problem here is that this does not provide proof-of-possession of
> privLTK, while CertificateVerify does exactly that.
>

[NR]: That's correct. CertificateVerify provides proof-of-possession.

> 3. Key schedule compliance: Using the standard handshake traffic write
> keys `(ksh, kch)` inside `rdata` binds the evidence to the handshake stat=
e
> at `ServerHello` while leaving the HKDF derivation tree 100% compliant wi=
th
> RFC 9846 =C2=A77.1.
>
> I am not sure reusing the keys intended for a specific purpose is helpful=
.
>
[NR]: It is demonstrably useful. Tying pubLTK and ID_S into the rdata nonce
provides the required binding, and the PoP proves it. This is why the G1
through G3 properties demonstrate a common correlation between the conveyed
Evidence and the secrets.

> This will not be visible in ProVerif but I think this will probably break
> the computational proofs of TLS 1.3. I think we would need to check with
> TLS WG if they are fine with it.
>
[NR]: I simply do not follow this idea as it's been presented. I think it
would be productive to present concrete technical details on this rather
than offering another unfalsifiable suggestion that somehow storing data
with a physical hw register (such as where REPORT_DATA is sent) could
affect computational proofs when it is not used as input to the key
schedule.

> Best regards,
>
> Usama, Slava, and Jean-Marie
>
> [0]
> https://mailarchive.ietf.org/arch/msg/seat/T78G1TFWqcj3O9vrCvNihcn8QeU/
>
> [1]
> https://mailarchive.ietf.org/arch/msg/seat/S3l-tc-pnfHs9rcAfeuMGyVzW1Q/
>
> [2]
> https://mailarchive.ietf.org/arch/msg/seat/RhYelVXkqUDKa3CKLvkqQU4Z23M/
>
> [3]
> https://github.com/nathanaelritz/intra-handshake-paper/tree/3719fddd7cf0b=
e930d1c256bac1096f7c53494f0/proposal
>
> [4]
> https://github.com/nathanaelritz/intra-handshake-paper/commit/3719fddd7cf=
0be930d1c256bac1096f7c53494f0#diff-8ffc30d09ebb6bc1fd9df2ae48d0a0bc0289582e=
a40c99f6c2ea66ee738f189d
>
> [5]
> https://mailarchive.ietf.org/arch/msg/seat/dKVqaL8RJSQLonIEmtzrDYEXEAU/
>
> [6]
> https://www.researchgate.net/publication/408219182_Intra-handshakefail_CV=
E-2026-33697_High-severity_CVE_in_Attested_TLS
>
> [7]
> https://mailarchive.ietf.org/arch/msg/seat/2_aGylmFHoLmqN7BBcYVoH-rNJk/
> _______________________________________________
> Seat mailing list -- seat@ietf.org
> To unsubscribe send an email to seat-leave@ietf.org


Cheers,
Nathanael

[8]
https://github.com/nathanaelritz/intra-handshake-paper/blob/nr-proposal-pat=
ch/proposal/verification_results_full.txt

-------------------
From: Muhammad Usama Sardar <muhammad_usama.sardar@tu-dresden.de>
Date: Tue, 28 Jul 2026 at 10:00
Subject: [Seat] Re: Comments on formal analysis of relay attacks in
intra-handshake attestation (CVE-2026-33697)
To: seat@ietf.org <seat@ietf.org>
Cc: ufmrg@irtf.org <ufmrg@irtf.org>


Hi Nathanael,

This does not address any of the questions in [5] where your working was
shown to be not correct, and these inaccuracies still remain here too. For
clarity, nothing has changed in the key schedule of TLS 1.3 for quite long
time (I think draft-20 which became RFC8446). Saying that RFC9846 is "new
work" for key schedule is almost surely wrong. Maybe Ekr can confirm.
On 28.07.26 16:48, Nathanael Ritz wrote:

In Usama's July 6 email [0], I was invited to present a formal
counter-example to Section 9 of the paper. The `binder6` model
(`tls-lib-simple.pvl`) provides that exact counter-example by addressing
the core architectural requirements:

Following the requests of many other WG/RG participants (e.g., [7]), the
email [0] clearly asks for a *property* that:

   1. the hybrid construction (intra- + post-handshake attestation)
*can* satisfy,
   but
   2. post-handshake attestation alone *cannot* satisfy

What you are changing is the model and not presenting a property. So either
the link [0] is wrong or else this needs a clarification. So is your claim
that the three binding properties *cannot* be achieved by post-handshake
attestation alone? I think that claim is very easily falsifiable. So I am
not sure what new information you are bringing on the table.

Which specific statement in Sec. 9 of the paper [6] do you claim to have
found a counter-example?

2. Infrastructure identity is preserved in `rdata`: Binding `pubLTK` and
`ID_S` directly inside the hardware-signed quote payload (`rdata`) anchors
infrastructure identity through the Attestation Key (`privAK`) itself. This
secures identity without altering `CertificateVerify` or modifying the TLS
1.3 state machine.

The problem here is that this does not provide proof-of-possession of
privLTK, while CertificateVerify does exactly that.

3. Key schedule compliance: Using the standard handshake traffic write keys
`(ksh, kch)` inside `rdata` binds the evidence to the handshake state at
`ServerHello` while leaving the HKDF derivation tree 100% compliant with
RFC 9846 =C2=A77.1.

I am not sure reusing the keys intended for a specific purpose is helpful.
This will not be visible in ProVerif but I think this will probably break
the computational proofs of TLS 1.3. I think we would need to check with
TLS WG if they are fine with it.

Best regards,

Usama, Slava, and Jean-Marie

[0] https://mailarchive.ietf.org/arch/msg/seat/T78G1TFWqcj3O9vrCvNihcn8QeU/

[1] https://mailarchive.ietf.org/arch/msg/seat/S3l-tc-pnfHs9rcAfeuMGyVzW1Q/

[2] https://mailarchive.ietf.org/arch/msg/seat/RhYelVXkqUDKa3CKLvkqQU4Z23M/

[3]
https://github.com/nathanaelritz/intra-handshake-paper/tree/3719fddd7cf0be9=
30d1c256bac1096f7c53494f0/proposal

[4]
https://github.com/nathanaelritz/intra-handshake-paper/commit/3719fddd7cf0b=
e930d1c256bac1096f7c53494f0#diff-8ffc30d09ebb6bc1fd9df2ae48d0a0bc0289582ea4=
0c99f6c2ea66ee738f189d

[5] https://mailarchive.ietf.org/arch/msg/seat/dKVqaL8RJSQLonIEmtzrDYEXEAU/

[6]
https://www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-=
2026-33697_High-severity_CVE_in_Attested_TLS

[7] https://mailarchive.ietf.org/arch/msg/seat/2_aGylmFHoLmqN7BBcYVoH-rNJk/
_______________________________________________
Seat mailing list -- seat@ietf.org
To unsubscribe send an email to seat-leave@ietf.org

--------------------
From: Nathanael Ritz <nathanritz@gmail.com>
Date: Tue, 28 Jul 2026 at 08:48
Subject: Re: [Seat] Re: Comments on formal analysis of relay attacks in
attested TLS (CVE-2026-3369)
To: seat@ietf.org <seat@ietf.org>
Cc: ufmrg@irtf.org <ufmrg@irtf.org>


Hello,

Top posting. In Usama's July 6 email [0], I was invited to present a formal
counter-example to Section 9 of the paper. The `binder6` model
(`tls-lib-simple.pvl`) provides that exact counter-example by addressing
the core architectural requirements:

1. Dual signatures (`CV_Ext`) are unnecessary: The removal of `CV_Ext` was
deliberate=E2=80=94to prove that non-standard dual transcript signatures ar=
e
completely redundant for achieving G1 through G3 correlation.

2. Infrastructure identity is preserved in `rdata`: Binding `pubLTK` and
`ID_S` directly inside the hardware-signed quote payload (`rdata`) anchors
infrastructure identity through the Attestation Key (`privAK`) itself. This
secures identity without altering `CertificateVerify` or modifying the TLS
1.3 state machine.

3. Key schedule compliance: Using the standard handshake traffic write keys
`(ksh, kch)` inside `rdata` binds the evidence to the handshake state at
`ServerHello` while leaving the HKDF derivation tree 100% compliant with
RFC 9846 =C2=A77.1. While Usama's stated position is well noted, as shared =
on
the list in Markus's recent thread [1], this WG will continue to work with,
and continue to leverage new work, from the TLSWG -- as it's been discussed
on-list before [2].

That said, I am happy to demonstrate the same result presented under
`proposal/`, which binds to G2 already. That variation is available to
review at [3] and yields the expected outcome:

```ocaml
(* All sanity/reachability checks passing *)

Query event(ClientStateEv(ev,gxy1)) && event(ServerStateEv(ev,gxy2)) =3D=3D=
>
gxy1 =3D gxy2 is true.

Query event(ClientStateEvKch(ev,kch1)) && event(ServerStateEvKch(ev,kch2))
=3D=3D> kch1 =3D kch2 is true.

Query event(ClientStateEvKc(ev,kc1)) && event(ServerStateEvKc(ev,kc2)) =3D=
=3D>
kc1 =3D kc2 is true.
```

The exact same pattern to lock in the fix was required [4]: populating
`rdata` to include `ID_S` and `pubLTK` directly inside the hardware quote
to anchor infrastructure identity, while stripping the redundant `selfsign`
payload out of `CRT` (which was a primary source of ProVerif
counter-examples). In this case, I left the non-standard `CV_Ext` construct
completely untouched, as the previously presented model already
demonstrated it to be superfluous.

Cheers,
Nathanael


[0] https://mailarchive.ietf.org/arch/msg/seat/T78G1TFWqcj3O9vrCvNihcn8QeU/

[1] https://mailarchive.ietf.org/arch/msg/seat/S3l-tc-pnfHs9rcAfeuMGyVzW1Q/

[2] https://mailarchive.ietf.org/arch/msg/seat/RhYelVXkqUDKa3CKLvkqQU4Z23M/

[3]
https://github.com/nathanaelritz/intra-handshake-paper/tree/3719fddd7cf0be9=
30d1c256bac1096f7c53494f0/proposal

[4]
https://github.com/nathanaelritz/intra-handshake-paper/commit/3719fddd7cf0b=
e930d1c256bac1096f7c53494f0#diff-8ffc30d09ebb6bc1fd9df2ae48d0a0bc0289582ea4=
0c99f6c2ea66ee738f189d


On Mon, 27 Jul 2026 at 12:57, Muhammad Usama Sardar <
muhammad_usama.sardar@tu-dresden.de> wrote:

> Hi Nathanael,
>
> We will be happy to review your artifacts if you would be more precise. A=
s
> it is now, there seems to be nothing concrete that we could utilize to
> improve the artifacts. You seem to criticize #2 but then use the same in
> your code. Something useful may be to revert #1, and show a fix for #2 th=
at
> you propose. We can then check the proposed change. Hopefully, you can
> clarify your perspective more precisely.
> On 27.07.26 13:55, Nathanael Ritz wrote:
>
> Top posting, following up on Markus's latest comments regarding the
> counter-examples for "Level 3" binding and whether handshake secret
> correlation holds across the entire session.
>
> As just clarified to Markus, the distinction between *handshake secret*
>  and *handshake traffic secrets* is critical in TLS 1.3 key schedule.
>
> I recently evaluated a streamlined model that strips out the non-standard
> dual-signed `CV_Ext` construct and the redundant ephemeral self-signature=
s,
> reverting to a clean, standard TLS 1.3 `CV(sg)` message signed solely by
> the ephemeral key.
>
> Removing the second signature, the client may get no guarantee of the
> infrastructure owner and diversion attacks may apply [3,4].
>
> Crucially, it binds the full security context=E2=80=94`(handshake_secret,=
 ID_S,
> pubLTK, pubEK)`=E2=80=94directly into the TEE-signed quote (`rdata`) [0].
>
> There is a potential risk though. The Target Environment needs to send
> handshake_secret to the Attesting Environment.
>
> ## 2. Other non-conformant Key Schedule issues
>
> When examining how the binder functions to correlate these secrets, I
> found the original model introduces two explicit key schedule modificatio=
ns
> that are completely absent from standard TLS and would produce
> non-conformant values the moment they are wired up in real implementation=
s:
>
> We are not aware of ProVerif code wired up in real implementation. It is
> typically an abstraction reasonable for the problem at hand. Could you
> please share some reference where ProVerif was wired up in real
> implementation?
>
> * **`kdf_exp` derives an exporter from the Handshake Secret:**  The
> construction derives an exporter directly from `hs`. RFC 9846 =C2=A77.5 p=
ermits
> only `early_exporter_secret` or `exporter_secret` as the exporter input,
> defining a strict two-stage construction: `Derive-Secret(Secret, label,
> "")` followed by `HKDF-Expand-Label(., "exporter", Hash(context_value))`.
> The modeled `kdf_exp` inserts a non-standard third stage, chaining `"h ex=
p
> master"` into an `"ra binder"` intermediate.
>
> We don't really see your point. Can you explain why having an additional
> Derive-Secret stage is problematic or what attack vectors it leads to? Wh=
at
> impact does removing it make in ProVerif? And if you have discovered a
> security problem, you may like to report to TLS WG because it would likel=
y
> have implications beyond our work since this is how the TLS 1.3 key
> schedule is built, and several researchers have done both the symbolic an=
d
> computational proofs of it.
>
> The paper never claims to be using standard or early exporters of RFC9846=
.
> In fact, using the former would pretty much become post-handshake
> attestation. As even the title of the paper says, the paper is about
> intra-handshake attestation.
>
> * **`kdf_es` returns `exp0` in place of `ems0`:** The model replaces the
> early exporter master secret (`ems0`) with `exp0`.
>
> We believe early_exporter_secret ("ems0") is correctly generated. The
> macro instead returns early exporter value "exp0" which was required. We
> don't see anything wrong in this modeling. Please clarify what you view a=
s
> wrong.
>
> While the shape resembles =C2=A77.5, it forces the early exporter into a
> handshake where `psk =3D NoPSK` in both roles=E2=80=94violating =C2=A77.5=
's requirement
> that implementations use `exporter_secret` unless explicitly specified by
> the application.
>
> This seems to be misunderstanding. "PSK" is always there in the key
> schedule, whether the handshake is PSK-based or not. In the former case, =
it
> has a value generated from previous connection. In the latter case, it ha=
s
> a value of '0'.
>
> Furthermore, it freezes the label and context into the schedule rather
> than exposing them to the application, while discarding `ems0` entirely s=
o
> no standard exporter can be derived downstream.
>
>
>    1. There is no application here. We are modeling in ProVerif.
>    2. early_exporter_secret 'ems0' is not discarded. The early exporter
>    value 'exp0' is indeed derived from 'ems0', returned and used.
>    3. early_exporter_secret 'ems0' has nothing to do with the standard
>    exporter.
>
> In any case, the demonstrated model uses `kch` and `ksh` directly within
> the rdata field, completely leaving the key schedule entirely untouched
> while using something derived from the handshake secret, as Markus had
> proposed.
>
> No field in Table 2 of [3] uses 'kch' or 'ksh' in rdata.
>
> ## 3. Omission of WebPKI and Host Validation
>
> One of the CertificateVerify is for exactly this purpose. So this point
> does not apply.
>
> Best regards,
>
> Usama, Slava, and Jean-Marie
>
>
> [0]
> https://github.com/nathanaelritz/intra-handshake-paper/commit/b5a79aff30d=
23c5169578acc92c6d6ff8147ed21#diff-31622704269a7b23066be433f93cb8eda0a33d4b=
793e2d72bc057a85b135f3e1
>
> [1]
> https://github.com/nathanaelritz/intra-handshake-paper/blob/b5a79aff30d23=
c5169578acc92c6d6ff8147ed21/binder6/full_verification_results.txt
>
> [2]
> https://github.com/nathanaelritz/intra-handshake-paper/tree/b5a79aff30d23=
c5169578acc92c6d6ff8147ed21/binder6
>
> [3]
> https://www.researchgate.net/publication/398839141_Identity_Crisis_in_Con=
fidential_Computing_Formal_Analysis_of_Attested_TLS
>
> [4] https://github.com/CCC-Attestation/formal-spec-id-crisis
>
-------------------
From: Nathanael Ritz <nathanritz@gmail.com>
Date: Mon, 27 Jul 2026 at 05:55
Subject: Re: [Seat] Re: Comments on formal analysis of relay attacks in
attested TLS (CVE-2026-3369)
To: Markus Rudy <mr=3D40edgeless.systems@dmarc.ietf.org>
Cc: Muhammad Usama Sardar <muhammad_usama.sardar@tu-dresden.de>,
seat@ietf.org <seat@ietf.org>, ufmrg@irtf.org <ufmrg@irtf.org>


Hello

Top posting, following up on Markus's latest comments regarding the
counter-examples for "Level 3" binding and whether handshake secret
correlation holds across the entire session. Following a previous
invitation to take a deeper look into the queries for the newer models, I
want to share some concrete analytical results that directly support
Markus's intuition.

I recently evaluated a streamlined model that strips out the non-standard
dual-signed `CV_Ext` construct and the redundant ephemeral self-signatures,
reverting to a clean, standard TLS 1.3 `CV(sg)` message signed solely by
the ephemeral key. Crucially, it binds the full security
context=E2=80=94`(handshake_secret, ID_S, pubLTK, pubEK)`=E2=80=94directly =
into the
TEE-signed quote (`rdata`) [0].


## 1. Evaluation of G1 through G3: Markus's Intuition Holds

When we evaluate the binding properties, the symbolic results diverge
noticeably from the negative expectations previously annotated in the
repository, without adding any explicit cryptographic caveats about typical
assumptions. Based on this model revision, Goals G1 through G3 are show to
weakly hold between the traffic keys and the evidence:


```ocaml
(* Reachability/sanity checks *)
Query not (event(ClientStateEv(ev,gxy_2)) &&
event(ServerStateEv(ev,gxy_2))) is false.

Query not (event(ClientStateEvKch(ev,kch_4)) &&
event(ServerStateEvKch(ev,kch_4))) is false.

Query not (event(ClientStateEvKc(ev,kc_4)) &&
event(ServerStateEvKc(ev,kc_4))) is false.

(* Binding goals *)
Query event(ClientStateEv(ev,gxy1)) && event(ServerStateEv(ev,gxy2)) =3D=3D=
>
gxy1 =3D gxy2 is true.

Query event(ClientStateEvKch(ev,kch1)) && event(ServerStateEvKch(ev,kch2))
=3D=3D> kch1 =3D kch2 is true.

Query event(ClientStateEvKc(ev,kc1)) && event(ServerStateEvKc(ev,kc2)) =3D=
=3D>
kc1 =3D kc2 is true.
```


Contrary to the assumption that Level 3 binding cannot be achieved without
violating protocol boundaries, ProVerif shows that when the handshake
secret and host identity are cryptographically anchored in the TEE quote,
endpoints accepting the same evidence are demonstrated to share identical
application traffic keys. Markus's argument holds: while the binding
material is generated earlier during the handshake, authenticating the
entire handshake state after session establishment successfully protects
the application traffic secrets.

Furthermore, evaluating Compound Authentication (`G-CA1`) in this model
reveals that injective agreement holds even when ephemeral key leakage
(`LeakedEK`) is permitted [1].


## 2. Other non-conformant Key Schedule issues

When examining how the binder functions to correlate these secrets, I found
the original model introduces two explicit key schedule modifications that
are completely absent from standard TLS and would produce non-conformant
values the moment they are wired up in real implementations:

* **`kdf_exp` derives an exporter from the Handshake Secret:**  The
construction derives an exporter directly from `hs`. RFC 9846 =C2=A77.5 per=
mits
only `early_exporter_secret` or `exporter_secret` as the exporter input,
defining a strict two-stage construction: `Derive-Secret(Secret, label,
"")` followed by `HKDF-Expand-Label(., "exporter", Hash(context_value))`.
The modeled `kdf_exp` inserts a non-standard third stage, chaining `"h exp
master"` into an `"ra binder"` intermediate.

* **`kdf_es` returns `exp0` in place of `ems0`:** The model replaces the
early exporter master secret (`ems0`) with `exp0`. While the shape
resembles =C2=A77.5, it forces the early exporter into a handshake where `p=
sk =3D
NoPSK` in both roles=E2=80=94violating =C2=A77.5's requirement that impleme=
ntations use
`exporter_secret` unless explicitly specified by the application.
Furthermore, it freezes the label and context into the schedule rather than
exposing them to the application, while discarding `ems0` entirely so no
standard exporter can be derived downstream.

Even if these changes were fine actually, I'm not sure why they would
otherwise be necessary.

This is in addition to the non-standard introduction of a dual-signature
CV_ext message.

In any case, the demonstrated model uses `kch` and `ksh` directly within
the rdata field, completely leaving the key schedule entirely untouched
while using something derived from the handshake secret, as Markus had
proposed.


## 3. Omission of WebPKI and Host Validation

It's worth noting, the demonstrated model completely forgoes webPKI and
`pubCA` validation while still holding the tested G1, G2 and G3 goals. In
the real world, I think it makes architectural sense to establish a
distinct proof of liveness tied to the TEE without needing to replace
webPKI itself, allowing the connection signing key to continue leveraging
standard certificate chains.

The full set of changes can be found here at [2].

Cheers,
Nathanael


[0]
https://github.com/nathanaelritz/intra-handshake-paper/commit/b5a79aff30d23=
c5169578acc92c6d6ff8147ed21#diff-31622704269a7b23066be433f93cb8eda0a33d4b79=
3e2d72bc057a85b135f3e1

[1]
https://github.com/nathanaelritz/intra-handshake-paper/blob/b5a79aff30d23c5=
169578acc92c6d6ff8147ed21/binder6/full_verification_results.txt

[2]
https://github.com/nathanaelritz/intra-handshake-paper/tree/b5a79aff30d23c5=
169578acc92c6d6ff8147ed21/binder6


-------------------
From: Markus Rudy <mr=3D40edgeless.systems@dmarc.ietf.org>
Date: Mon, 27 Jul 2026 at 02:32
Subject: [Seat] Re: Comments on formal analysis of relay attacks in
attested TLS (CVE-2026-3369)
To: Muhammad Usama Sardar <muhammad_usama.sardar@tu-dresden.de>,
seat@ietf.org <seat@ietf.org>
Cc: ufmrg@irtf.org <ufmrg@irtf.org>


Hi Usama,

> I think we are largely talking past each other.

I agree - let's try to understand where and why.

> 1. Unless I am misunderstanding something, that is not really "missing"
in the paper since that is the proposed binder in Sec. 7.2 of [0], and the
results are already in Table 4 of [0]. ProVerif artifacts are in folder
'proposal' of [3].

Thanks, I don't know how I managed to miss that, sorry. The paper states:

"We prove in
ProVerif that it achieves level 2 (G2), as shown in Table 4, whereas G3
evaluates
to false. Our observation from the TLS key schedule is that at the point in
time when the intra-HS binder is created, kc is not yet derivable. Based on
this
observation and our extensive discussions with the TLS WG, we believe that
it
may not be possible to achieve level 3 in intra-HS attestation while
preserving
the established security and privacy properties of the TLS protocol."

If G3 evaluates to false, you should be able to provide a counter-example
that shows how an adversary can come in possession of the traffic secrets
while the session is bound to the handshake secret. I'd be interested how
that vector looks like, because it would contradict my proof directly.

> 2. I believe I covered a good number of intuitive arguments in slide 2 of
my SEAT presentation [1].

I think what's missing in that slide are two observations:

- If the handshake secret is known to the attacker, that attacker can
compromise the application traffic secrets. So the handshake secret
security is not "irrelevant for security goals".
- The server may not be authenticated at the point where evidence is
generated, but it is authenticated after the TLS handshake completes.
That's my argument: if you look at the entire state of the TLS session,
after it's created, it's enough to observe binding to the handshake secret
and authenticating the server as in standard TLS.

> 3. I'm not sure what question you are trying to settle for SEAT, where
the charter says [...]

This discussion came up several times on the list, and I don't think
"deriving a binder from a TLS key" is considered an extension of the key
schedule by everyone. Is EKM an extension of the key schedule, too?
Deriving another key from the exported key material?

> Thanks for the clarification. I believe Table 4 in [0] has clear
counter-examples to your argument. For instance, there are binders which
satisfy G1 but not G2 and G3.

I'm sorry to say, but that is a table with emojis, not a clear
counter-example. You may be aware of the concrete counter examples, but
they are not very accessible in their current form. It would be
enlightening to see the actual counter-examples, because then we could
understand whether we're missing considerations from standard TLS security
in the formal analysis.

> Just to make sure you are looking at the right figure, I mentioned Fig. 3
of [0] which is the protocol and not the TLS key schedule. So I am not sure
why you are mentioning "not part of the TLS key schedule."

Sorry for the imprecision, but I was hoping the rest of my mail somehow
conveyed the message: this is not specific to TLS! Nothing changes in that
picture! Assurance of non-LEK is guaranteed out of band!

I'm going to answer the following questions from my product's POV, but
there may be other interpretations that make sense.

> 1. What exactly is the server identity in your view?

The hardware identity (Platform instance identity for TDX). This is unique,
bound to a specific server and can't be forced by an attacker on different
hardware.

> 2. Who assigns this identity?

Intel.

> 3. How is that identity supplying entity trusted?

I'm going to interpret this as "how is the PIID known to the verifier",
since the ID supplier is trusted anyway in this case. Two ways:

- I'm running my own datacenter, and when I set up a new server I record
the PIID into my verifier database.
- I'm running on hardware provided by my CSP. The CSP can simply publish a
list of known PIIDs; or they can cross-sign PCK certificates to endorse the
machines they own and operate (this is what POE does).

> 4. Where in the Evidence is the server identity conveyed? (exact field in
Quote and Report of Intel TDX and AMD SEV-SNP)

This is part of the AK certificates, i.e. the PCK or the VCEK. Which is why
I keep saying that the issue is in remote attestation per se, and can be
mitigated in the verifier. It does not need to be considered in the TLS
integration.

> I am not sure what you are talking about, and how this is related to the
paper and this discussion. We are not comparing with and without TEE. In
the world I live in, security is always evaluated compared to the claimed
security properties. Confidential computing made a claim that there is no
need to trust the cloud provider, and we are saying this is not possible in
the current technologies.

I don't think we need to discuss the discrepancy between marketing and
reality here - we agree on that. However, if we take "Cloud provider does
not need to be trusted to some extent" as a mandatory security property, we
will not be able to produce any secure protocol. This is very intuitive to
understand: the CSP can mount a hardware attack, which is out of scope for
TEE security properties, and either impersonate a TEE or extract secrets
(not only EK, but also the traffic secrets). What I'm saying is that
trusting the CSP does not defeat the purpose of TEEs (at least not
entirely).

Cheers, Markus


-------------------
From: Muhammad Usama Sardar <muhammad_usama.sardar@tu-dresden.de>
Date: Sun, 26 Jul 2026 at 17:31
Subject: [Seat] Re: Comments on formal analysis of relay attacks in
attested TLS (CVE-2026-3369)
To: Markus Rudy <mr@edgeless.systems>, seat@ietf.org <seat@ietf.org>
Cc: ufmrg@irtf.org <ufmrg@irtf.org>


Hi Markus,

I think we are largely talking past each other.

Let me summarize what you seem to be saying: you seem to believe that there
are binary levels: level0 (no binding) and level1 (G1 <=3D> G2 <=3D> G3). I=
s
that correct?

On the contrary, we show in paper that there four fine-grained levels:
level0 (no binding); level1 (G1); level2 (G2) and level3 (G3). Results in
Table 4 of [0] provide concrete counter-examples to your levels. We'll
happily clarify this in the extended technical report with intuition and
examples.
On 26.07.26 21:42, Markus Rudy wrote:

If someone thinks a specific binding mechanism is missing that might
lead to different results for intra-handshake attestation, please let
us know, and we will happily share the analysis with the WG.

The binding mechanism I have in mind is the handshake secret, or
something derived from it. Would be nice to see how this breaks down
under formal analysis - I've not seen an argument that would explain
that intuitively.

Thanks, that is helpful. A few notes:

   1. Unless I am misunderstanding something, that is not really "missing"
   in the paper since that is the proposed binder in Sec. 7.2 of [0], and t=
he
   results are already in Table 4 of [0]. ProVerif artifacts are in folder
   'proposal' of [3].
   2. I believe I covered a good number of intuitive arguments in slide 2
   of my SEAT presentation [1]. For example, I removed the whole encryption
   done by handshake traffic key, and nothing changes in the security
   properties of TLS. Doing the same with encryption done by application
   traffic key literally beats the whole purpose of TLS; like why do TLS at
   all if all you want to do is to send application data unencrypted. I don=
't
   know how else to explain it more intuitively. Maybe someone else can phr=
ase
   it better than me.
   3. I'm not sure what question you are trying to settle for SEAT, where
   the charter says (*emphasis* my own):

The attested (D)TLS protocol extension will not modify the (D)TLS
protocol itself. It may define (D)TLS extensions to support its goals
but will not modify, add, or remove any existing protocol messages
or *modify the key schedule*.

    Deriving keys from handshake secret is an extension of the key schedule
which would already violate the SEAT charter.

Please see Sec. 6.4 in paper [0] which explicitly proves it
cryptographically, and let us know what specifically you disagree
with. Just vaguely disagreeing is not very helpful.

I thought I was specific: you proved G3 =3D> G2 =3D> G1, but you don't
prove it strictly, such that G1 =3D!> G3. I'm arguing that G1 <=3D> G2 <=3D=
>
G3, which does not contradict your prove, but makes it more precise.

Thanks for the clarification. I believe Table 4 in [0] has clear
counter-examples to your argument. For instance, there are binders which
satisfy G1 but not G2 and G3.

In the extended technical report, we will add more detailed traces and
intuitive explanations for each binder, and disprove G1 =3D> G2 =3D> G3.

Please see first paragraph of G_3 in Sec. 6.3 in paper [0], which
explains explicitly why it is an essential goal.

What I see in the paper is the following paragraph:

"After establishing an attested TLS connection, the client=E2=80=99s secret=
s
(such as weights and context
data for inference) are encrypted using a key derived from the
client=E2=80=99s application
traffic key atsc. Hence, an essential security goal is to analyze the
correlation
of Evidence with atsc. The derivation of atsc includes handshake messages u=
p
to the server=E2=80=99s F IN. Hence, G3 is at least as strong as G2."

That paragraph is entirely correct! However, it _does not rule out_
that you can _correlate_ to atsc by _binding_ to htsc. This is the
same argument as above: (G1 <=3D> G3) would imply you can bind to any
and correlate to atsc. Note that you are using "at least as strong"
exactly as I mean it: it is as strong, but might not be strictly
stronger.

As a concrete counter-example, there exists a binder (namely the one
proposed in Sec. 7.2 of [0]) which satisfies G1 and G2 but not G3. I
believe I covered a good number of arguments in slide 2 of my SEAT
presentation [1].

Please see #4 in Sec. 7.1 of [0] for several practical reasons. Do we
want that LEK in an unrelated server anywhere in the world breaks our
connection? That is clearly too bad, and the world is probably better
with standard TLS than have such a broken design of attested TLS.

I'm aware that the relay attack for the binding mechanisms you
analyzed applies to any unrelated server being compromised. The
mistake is the assumption that servers are cattle, and that you can't
tell between a server compromised in someones basement and a server at
your contractual $CSP. That, however, is not true: I can configure my
evidence verification to only consider trusted (known) server hardware
in the first place. This is independent of attested TLS, but a
function of the verifier.

I disagree. Developers who are used to TLS must be explicitly given this
guidance. Please see the chartering time discussion where IESG explicitly
requested operational considerations.

Even if you consider configuration outside the scope of attested TLS,
having configuration is insufficient. Somehow the identity of server
hardware must be sent during the protocol to match against the configured
trusted (known) server hardware.

We would be happy if you can share precisely what changes in Fig. 3 of
[0] in the mitigations you have applied.

As I tried to explain several times, including in the post you
responded to: this defect is _not part of the TLS key schedule_ - it's
a shortcoming of remote attestation with current generation of TEEs!
It arises due to the hardware vendors' threat model which does not
cover everything that CC once advertised for. The mitigation removes
the LEK attack vector, which the relay attack relies on.

Just to make sure you are looking at the right figure, I mentioned Fig. 3
of [0] which is the protocol and not the TLS key schedule. So I am not sure
why you are mentioning "not part of the TLS key schedule."

Also, as I mentioned, the statements/presentations/answers of Intel and
what is written in their specifications are all very contradictory.

Continuing the idea of the last response above, I would like to see precise
answers without handwaving to:

   1. What exactly is the server identity in your view?
   2. Who assigns this identity?
   3. How is that identity supplying entity trusted?
   4. Where in the Evidence is the server identity conveyed? (exact field
   in Quote and Report of Intel TDX and AMD SEV-SNP)

Second, this requires trusting the cloud provider, contrary to the
whole claim of confidential computing.

We agree on that in principle, but not everything is so black and
white. Running in a TEE still reduces the attack surface by a lot.
Physical attacks in a hyperscaler datacenter are much harder to
perform than software attacks (bringing a suitcase onto the floor and
hooking up a machine vs. SSHing into it remotely). TEEs still protect
from co-tenants that managed to breach their containment and gain
software root on the hypervisor.

I am not sure what you are talking about, and how this is related to the
paper and this discussion. We are not comparing with and without TEE. In
the world I live in, security is always evaluated compared to the claimed
security properties. Confidential computing made a claim that there is no
need to trust the cloud provider, and we are saying this is not possible in
the current technologies.

Third, what we report is the binding weakness. We do not believe it
can be reasonably eliminated by anything other than changes in the
protocol.

My entire message was about that. I do think there is an option for
binding securely - the handshake secret - and I made both intuitive
and mathematical arguments for why that holds. These should be
countered with examples, rather than beliefs.

Please see my three points in the beginning and please answer them
individually as precisely as possible.

If these CVEs are related to the discussion at hand I'd like to remind
you: Edgeless uses a scheme you publicly call broken (correct), and I
explained the mitigation we're using and why I think this invalidates
the claim, looking at the whole picture. If you think this mitigation
is not enough, you are cordially invited to responsibly disclose the
reason to me, too.

Will follow-up off-list

Best regards,

Usama, Slava, and Jean-Marie

[0] https://www.researchgate.net/publication/408219182_Intra-handshakefail_=
CVE-2026-33697_High-severity_CVE_in_Attested_TLS
[1]: https://datatracker.ietf.org/meeting/126/materials/slides-126-seat-bin=
ding-properties-of-expat-00

[2] https://www.researchgate.net/publication/398839141_Identity_Crisis_in_C=
onfidential_Computing_Formal_Analysis_of_Attested_TLS
[3] https://github.com/muhammad-usama-sardar/intra-handshake.fail

_______________________________________________
Seat mailing list -- seat@ietf.org
To unsubscribe send an email to seat-leave@ietf.org


>

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

<div dir=3D"ltr"><div dir=3D"ltr"><div>Hello,</div><div><br></div><div>I ha=
ve additional comments to offer to this thread.=C2=A0</div><div><br></div><=
div>Comments are offered below with [NR]:</div><br><div class=3D"gmail_quot=
e"><div dir=3D"ltr" class=3D"gmail_attr">On Tue, 28 Jul 2026 at 10:00, Muha=
mmad Usama Sardar &lt;<a href=3D"mailto:muhammad_usama.sardar@tu-dresden.de=
" target=3D"_blank">muhammad_usama.sardar@tu-dresden.de</a>&gt; wrote:<br><=
/div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;bo=
rder-left:1px solid rgb(204,204,204);padding-left:1ex"><u></u><div><p>Hi Na=
thanael,<br></p><p>This does not address any of the questions in [5] where =
your working was shown to be not correct, and these inaccuracies still rema=
in here too.</p></div></blockquote><div>[NR}: I disagree, but the authors a=
re welcome to cite my work and my words directly in relationship to any que=
stions that are, in their opinion, left unanswered so that I can address th=
em directly rather than guessing.=C2=A0</div><blockquote class=3D"gmail_quo=
te" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204=
);padding-left:1ex"><div><p>For clarity, nothing has changed in the key sch=
edule of TLS 1.3 for quite long time (I think draft-20 which became RFC8446=
). Saying that RFC9846 is &quot;new work&quot; for key schedule is almost s=
urely wrong. Maybe Ekr can confirm.<br></p></div></blockquote><div>[NR]: If=
 it is being stated that I am suggesting RFC9846 includes &#39;new work for=
 key schedule&#39;, please quote me directly, as I am currently unclear to =
what context and statements are being referenced to right now.=C2=A0</div><=
blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-l=
eft:1px solid rgb(204,204,204);padding-left:1ex"><div><p></p><div>On 28.07.=
26 16:48, Nathanael Ritz wrote:<br></div><blockquote type=3D"cite"><div dir=
=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr">In Usama&#39;s =
July 6 email [0], I was invited to present a formal counter-example to Sect=
ion 9 of the paper. The `binder6` model (`tls-lib-simple.pvl`) provides tha=
t exact counter-example by addressing the core architectural requirements:<=
br></div></div></div></div></blockquote><p>Following the requests of many o=
ther WG/RG participants (e.g., [7]), the email [0] clearly asks for a=C2=A0=
<b>property</b>=C2=A0that:</p><ol><li>the hybrid construction (intra- + pos=
t-handshake attestation)=C2=A0<i>can</i>=C2=A0satisfy, but<br></li><li>post=
-handshake attestation alone=C2=A0<i>cannot</i>=C2=A0satisfy</li></ol><p>Wh=
at you are changing is the model and not presenting a property.</p></div></=
blockquote><div>[NR]: It&#39;s fine to suggest such specificy, but it is pl=
ainly not possible to present a property demonstrating what post-handshake =
attestation alone cannot satisfy without either A) changing the model to de=
monstrate post-handshake or B) moving to a seperate model altogether. There=
fore,<span style=3D"background-color:transparent">=C2=A0I do not believe it=
 is reasonable to suggest that my simple changes to the existing model are =
somehow out of scope for demonstrating a direct counter-example to the pape=
r&#39;s otherwise unfalsifiable claim that &quot;it may not be possible to =
achieve strong application-traffic (level 3) binding using intra-handshake =
attestation alone.&quot;=C2=A0</span></div><blockquote class=3D"gmail_quote=
" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);=
padding-left:1ex"><div><p>So either the link [0] is wrong or else this need=
s a clarification. So is your claim that the three binding properties=C2=A0=
<i>cannot</i>=C2=A0be achieved by post-handshake attestation alone?</p></di=
v></blockquote><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0p=
x 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><p>I =
think that claim is very easily falsifiable. So I am not sure what new info=
rmation you are bringing on the table.<br></p><p>Which specific statement i=
n Sec. 9 of the paper [6] do you claim to have found a counter-example?<br>=
</p></div></blockquote><div><span style=3D"background-color:transparent">[N=
R]: Once again, <b>this model demonstrates that it is possible to achieve s=
trong application-traffic (level 3) binding using intra-handshake attestati=
on alone.</b> This is why I supplied the full verification run, which inclu=
des the optional properties demonstrating that they also return true where =
the previous models returned false.</span></div><blockquote class=3D"gmail_=
quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,=
204);padding-left:1ex"><div><p></p><blockquote type=3D"cite"><div dir=3D"lt=
r"><div dir=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr">2. Infrastructure ide=
ntity is preserved in `rdata`: Binding `pubLTK` and `ID_S` directly inside =
the hardware-signed quote payload (`rdata`) anchors infrastructure identity=
 through the Attestation Key (`privAK`) itself. This secures identity witho=
ut altering `CertificateVerify` or modifying the TLS 1.3 state machine.<br>=
</div></div></div></div></blockquote>The problem here is that this does not=
 provide proof-of-possession of privLTK, while CertificateVerify does exact=
ly that.<br></div></blockquote><div><br></div><div>[NR]: That&#39;s correct=
. CertificateVerify provides proof-of-possession.=C2=A0</div><blockquote cl=
ass=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid=
 rgb(204,204,204);padding-left:1ex"><div><blockquote type=3D"cite"><div dir=
=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr">3. Key schedule=
 compliance: Using the standard handshake traffic write keys `(ksh, kch)` i=
nside `rdata` binds the evidence to the handshake state at `ServerHello` wh=
ile leaving the HKDF derivation tree 100% compliant with RFC 9846 =C2=A77.1=
.</div></div></div></div></blockquote><p>I am not sure reusing the keys int=
ended for a specific purpose is helpful.</p></div></blockquote><div>[NR]: I=
t is demonstrably useful.=C2=A0<span style=3D"background-color:transparent"=
>Tying pubLTK and ID_S into the rdata nonce provides the required binding, =
and the PoP proves it. This is why the G1 through G3 properties demonstrate=
 a common correlation between the conveyed Evidence and the secrets.=C2=A0<=
/span></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0=
.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><p>This =
will not be visible in ProVerif but I think this will probably break the co=
mputational proofs of TLS 1.3. I think we would need to check with TLS WG i=
f they are fine with it.</p></div></blockquote><div>[NR]: I simply do not f=
ollow this idea as it&#39;s been presented. I think it would be productive =
to present concrete technical details on this rather than offering another =
unfalsifiable suggestion that somehow storing data with a physical hw regis=
ter (such as where REPORT_DATA is sent) could affect computational proofs w=
hen it is not used as input to the key schedule.</div><blockquote class=3D"=
gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(20=
4,204,204);padding-left:1ex"><div><p>Best regards,</p><p>Usama, Slava, and =
Jean-Marie<br></p><blockquote type=3D"cite"><div dir=3D"ltr"><div dir=3D"lt=
r"><div dir=3D"ltr"><div dir=3D"ltr">[0]=C2=A0<a href=3D"https://mailarchiv=
e.ietf.org/arch/msg/seat/T78G1TFWqcj3O9vrCvNihcn8QeU/" target=3D"_blank">ht=
tps://mailarchive.ietf.org/arch/msg/seat/T78G1TFWqcj3O9vrCvNihcn8QeU/</a><b=
r><br>[1]=C2=A0<a href=3D"https://mailarchive.ietf.org/arch/msg/seat/S3l-tc=
-pnfHs9rcAfeuMGyVzW1Q/" target=3D"_blank">https://mailarchive.ietf.org/arch=
/msg/seat/S3l-tc-pnfHs9rcAfeuMGyVzW1Q/</a><br><br>[2]=C2=A0<a href=3D"https=
://mailarchive.ietf.org/arch/msg/seat/RhYelVXkqUDKa3CKLvkqQU4Z23M/" target=
=3D"_blank">https://mailarchive.ietf.org/arch/msg/seat/RhYelVXkqUDKa3CKLvkq=
QU4Z23M/</a><br><br>[3]=C2=A0<a href=3D"https://github.com/nathanaelritz/in=
tra-handshake-paper/tree/3719fddd7cf0be930d1c256bac1096f7c53494f0/proposal"=
 target=3D"_blank">https://github.com/nathanaelritz/intra-handshake-paper/t=
ree/3719fddd7cf0be930d1c256bac1096f7c53494f0/proposal</a><br><br>[4]=C2=A0<=
a href=3D"https://github.com/nathanaelritz/intra-handshake-paper/commit/371=
9fddd7cf0be930d1c256bac1096f7c53494f0#diff-8ffc30d09ebb6bc1fd9df2ae48d0a0bc=
0289582ea40c99f6c2ea66ee738f189d" target=3D"_blank">https://github.com/nath=
anaelritz/intra-handshake-paper/commit/3719fddd7cf0be930d1c256bac1096f7c534=
94f0#diff-8ffc30d09ebb6bc1fd9df2ae48d0a0bc0289582ea40c99f6c2ea66ee738f189d<=
/a><br><div><br></div></div></div></div></div></blockquote><p>[5]=C2=A0<a h=
ref=3D"https://mailarchive.ietf.org/arch/msg/seat/dKVqaL8RJSQLonIEmtzrDYEXE=
AU/" target=3D"_blank">https://mailarchive.ietf.org/arch/msg/seat/dKVqaL8RJ=
SQLonIEmtzrDYEXEAU/</a></p><p>[6]=C2=A0<a href=3D"https://www.researchgate.=
net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_=
CVE_in_Attested_TLS" target=3D"_blank">https://www.researchgate.net/publica=
tion/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Atte=
sted_TLS</a></p><p>[7]=C2=A0<a href=3D"https://mailarchive.ietf.org/arch/ms=
g/seat/2_aGylmFHoLmqN7BBcYVoH-rNJk/" target=3D"_blank">https://mailarchive.=
ietf.org/arch/msg/seat/2_aGylmFHoLmqN7BBcYVoH-rNJk/</a><br></p></div>______=
_________________________________________<br>Seat mailing list --=C2=A0<a h=
ref=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.org</a><br>To unsu=
bscribe send an email to=C2=A0<a href=3D"mailto:seat-leave@ietf.org" target=
=3D"_blank">seat-leave@ietf.org</a></blockquote><div><br></div><div>Cheers,=
<br>Nathanael=C2=A0<br><br>[8]=C2=A0<a href=3D"https://github.com/nathanael=
ritz/intra-handshake-paper/blob/nr-proposal-patch/proposal/verification_res=
ults_full.txt" target=3D"_blank">https://github.com/nathanaelritz/intra-han=
dshake-paper/blob/nr-proposal-patch/proposal/verification_results_full.txt<=
/a><br><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr"=
>-------------------<br>From:=C2=A0<strong class=3D"gmail_sendername" dir=
=3D"auto">Muhammad Usama Sardar</strong>=C2=A0<span dir=3D"auto">&lt;<a hre=
f=3D"mailto:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad=
_usama.sardar@tu-dresden.de</a>&gt;</span><br>Date: Tue, 28 Jul 2026 at 10:=
00<br>Subject: [Seat] Re: Comments on formal analysis of relay attacks in i=
ntra-handshake attestation (CVE-2026-33697)<br>To:=C2=A0<a href=3D"mailto:s=
eat@ietf.org" target=3D"_blank">seat@ietf.org</a>=C2=A0&lt;<a href=3D"mailt=
o:seat@ietf.org" target=3D"_blank">seat@ietf.org</a>&gt;<br>Cc:=C2=A0<a hre=
f=3D"mailto:ufmrg@irtf.org" target=3D"_blank">ufmrg@irtf.org</a>=C2=A0&lt;<=
a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">ufmrg@irtf.org</a>&gt;<b=
r></div><br><br><u></u><div><p>Hi Nathanael,<br></p><p>This does not addres=
s any of the questions in [5] where your working was shown to be not correc=
t, and these inaccuracies still remain here too. For clarity, nothing has c=
hanged in the key schedule of TLS 1.3 for quite long time (I think draft-20=
 which became RFC8446). Saying that RFC9846 is &quot;new work&quot; for key=
 schedule is almost surely wrong. Maybe Ekr can confirm.<br></p><div>On 28.=
07.26 16:48, Nathanael Ritz wrote:<br></div><blockquote type=3D"cite"><div =
dir=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr">In Usama&#39=
;s July 6 email [0], I was invited to present a formal counter-example to S=
ection 9 of the paper. The `binder6` model (`tls-lib-simple.pvl`) provides =
that exact counter-example by addressing the core architectural requirement=
s:<br></div></div></div></div></blockquote><p>Following the requests of man=
y other WG/RG participants (e.g., [7]), the email [0] clearly asks for a=C2=
=A0<b>property</b>=C2=A0that:</p><ol><li>the hybrid construction (intra- + =
post-handshake attestation)=C2=A0<i>can</i>=C2=A0satisfy, but<br></li><li>p=
ost-handshake attestation alone=C2=A0<i>cannot</i>=C2=A0satisfy</li></ol><p=
>What you are changing is the model and not presenting a property. So eithe=
r the link [0] is wrong or else this needs a clarification. So is your clai=
m that the three binding properties=C2=A0<i>cannot</i>=C2=A0be achieved by =
post-handshake attestation alone? I think that claim is very easily falsifi=
able. So I am not sure what new information you are bringing on the table.<=
br></p><p>Which specific statement in Sec. 9 of the paper [6] do you claim =
to have found a counter-example?<br></p><blockquote type=3D"cite"><div dir=
=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr">2. Infrastructu=
re identity is preserved in `rdata`: Binding `pubLTK` and `ID_S` directly i=
nside the hardware-signed quote payload (`rdata`) anchors infrastructure id=
entity through the Attestation Key (`privAK`) itself. This secures identity=
 without altering `CertificateVerify` or modifying the TLS 1.3 state machin=
e.<br></div></div></div></div></blockquote>The problem here is that this do=
es not provide proof-of-possession of privLTK, while CertificateVerify does=
 exactly that.<br><blockquote type=3D"cite"><div dir=3D"ltr"><div dir=3D"lt=
r"><div dir=3D"ltr"><div dir=3D"ltr">3. Key schedule compliance: Using the =
standard handshake traffic write keys `(ksh, kch)` inside `rdata` binds the=
 evidence to the handshake state at `ServerHello` while leaving the HKDF de=
rivation tree 100% compliant with RFC 9846 =C2=A77.1.</div></div></div></di=
v></blockquote><p>I am not sure reusing the keys intended for a specific pu=
rpose is helpful. This will not be visible in ProVerif but I think this wil=
l probably break the computational proofs of TLS 1.3. I think we would need=
 to check with TLS WG if they are fine with it.</p><p>Best regards,</p><p>U=
sama, Slava, and Jean-Marie<br></p><blockquote type=3D"cite"><div dir=3D"lt=
r"><div dir=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr">[0]=C2=A0<a href=3D"h=
ttps://mailarchive.ietf.org/arch/msg/seat/T78G1TFWqcj3O9vrCvNihcn8QeU/" tar=
get=3D"_blank">https://mailarchive.ietf.org/arch/msg/seat/T78G1TFWqcj3O9vrC=
vNihcn8QeU/</a><br><br>[1]=C2=A0<a href=3D"https://mailarchive.ietf.org/arc=
h/msg/seat/S3l-tc-pnfHs9rcAfeuMGyVzW1Q/" target=3D"_blank">https://mailarch=
ive.ietf.org/arch/msg/seat/S3l-tc-pnfHs9rcAfeuMGyVzW1Q/</a><br><br>[2]=C2=
=A0<a href=3D"https://mailarchive.ietf.org/arch/msg/seat/RhYelVXkqUDKa3CKLv=
kqQU4Z23M/" target=3D"_blank">https://mailarchive.ietf.org/arch/msg/seat/Rh=
YelVXkqUDKa3CKLvkqQU4Z23M/</a><br><br>[3]=C2=A0<a href=3D"https://github.co=
m/nathanaelritz/intra-handshake-paper/tree/3719fddd7cf0be930d1c256bac1096f7=
c53494f0/proposal" target=3D"_blank">https://github.com/nathanaelritz/intra=
-handshake-paper/tree/3719fddd7cf0be930d1c256bac1096f7c53494f0/proposal</a>=
<br><br>[4]=C2=A0<a href=3D"https://github.com/nathanaelritz/intra-handshak=
e-paper/commit/3719fddd7cf0be930d1c256bac1096f7c53494f0#diff-8ffc30d09ebb6b=
c1fd9df2ae48d0a0bc0289582ea40c99f6c2ea66ee738f189d" target=3D"_blank">https=
://github.com/nathanaelritz/intra-handshake-paper/commit/3719fddd7cf0be930d=
1c256bac1096f7c53494f0#diff-8ffc30d09ebb6bc1fd9df2ae48d0a0bc0289582ea40c99f=
6c2ea66ee738f189d</a><br><div><br></div></div></div></div></div></blockquot=
e><p>[5]=C2=A0<a href=3D"https://mailarchive.ietf.org/arch/msg/seat/dKVqaL8=
RJSQLonIEmtzrDYEXEAU/" target=3D"_blank">https://mailarchive.ietf.org/arch/=
msg/seat/dKVqaL8RJSQLonIEmtzrDYEXEAU/</a></p><p>[6]=C2=A0<a href=3D"https:/=
/www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33=
697_High-severity_CVE_in_Attested_TLS" target=3D"_blank">https://www.resear=
chgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-se=
verity_CVE_in_Attested_TLS</a></p><p>[7]=C2=A0<a href=3D"https://mailarchiv=
e.ietf.org/arch/msg/seat/2_aGylmFHoLmqN7BBcYVoH-rNJk/" target=3D"_blank">ht=
tps://mailarchive.ietf.org/arch/msg/seat/2_aGylmFHoLmqN7BBcYVoH-rNJk/</a><b=
r></p></div>_______________________________________________<br>Seat mailing=
 list --=C2=A0<a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.=
org</a><br>To unsubscribe send an email to=C2=A0<a href=3D"mailto:seat-leav=
e@ietf.org" target=3D"_blank">seat-leave@ietf.org</a></div></div></div><br>=
<div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">----------=
----------<br>From:=C2=A0<strong class=3D"gmail_sendername" dir=3D"auto">Na=
thanael Ritz</strong>=C2=A0<span dir=3D"auto">&lt;<a href=3D"mailto:nathanr=
itz@gmail.com" target=3D"_blank">nathanritz@gmail.com</a>&gt;</span><br>Dat=
e: Tue, 28 Jul 2026 at 08:48<br>Subject: Re: [Seat] Re: Comments on formal =
analysis of relay attacks in attested TLS (CVE-2026-3369)<br>To:=C2=A0<a hr=
ef=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.org</a>=C2=A0&lt;<a=
 href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.org</a>&gt;<br>C=
c:=C2=A0<a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">ufmrg@irtf.org<=
/a>=C2=A0&lt;<a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">ufmrg@irtf=
.org</a>&gt;<br></div><br><br><div dir=3D"ltr"><div dir=3D"ltr"><div dir=3D=
"ltr"><div dir=3D"ltr">Hello,<br><br>Top posting. In Usama&#39;s July 6 ema=
il [0], I was invited to present a formal counter-example to Section 9 of t=
he paper. The `binder6` model (`tls-lib-simple.pvl`) provides that exact co=
unter-example by addressing the core architectural requirements:<br><br>1. =
Dual signatures (`CV_Ext`) are unnecessary: The removal of `CV_Ext` was del=
iberate=E2=80=94to prove that non-standard dual transcript signatures are c=
ompletely redundant for achieving G1 through G3 correlation.<br><br>2. Infr=
astructure identity is preserved in `rdata`: Binding `pubLTK` and `ID_S` di=
rectly inside the hardware-signed quote payload (`rdata`) anchors infrastru=
cture identity through the Attestation Key (`privAK`) itself. This secures =
identity without altering `CertificateVerify` or modifying the TLS 1.3 stat=
e machine.<br><br>3. Key schedule compliance: Using the standard handshake =
traffic write keys `(ksh, kch)` inside `rdata` binds the evidence to the ha=
ndshake state at `ServerHello` while leaving the HKDF derivation tree 100% =
compliant with RFC 9846 =C2=A77.1. While Usama&#39;s stated position is wel=
l noted, as shared on the list in Markus&#39;s recent thread [1], this WG w=
ill continue to work with, and continue to leverage new work, from the TLSW=
G -- as it&#39;s been discussed on-list before [2].<br><br>That said, I am =
happy to demonstrate the same result presented under `proposal/`, which bin=
ds to G2 already. That variation is available to review at [3] and yields t=
he expected outcome:<br><br>```ocaml<br>(* All sanity/reachability checks p=
assing *)<br><br>Query event(ClientStateEv(ev,gxy1)) &amp;&amp; event(Serve=
rStateEv(ev,gxy2)) =3D=3D&gt; gxy1 =3D gxy2 is true.<br><br>Query event(Cli=
entStateEvKch(ev,kch1)) &amp;&amp; event(ServerStateEvKch(ev,kch2)) =3D=3D&=
gt; kch1 =3D kch2 is true.<br><br>Query event(ClientStateEvKc(ev,kc1)) &amp=
;&amp; event(ServerStateEvKc(ev,kc2)) =3D=3D&gt; kc1 =3D kc2 is true.<br>``=
`<br><br>The exact same pattern to lock in the fix was required [4]: popula=
ting `rdata` to include `ID_S` and `pubLTK` directly inside the hardware qu=
ote to anchor infrastructure identity, while stripping the redundant `selfs=
ign` payload out of `CRT` (which was a primary source of ProVerif counter-e=
xamples). In this case, I left the non-standard `CV_Ext` construct complete=
ly untouched, as the previously presented model already demonstrated it to =
be superfluous.<br><br>Cheers,<br>Nathanael<br><br><br>[0]=C2=A0<a href=3D"=
https://mailarchive.ietf.org/arch/msg/seat/T78G1TFWqcj3O9vrCvNihcn8QeU/" ta=
rget=3D"_blank">https://mailarchive.ietf.org/arch/msg/seat/T78G1TFWqcj3O9vr=
CvNihcn8QeU/</a><br><br>[1]=C2=A0<a href=3D"https://mailarchive.ietf.org/ar=
ch/msg/seat/S3l-tc-pnfHs9rcAfeuMGyVzW1Q/" target=3D"_blank">https://mailarc=
hive.ietf.org/arch/msg/seat/S3l-tc-pnfHs9rcAfeuMGyVzW1Q/</a><br><br>[2]=C2=
=A0<a href=3D"https://mailarchive.ietf.org/arch/msg/seat/RhYelVXkqUDKa3CKLv=
kqQU4Z23M/" target=3D"_blank">https://mailarchive.ietf.org/arch/msg/seat/Rh=
YelVXkqUDKa3CKLvkqQU4Z23M/</a><br><br>[3]=C2=A0<a href=3D"https://github.co=
m/nathanaelritz/intra-handshake-paper/tree/3719fddd7cf0be930d1c256bac1096f7=
c53494f0/proposal" target=3D"_blank">https://github.com/nathanaelritz/intra=
-handshake-paper/tree/3719fddd7cf0be930d1c256bac1096f7c53494f0/proposal</a>=
<br><br>[4]=C2=A0<a href=3D"https://github.com/nathanaelritz/intra-handshak=
e-paper/commit/3719fddd7cf0be930d1c256bac1096f7c53494f0#diff-8ffc30d09ebb6b=
c1fd9df2ae48d0a0bc0289582ea40c99f6c2ea66ee738f189d" target=3D"_blank">https=
://github.com/nathanaelritz/intra-handshake-paper/commit/3719fddd7cf0be930d=
1c256bac1096f7c53494f0#diff-8ffc30d09ebb6bc1fd9df2ae48d0a0bc0289582ea40c99f=
6c2ea66ee738f189d</a><br><div><br><br><div class=3D"gmail_quote"><div dir=
=3D"ltr" class=3D"gmail_attr">On Mon, 27 Jul 2026 at 12:57, Muhammad Usama =
Sardar &lt;<a href=3D"mailto:muhammad_usama.sardar@tu-dresden.de" target=3D=
"_blank">muhammad_usama.sardar@tu-dresden.de</a>&gt; wrote:<br></div><block=
quote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1=
px solid rgb(204,204,204);padding-left:1ex"><u></u><div><p>Hi Nathanael,<br=
></p><p>We will be happy to review your artifacts if you would be more prec=
ise. As it is now, there seems to be nothing concrete that we could utilize=
 to improve the artifacts. You seem to criticize #2 but then use the same i=
n your code. Something useful may be to revert #1, and show a fix for #2 th=
at you propose. We can then check the proposed change. Hopefully, you can c=
larify your perspective more precisely.<br></p><div>On 27.07.26 13:55, Nath=
anael Ritz wrote:<br></div><blockquote type=3D"cite"><div dir=3D"ltr"><div =
dir=3D"ltr">Top posting, following up on Markus&#39;s latest comments regar=
ding the counter-examples for &quot;Level 3&quot; binding and whether hands=
hake secret correlation holds across the entire session.</div></div></block=
quote>As just clarified to Markus, the distinction between=C2=A0<i>handshak=
e secret</i>=C2=A0and=C2=A0<i>handshake traffic secrets</i>=C2=A0is critica=
l in TLS 1.3 key schedule.<br><blockquote type=3D"cite"><div dir=3D"ltr"><d=
iv dir=3D"ltr">I recently evaluated a streamlined model that strips out the=
 non-standard dual-signed `CV_Ext` construct and the redundant ephemeral se=
lf-signatures, reverting to a clean, standard TLS 1.3 `CV(sg)` message sign=
ed solely by the ephemeral key.</div></div></blockquote>Removing the second=
 signature, the client may get no guarantee of the infrastructure owner and=
 diversion attacks may apply [3,4].<br><blockquote type=3D"cite"><div dir=
=3D"ltr"><div dir=3D"ltr">Crucially, it binds the full security context=E2=
=80=94`(handshake_secret, ID_S, pubLTK, pubEK)`=E2=80=94directly into the T=
EE-signed quote (`rdata`) [0].<br></div></div></blockquote>There is a poten=
tial risk though. The Target Environment needs to send handshake_secret to =
the Attesting Environment.<br><blockquote type=3D"cite"><div dir=3D"ltr"><d=
iv dir=3D"ltr">## 2. Other non-conformant Key Schedule issues<br><br>When e=
xamining how the binder functions to correlate these secrets, I found the o=
riginal model introduces two explicit key schedule modifications that are c=
ompletely absent from standard TLS and would produce non-conformant values =
the moment they are wired up in real implementations:<br></div></div></bloc=
kquote><p>We are not aware of ProVerif code wired up in real implementation=
. It is typically an abstraction reasonable for the problem at hand. Could =
you please share some reference where ProVerif was wired up in real impleme=
ntation?<br></p><blockquote type=3D"cite"><div dir=3D"ltr"><div dir=3D"ltr"=
>* **`kdf_exp` derives an exporter from the Handshake Secret:** =C2=A0The c=
onstruction derives an exporter directly from `hs`. RFC 9846 =C2=A77.5 perm=
its only `early_exporter_secret` or `exporter_secret` as the exporter input=
, defining a strict two-stage construction: `Derive-Secret(Secret, label, &=
quot;&quot;)` followed by `HKDF-Expand-Label(., &quot;exporter&quot;, Hash(=
context_value))`. The modeled `kdf_exp` inserts a non-standard third stage,=
 chaining `&quot;h exp master&quot;` into an `&quot;ra binder&quot;` interm=
ediate.<br></div></div></blockquote><p>We don&#39;t really see your point. =
Can you explain why having an additional Derive-Secret stage is problematic=
 or what attack vectors it leads to? What impact does removing it make in P=
roVerif? And if you have discovered a security problem, you may like to rep=
ort to TLS WG because it would likely have implications beyond our work sin=
ce this is how the TLS 1.3 key schedule is built, and several researchers h=
ave done both the symbolic and computational proofs of it.<br></p><p>The pa=
per never claims to be using standard or early exporters of RFC9846. In fac=
t, using the former would pretty much become post-handshake attestation. As=
 even the title of the paper says, the paper is about intra-handshake attes=
tation.</p><blockquote type=3D"cite"><div dir=3D"ltr"><div dir=3D"ltr">* **=
`kdf_es` returns `exp0` in place of `ems0`:** The model replaces the early =
exporter master secret (`ems0`) with `exp0`.</div></div></blockquote>We bel=
ieve early_exporter_secret (&quot;ems0&quot;) is correctly generated. The m=
acro instead returns early exporter value &quot;exp0&quot; which was requir=
ed. We don&#39;t see anything wrong in this modeling. Please clarify what y=
ou view as wrong.<br><blockquote type=3D"cite"><div dir=3D"ltr"><div dir=3D=
"ltr">While the shape resembles =C2=A77.5, it forces the early exporter int=
o a handshake where `psk =3D NoPSK` in both roles=E2=80=94violating =C2=A77=
.5&#39;s requirement that implementations use `exporter_secret` unless expl=
icitly specified by the application.</div></div></blockquote>This seems to =
be misunderstanding. &quot;PSK&quot; is always there in the key schedule, w=
hether the handshake is PSK-based or not. In the former case, it has a valu=
e generated from previous connection. In the latter case, it has a value of=
 &#39;0&#39;.<br><blockquote type=3D"cite"><div dir=3D"ltr"><div dir=3D"ltr=
">Furthermore, it freezes the label and context into the schedule rather th=
an exposing them to the application, while discarding `ems0` entirely so no=
 standard exporter can be derived downstream.<br></div></div></blockquote><=
ol><li>There is no application here. We are modeling in ProVerif.</li><li>e=
arly_exporter_secret &#39;ems0&#39; is not discarded. The early exporter va=
lue &#39;exp0&#39; is indeed derived from &#39;ems0&#39;, returned and used=
.</li><li>early_exporter_secret &#39;ems0&#39; has nothing to do with the s=
tandard exporter.<br></li></ol><blockquote type=3D"cite"><div dir=3D"ltr"><=
div dir=3D"ltr">In any case, the demonstrated model uses `kch` and `ksh` di=
rectly within the rdata field, completely leaving the key schedule entirely=
 untouched while using something derived from the handshake secret, as Mark=
us had proposed.<br></div></div></blockquote>No field in Table 2 of [3] use=
s &#39;kch&#39; or &#39;ksh&#39; in rdata.<br><blockquote type=3D"cite"><di=
v dir=3D"ltr"><div dir=3D"ltr">## 3. Omission of WebPKI and Host Validation=
<br></div></div></blockquote><p>One of the CertificateVerify is for exactly=
 this purpose. So this point does not apply.<br></p><p>Best regards,</p><p>=
Usama, Slava, and Jean-Marie<br></p><blockquote type=3D"cite"><div dir=3D"l=
tr"><div dir=3D"ltr"><br>[0]=C2=A0<a href=3D"https://github.com/nathanaelri=
tz/intra-handshake-paper/commit/b5a79aff30d23c5169578acc92c6d6ff8147ed21#di=
ff-31622704269a7b23066be433f93cb8eda0a33d4b793e2d72bc057a85b135f3e1" target=
=3D"_blank">https://github.com/nathanaelritz/intra-handshake-paper/commit/b=
5a79aff30d23c5169578acc92c6d6ff8147ed21#diff-31622704269a7b23066be433f93cb8=
eda0a33d4b793e2d72bc057a85b135f3e1</a><br><br>[1]=C2=A0<a href=3D"https://g=
ithub.com/nathanaelritz/intra-handshake-paper/blob/b5a79aff30d23c5169578acc=
92c6d6ff8147ed21/binder6/full_verification_results.txt" target=3D"_blank">h=
ttps://github.com/nathanaelritz/intra-handshake-paper/blob/b5a79aff30d23c51=
69578acc92c6d6ff8147ed21/binder6/full_verification_results.txt</a><br><br>[=
2]=C2=A0<a href=3D"https://github.com/nathanaelritz/intra-handshake-paper/t=
ree/b5a79aff30d23c5169578acc92c6d6ff8147ed21/binder6" target=3D"_blank">htt=
ps://github.com/nathanaelritz/intra-handshake-paper/tree/b5a79aff30d23c5169=
578acc92c6d6ff8147ed21/binder6</a><br></div></div></blockquote><p>[3]=C2=A0=
<a href=3D"https://www.researchgate.net/publication/398839141_Identity_Cris=
is_in_Confidential_Computing_Formal_Analysis_of_Attested_TLS" target=3D"_bl=
ank">https://www.researchgate.net/publication/398839141_Identity_Crisis_in_=
Confidential_Computing_Formal_Analysis_of_Attested_TLS</a></p><p>[4]=C2=A0<=
a href=3D"https://github.com/CCC-Attestation/formal-spec-id-crisis" target=
=3D"_blank">https://github.com/CCC-Attestation/formal-spec-id-crisis</a></p=
></div></blockquote>-------------------<br>From: Nathanael Ritz &lt;<a href=
=3D"mailto:nathanritz@gmail.com" target=3D"_blank">nathanritz@gmail.com</a>=
&gt;<br>Date: Mon, 27 Jul 2026 at 05:55<br>Subject: Re: [Seat] Re: Comments=
 on formal analysis of relay attacks in attested TLS (CVE-2026-3369)<br>To:=
 Markus Rudy &lt;mr=3D<a href=3D"mailto:40edgeless.systems@dmarc.ietf.org" =
target=3D"_blank">40edgeless.systems@dmarc.ietf.org</a>&gt;<br>Cc: Muhammad=
 Usama Sardar &lt;<a href=3D"mailto:muhammad_usama.sardar@tu-dresden.de" ta=
rget=3D"_blank">muhammad_usama.sardar@tu-dresden.de</a>&gt;,=C2=A0<a href=
=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.org</a>=C2=A0&lt;<a h=
ref=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.org</a>&gt;,=C2=A0=
<a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">ufmrg@irtf.org</a>=C2=
=A0&lt;<a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">ufmrg@irtf.org</=
a>&gt;<br><br><br>Hello<br><br>Top posting, following up on Markus&#39;s la=
test comments regarding the counter-examples for &quot;Level 3&quot; bindin=
g and whether handshake secret correlation holds across the entire session.=
 Following a previous invitation to take a deeper look into the queries for=
 the newer models, I want to share some concrete analytical results that di=
rectly support Markus&#39;s intuition.<br><br>I recently evaluated a stream=
lined model that strips out the non-standard dual-signed `CV_Ext` construct=
 and the redundant ephemeral self-signatures, reverting to a clean, standar=
d TLS 1.3 `CV(sg)` message signed solely by the ephemeral key. Crucially, i=
t binds the full security context=E2=80=94`(handshake_secret, ID_S, pubLTK,=
 pubEK)`=E2=80=94directly into the TEE-signed quote (`rdata`) [0].<br><br><=
br>## 1. Evaluation of G1 through G3: Markus&#39;s Intuition Holds<br><br>W=
hen we evaluate the binding properties, the symbolic results diverge notice=
ably from the negative expectations previously annotated in the repository,=
 without adding any explicit cryptographic caveats about typical assumption=
s. Based on this model revision, Goals G1 through G3 are show to weakly hol=
d between the traffic keys and the evidence:<br><br><br>```ocaml<br>(* Reac=
hability/sanity checks *)<br>Query not (event(ClientStateEv(ev,gxy_2)) &amp=
;&amp; event(ServerStateEv(ev,gxy_2))) is false.<br><br>Query not (event(Cl=
ientStateEvKch(ev,kch_4)) &amp;&amp; event(ServerStateEvKch(ev,kch_4))) is =
false.<br><br>Query not (event(ClientStateEvKc(ev,kc_4)) &amp;&amp; event(S=
erverStateEvKc(ev,kc_4))) is false.<br><br>(* Binding goals *)<br>Query eve=
nt(ClientStateEv(ev,gxy1)) &amp;&amp; event(ServerStateEv(ev,gxy2)) =3D=3D&=
gt; gxy1 =3D gxy2 is true.<br><br>Query event(ClientStateEvKch(ev,kch1)) &a=
mp;&amp; event(ServerStateEvKch(ev,kch2)) =3D=3D&gt; kch1 =3D kch2 is true.=
<br><br>Query event(ClientStateEvKc(ev,kc1)) &amp;&amp; event(ServerStateEv=
Kc(ev,kc2)) =3D=3D&gt; kc1 =3D kc2 is true.<br>```<br><br><br>Contrary to t=
he assumption that Level 3 binding cannot be achieved without violating pro=
tocol boundaries, ProVerif shows that when the handshake secret and host id=
entity are cryptographically anchored in the TEE quote, endpoints accepting=
 the same evidence are demonstrated to share identical application traffic =
keys. Markus&#39;s argument holds: while the binding material is generated =
earlier during the handshake, authenticating the entire handshake state aft=
er session establishment successfully protects the application traffic secr=
ets.<br><br>Furthermore, evaluating Compound Authentication (`G-CA1`) in th=
is model reveals that injective agreement holds even when ephemeral key lea=
kage (`LeakedEK`) is permitted [1].<br><br><br>## 2. Other non-conformant K=
ey Schedule issues<br><br>When examining how the binder functions to correl=
ate these secrets, I found the original model introduces two explicit key s=
chedule modifications that are completely absent from standard TLS and woul=
d produce non-conformant values the moment they are wired up in real implem=
entations:<br><br>* **`kdf_exp` derives an exporter from the Handshake Secr=
et:** =C2=A0The construction derives an exporter directly from `hs`. RFC 98=
46 =C2=A77.5 permits only `early_exporter_secret` or `exporter_secret` as t=
he exporter input, defining a strict two-stage construction: `Derive-Secret=
(Secret, label, &quot;&quot;)` followed by `HKDF-Expand-Label(., &quot;expo=
rter&quot;, Hash(context_value))`. The modeled `kdf_exp` inserts a non-stan=
dard third stage, chaining `&quot;h exp master&quot;` into an `&quot;ra bin=
der&quot;` intermediate.<br><br>* **`kdf_es` returns `exp0` in place of `em=
s0`:** The model replaces the early exporter master secret (`ems0`) with `e=
xp0`. While the shape resembles =C2=A77.5, it forces the early exporter int=
o a handshake where `psk =3D NoPSK` in both roles=E2=80=94violating =C2=A77=
.5&#39;s requirement that implementations use `exporter_secret` unless expl=
icitly specified by the application. Furthermore, it freezes the label and =
context into the schedule rather than exposing them to the application, whi=
le discarding `ems0` entirely so no standard exporter can be derived downst=
ream.<br><br>Even if these changes were fine actually, I&#39;m not sure why=
 they would otherwise be necessary.<br><br>This is in addition to the non-s=
tandard introduction of a dual-signature CV_ext message.<br><br>In any case=
, the demonstrated model uses `kch` and `ksh` directly within the rdata fie=
ld, completely leaving the key schedule entirely untouched while using some=
thing derived from the handshake secret, as Markus had proposed.<br><br><br=
>## 3. Omission of WebPKI and Host Validation<br><br>It&#39;s worth noting,=
 the demonstrated model completely forgoes webPKI and `pubCA` validation wh=
ile still holding the tested G1, G2 and G3 goals. In the real world, I thin=
k it makes architectural sense to establish a distinct proof of liveness ti=
ed to the TEE without needing to replace webPKI itself, allowing the connec=
tion signing key to continue leveraging standard certificate chains.<br><br=
>The full set of changes can be found here at [2].<br><br>Cheers,<br>Nathan=
ael<br><br><br>[0]=C2=A0<a href=3D"https://github.com/nathanaelritz/intra-h=
andshake-paper/commit/b5a79aff30d23c5169578acc92c6d6ff8147ed21#diff-3162270=
4269a7b23066be433f93cb8eda0a33d4b793e2d72bc057a85b135f3e1" target=3D"_blank=
">https://github.com/nathanaelritz/intra-handshake-paper/commit/b5a79aff30d=
23c5169578acc92c6d6ff8147ed21#diff-31622704269a7b23066be433f93cb8eda0a33d4b=
793e2d72bc057a85b135f3e1</a><br><br>[1]=C2=A0<a href=3D"https://github.com/=
nathanaelritz/intra-handshake-paper/blob/b5a79aff30d23c5169578acc92c6d6ff81=
47ed21/binder6/full_verification_results.txt" target=3D"_blank">https://git=
hub.com/nathanaelritz/intra-handshake-paper/blob/b5a79aff30d23c5169578acc92=
c6d6ff8147ed21/binder6/full_verification_results.txt</a><br><br>[2]=C2=A0<a=
 href=3D"https://github.com/nathanaelritz/intra-handshake-paper/tree/b5a79a=
ff30d23c5169578acc92c6d6ff8147ed21/binder6" target=3D"_blank">https://githu=
b.com/nathanaelritz/intra-handshake-paper/tree/b5a79aff30d23c5169578acc92c6=
d6ff8147ed21/binder6</a><br><br><br><br>-------------------<br>From: Markus=
 Rudy &lt;mr=3D<a href=3D"mailto:40edgeless.systems@dmarc.ietf.org" target=
=3D"_blank">40edgeless.systems@dmarc.ietf.org</a>&gt;<br>Date: Mon, 27 Jul =
2026 at 02:32<br>Subject: [Seat] Re: Comments on formal analysis of relay a=
ttacks in attested TLS (CVE-2026-3369)<br>To: Muhammad Usama Sardar &lt;<a =
href=3D"mailto:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muham=
mad_usama.sardar@tu-dresden.de</a>&gt;,=C2=A0<a href=3D"mailto:seat@ietf.or=
g" target=3D"_blank">seat@ietf.org</a>=C2=A0&lt;<a href=3D"mailto:seat@ietf=
.org" target=3D"_blank">seat@ietf.org</a>&gt;<br>Cc:=C2=A0<a href=3D"mailto=
:ufmrg@irtf.org" target=3D"_blank">ufmrg@irtf.org</a>=C2=A0&lt;<a href=3D"m=
ailto:ufmrg@irtf.org" target=3D"_blank">ufmrg@irtf.org</a>&gt;<br><br><br>H=
i Usama,<br><br>&gt; I think we are largely talking past each other.<br><br=
>I agree - let&#39;s try to understand where and why.<br><br>&gt; 1. Unless=
 I am misunderstanding something, that is not really &quot;missing&quot; in=
 the paper since that is the proposed binder in Sec. 7.2 of [0], and the re=
sults are already in Table 4 of [0]. ProVerif artifacts are in folder &#39;=
proposal&#39; of [3].<br><br>Thanks, I don&#39;t know how I managed to miss=
 that, sorry. The paper states:<br><br>&quot;We prove in<br>ProVerif that i=
t achieves level 2 (G2), as shown in Table 4, whereas G3 evaluates<br>to fa=
lse. Our observation from the TLS key schedule is that at the point in<br>t=
ime when the intra-HS binder is created, kc is not yet derivable. Based on =
this<br>observation and our extensive discussions with the TLS WG, we belie=
ve that it<br>may not be possible to achieve level 3 in intra-HS attestatio=
n while preserving<br>the established security and privacy properties of th=
e TLS protocol.&quot;<br><br>If G3 evaluates to false, you should be able t=
o provide a counter-example that shows how an adversary can come in possess=
ion of the traffic secrets while the session is bound to the handshake secr=
et. I&#39;d be interested how that vector looks like, because it would cont=
radict my proof directly.<br><br>&gt; 2. I believe I covered a good number =
of intuitive arguments in slide 2 of my SEAT presentation [1].<br><br>I thi=
nk what&#39;s missing in that slide are two observations:<br><br>- If the h=
andshake secret is known to the attacker, that attacker can compromise the =
application traffic secrets. So the handshake secret security is not &quot;=
irrelevant for security goals&quot;.<br>- The server may not be authenticat=
ed at the point where evidence is generated, but it is authenticated after =
the TLS handshake completes. That&#39;s my argument: if you look at the ent=
ire state of the TLS session, after it&#39;s created, it&#39;s enough to ob=
serve binding to the handshake secret and authenticating the server as in s=
tandard TLS.<br><br>&gt; 3. I&#39;m not sure what question you are trying t=
o settle for SEAT, where the charter says [...]<br><br>This discussion came=
 up several times on the list, and I don&#39;t think &quot;deriving a binde=
r from a TLS key&quot; is considered an extension of the key schedule by ev=
eryone. Is EKM an extension of the key schedule, too? Deriving another key =
from the exported key material?<br><br>&gt; Thanks for the clarification. I=
 believe Table 4 in [0] has clear counter-examples to your argument. For in=
stance, there are binders which satisfy G1 but not G2 and G3.<br><br>I&#39;=
m sorry to say, but that is a table with emojis, not a clear counter-exampl=
e. You may be aware of the concrete counter examples, but they are not very=
 accessible in their current form. It would be enlightening to see the actu=
al counter-examples, because then we could understand whether we&#39;re mis=
sing considerations from standard TLS security in the formal analysis.<br><=
br>&gt; Just to make sure you are looking at the right figure, I mentioned =
Fig. 3 of [0] which is the protocol and not the TLS key schedule. So I am n=
ot sure why you are mentioning &quot;not part of the TLS key schedule.&quot=
;<br><br>Sorry for the imprecision, but I was hoping the rest of my mail so=
mehow conveyed the message: this is not specific to TLS! Nothing changes in=
 that picture! Assurance of non-LEK is guaranteed out of band!<br><br>I&#39=
;m going to answer the following questions from my product&#39;s POV, but t=
here may be other interpretations that make sense.<br><br>&gt; 1. What exac=
tly is the server identity in your view?<br><br>The hardware identity (Plat=
form instance identity for TDX). This is unique, bound to a specific server=
 and can&#39;t be forced by an attacker on different hardware.<br><br>&gt; =
2. Who assigns this identity?<br><br>Intel.<br><br>&gt; 3. How is that iden=
tity supplying entity trusted?<br><br>I&#39;m going to interpret this as &q=
uot;how is the PIID known to the verifier&quot;, since the ID supplier is t=
rusted anyway in this case. Two ways:<br><br>- I&#39;m running my own datac=
enter, and when I set up a new server I record the PIID into my verifier da=
tabase.<br>- I&#39;m running on hardware provided by my CSP. The CSP can si=
mply publish a list of known PIIDs; or they can cross-sign PCK certificates=
 to endorse the machines they own and operate (this is what POE does).<br><=
br>&gt; 4. Where in the Evidence is the server identity conveyed? (exact fi=
eld in Quote and Report of Intel TDX and AMD SEV-SNP)<br><br>This is part o=
f the AK certificates, i.e. the PCK or the VCEK. Which is why I keep saying=
 that the issue is in remote attestation per se, and can be mitigated in th=
e verifier. It does not need to be considered in the TLS integration.<br><b=
r>&gt; I am not sure what you are talking about, and how this is related to=
 the paper and this discussion. We are not comparing with and without TEE. =
In the world I live in, security is always evaluated compared to the claime=
d security properties. Confidential computing made a claim that there is no=
 need to trust the cloud provider, and we are saying this is not possible i=
n the current technologies.<br><br>I don&#39;t think we need to discuss the=
 discrepancy between marketing and reality here - we agree on that. However=
, if we take &quot;Cloud provider does not need to be trusted to some exten=
t&quot; as a mandatory security property, we will not be able to produce an=
y secure protocol. This is very intuitive to understand: the CSP can mount =
a hardware attack, which is out of scope for TEE security properties, and e=
ither impersonate a TEE or extract secrets (not only EK, but also the traff=
ic secrets). What I&#39;m saying is that trusting the CSP does not defeat t=
he purpose of TEEs (at least not entirely).<br><br>Cheers, Markus<br><br><b=
r><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">----=
---------------<br>From:=C2=A0<strong class=3D"gmail_sendername" dir=3D"aut=
o">Muhammad Usama Sardar</strong>=C2=A0<span dir=3D"auto">&lt;<a href=3D"ma=
ilto:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_usama.=
sardar@tu-dresden.de</a>&gt;</span><br>Date: Sun, 26 Jul 2026 at 17:31<br>S=
ubject: [Seat] Re: Comments on formal analysis of relay attacks in attested=
 TLS (CVE-2026-3369)<br>To: Markus Rudy &lt;mr@edgeless.systems&gt;,=C2=A0<=
a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.org</a>=C2=A0&l=
t;<a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.org</a>&gt;<=
br>Cc:=C2=A0<a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">ufmrg@irtf.=
org</a>=C2=A0&lt;<a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">ufmrg@=
irtf.org</a>&gt;<br></div><br><br><u></u><div><p>Hi Markus,</p><p>I think w=
e are largely talking past each other.<br></p><p>Let me summarize what you =
seem to be saying: you seem to believe that there are binary levels: level0=
 (no binding) and level1 (G1 &lt;=3D&gt; G2=C2=A0&lt;=3D&gt; G3). Is that c=
orrect?<br></p><p>On the contrary, we show in paper that there four fine-gr=
ained levels: level0 (no binding); level1 (G1); level2 (G2) and level3 (G3)=
. Results in Table 4 of [0] provide concrete counter-examples to your level=
s. We&#39;ll happily clarify this in the extended technical report with int=
uition and examples.<br></p><div>On 26.07.26 21:42, Markus Rudy wrote:<span=
 style=3D"white-space:pre-wrap">
</span><span style=3D"white-space:pre-wrap">
</span></div><blockquote type=3D"cite"><blockquote type=3D"cite"><pre>If so=
meone thinks a specific binding mechanism is missing that might lead to dif=
ferent results for intra-handshake attestation, please let us know, and we =
will happily share the analysis with the WG.
</pre></blockquote><pre>The binding mechanism I have in mind is the handsha=
ke secret, or something derived from it. Would be nice to see how this brea=
ks down under formal analysis - I&#39;ve not seen an argument that would ex=
plain that intuitively.</pre></blockquote><p>Thanks, that is helpful. A few=
 notes:<br></p><ol><li>Unless I am misunderstanding something, that is not =
really &quot;missing&quot; in the paper since that is the proposed binder i=
n Sec. 7.2 of [0], and the results are already in Table 4 of [0]. ProVerif =
artifacts are in folder &#39;proposal&#39; of [3].</li><li>I believe I cove=
red a good number of intuitive arguments in slide 2 of my SEAT presentation=
 [1]. For example, I removed the whole encryption done by handshake traffic=
 key, and nothing changes in the security properties of TLS. Doing the same=
 with encryption done by application traffic key literally beats the whole =
purpose of TLS; like why do TLS at all if all you want to do is to send app=
lication data unencrypted. I don&#39;t know how else to explain it more int=
uitively. Maybe someone else can phrase it better than me.<br></li><li>I=
9;m not sure what question you are trying to settle for SEAT, where the cha=
rter says (<i>emphasis</i>=C2=A0my own):</li></ol><blockquote><blockquote><=
p>The attested (D)TLS protocol extension will not modify the (D)TLS<br>prot=
ocol itself. It may define (D)TLS extensions to support its goals<br>but wi=
ll not modify, add, or remove any existing protocol messages<br>or=C2=A0<i>=
modify the key schedule</i>.<br></p></blockquote></blockquote><p>=C2=A0=C2=
=A0=C2=A0 Deriving keys from handshake secret is an extension of the key sc=
hedule which would already violate the SEAT charter.</p><blockquote type=3D=
"cite"><blockquote type=3D"cite"><pre>Please see Sec. 6.4 in paper [0] whic=
h explicitly proves it cryptographically, and let us know what specifically=
 you disagree with. Just vaguely disagreeing is not very helpful.
</pre></blockquote><pre>I thought I was specific: you proved G3 =3D&gt; G2 =
=3D&gt; G1, but you don&#39;t prove it strictly, such that G1 =3D!&gt; G3. =
I&#39;m arguing that G1 &lt;=3D&gt; G2 &lt;=3D&gt; G3, which does not contr=
adict your prove, but makes it more precise.</pre></blockquote><p>Thanks fo=
r the clarification. I believe Table 4 in [0] has clear counter-examples to=
 your argument. For instance, there are binders which satisfy G1 but not G2=
 and G3.</p><p>In the extended technical report, we will add more detailed =
traces and intuitive explanations for each binder, and disprove G1 =3D&gt; =
G2 =3D&gt; G3.<br></p><blockquote type=3D"cite"><blockquote type=3D"cite"><=
pre>Please see first paragraph of G_3 in Sec. 6.3 in paper [0], which expla=
ins explicitly why it is an essential goal.
</pre></blockquote><pre>What I see in the paper is the following paragraph:

&quot;After establishing an attested TLS connection, the client=E2=80=99s s=
ecrets (such as weights and context
data for inference) are encrypted using a key derived from the client=E2=80=
=99s application
traffic key atsc. Hence, an essential security goal is to analyze the corre=
lation
of Evidence with atsc. The derivation of atsc includes handshake messages u=
p
to the server=E2=80=99s F IN. Hence, G3 is at least as strong as G2.&quot;

That paragraph is entirely correct! However, it _does not rule out_ that yo=
u can _correlate_ to atsc by _binding_ to htsc. This is the same argument a=
s above: (G1 &lt;=3D&gt; G3) would imply you can bind to any and correlate =
to atsc. Note that you are using &quot;at least as strong&quot; exactly as =
I mean it: it is as strong, but might not be strictly stronger.</pre></bloc=
kquote>As a concrete counter-example, there exists a binder (namely the one=
 proposed in=C2=A0Sec. 7.2 of [0]) which satisfies G1 and G2 but not G3. I =
believe I covered a good number of arguments in slide 2 of my SEAT presenta=
tion [1].<blockquote type=3D"cite"><blockquote type=3D"cite"><pre>Please se=
e #4 in Sec. 7.1 of [0] for several practical reasons. Do we want that LEK =
in an unrelated server anywhere in the world breaks our connection? That is=
 clearly too bad, and the world is probably better with standard TLS than h=
ave such a broken design of attested TLS.
</pre></blockquote><pre>I&#39;m aware that the relay attack for the binding=
 mechanisms you analyzed applies to any unrelated server being compromised.=
 The mistake is the assumption that servers are cattle, and that you can=
9;t tell between a server compromised in someones basement and a server at =
your contractual $CSP. That, however, is not true: I can configure my evide=
nce verification to only consider trusted (known) server hardware in the fi=
rst place. This is independent of attested TLS, but a function of the verif=
ier.</pre></blockquote><p>I disagree. Developers who are used to TLS must b=
e explicitly given this guidance. Please see the chartering time discussion=
 where IESG explicitly requested operational considerations.<br></p><p>Even=
 if you consider configuration outside the scope of attested TLS, having co=
nfiguration is insufficient. Somehow the identity of server hardware must b=
e sent during the protocol to match against the configured trusted (known) =
server hardware.</p><blockquote type=3D"cite"><blockquote type=3D"cite"><pr=
e>We would be happy if you can share precisely what changes in Fig. 3 of [0=
] in the mitigations you have applied.
</pre></blockquote><pre>As I tried to explain several times, including in t=
he post you responded to: this defect is _not part of the TLS key schedule_=
 - it&#39;s a shortcoming of remote attestation with current generation of =
TEEs! It arises due to the hardware vendors&#39; threat model which does no=
t cover everything that CC once advertised for. The mitigation removes the =
LEK attack vector, which the relay attack relies on. </pre></blockquote><p>=
Just to make sure you are looking at the right figure, I mentioned Fig. 3 o=
f [0] which is the protocol and not the TLS key schedule. So I am not sure =
why you are mentioning &quot;not part of the TLS key schedule.&quot;</p><p>=
Also, as I mentioned, the statements/presentations/answers of Intel and wha=
t is written in their specifications are all very contradictory.<br></p><p>=
Continuing the idea of the last response above, I would like to see precise=
 answers without handwaving to:<br></p><ol><li>What exactly is the server i=
dentity in your view?</li><li>Who assigns this identity?</li><li>How is tha=
t identity supplying entity trusted?</li><li>Where in the Evidence is the s=
erver identity conveyed? (exact field in Quote and Report of Intel TDX and =
AMD SEV-SNP)</li></ol><blockquote type=3D"cite"><blockquote type=3D"cite"><=
pre>Second, this requires trusting the cloud provider, contrary to the whol=
e claim of confidential computing.
</pre></blockquote><pre>We agree on that in principle, but not everything i=
s so black and white. Running in a TEE still reduces the attack surface by =
a lot. Physical attacks in a hyperscaler datacenter are much harder to perf=
orm than software attacks (bringing a suitcase onto the floor and hooking u=
p a machine vs. SSHing into it remotely). TEEs still protect from co-tenant=
s that managed to breach their containment and gain software root on the hy=
pervisor.</pre></blockquote>I am not sure what you are talking about, and h=
ow this is related to the paper and this discussion.=C2=A0<span style=3D"wh=
ite-space:pre-wrap">We are not comparing with and without TEE. </span>In th=
e world I live in, security is always evaluated compared to the claimed sec=
urity properties. Confidential computing made a claim that there is no need=
 to trust the cloud provider, and we are saying this is not possible in the=
 current technologies.<span style=3D"white-space:pre-wrap">
</span><blockquote type=3D"cite"><blockquote type=3D"cite"><pre>Third, what=
 we report is the binding weakness. We do not believe it can be reasonably =
eliminated by anything other than changes in the protocol.
</pre></blockquote><pre>My entire message was about that. I do think there =
is an option for binding securely - the handshake secret - and I made both =
intuitive and mathematical arguments for why that holds. These should be co=
untered with examples, rather than beliefs.</pre></blockquote>Please see my=
 three points in the beginning and please answer them individually as preci=
sely as possible.<span style=3D"white-space:pre-wrap">
</span><blockquote type=3D"cite"><pre>If these CVEs are related to the disc=
ussion at hand I&#39;d like to remind you: Edgeless uses a scheme you publi=
cly call broken (correct), and I explained the mitigation we&#39;re using a=
nd why I think this invalidates the claim, looking at the whole picture. If=
 you think this mitigation is not enough, you are cordially invited to resp=
onsibly disclose the reason to me, too.</pre></blockquote><p>Will follow-up=
 off-list</p><p><span style=3D"white-space:pre-wrap">Best regards,</span></=
p><p><span style=3D"white-space:pre-wrap">Usama, Slava, and Jean-Marie
</span></p><blockquote type=3D"cite"><pre>[0] <a href=3D"https://www.resear=
chgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-se=
verity_CVE_in_Attested_TLS" target=3D"_blank">https://www.researchgate.net/=
publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_=
in_Attested_TLS</a>
[1]: <a href=3D"https://datatracker.ietf.org/meeting/126/materials/slides-1=
26-seat-binding-properties-of-expat-00" target=3D"_blank">https://datatrack=
er.ietf.org/meeting/126/materials/slides-126-seat-binding-properties-of-exp=
at-00</a>

[2] <a href=3D"https://www.researchgate.net/publication/398839141_Identity_=
Crisis_in_Confidential_Computing_Formal_Analysis_of_Attested_TLS" target=3D=
"_blank">https://www.researchgate.net/publication/398839141_Identity_Crisis=
_in_Confidential_Computing_Formal_Analysis_of_Attested_TLS</a>
[3] <a href=3D"https://github.com/muhammad-usama-sardar/intra-handshake.fai=
l" target=3D"_blank">https://github.com/muhammad-usama-sardar/intra-handsha=
ke.fail</a></pre></blockquote></div>_______________________________________=
________<br>Seat mailing list --=C2=A0<a href=3D"mailto:seat@ietf.org" targ=
et=3D"_blank">seat@ietf.org</a><br>To unsubscribe send an email to=C2=A0<a =
href=3D"mailto:seat-leave@ietf.org" target=3D"_blank">seat-leave@ietf.org</=
a></div><div>=C2=A0</div></div></div></div></div></div></div></div></div><d=
iv class=3D"gmail_quote gmail_quote_container"><blockquote class=3D"gmail_q=
uote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,2=
04);padding-left:1ex"><div dir=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr">
</div>
</div>
</div>
</blockquote></div></div>

--000000000000701e830657b05409--