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>
In-Reply-To: 
 <MRWPR02MB12086E888B91ECDB72D4B230AB7CC2@MRWPR02MB12086.eurprd02.prod.outlook.com>
From: Nathanael Ritz <nathanritz@gmail.com>
Date: Mon, 27 Jul 2026 05:55:59 -0600
Message-ID: 
 <CAHxYnaPYKJ_jdbVXraoXQootU4KeaSsmE8Dh0r=RLkZUqcaFqg@mail.gmail.com>
To: Markus Rudy <mr=40edgeless.systems@dmarc.ietf.org>
Content-Type: multipart/alternative; boundary="000000000000930f1a06579668dd"
Message-ID-Hash: QPUQY57VLDEVYGBBDAC5PGD7KCLK33CH
CC: Muhammad Usama Sardar <muhammad_usama.sardar@tu-dresden.de>,
 "seat@ietf.org" <seat@ietf.org>, "ufmrg@irtf.org" <ufmrg@irtf.org>
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-3369=29?=
Archived-At: 
 <https://mailarchive.ietf.org/arch/msg/ufmrg/CDK6POvwh8alcGGmr7QJaEYDfGw>

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

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

On Mon, 27 Jul 2026 at 02:32, Markus Rudy <mr=3D
40edgeless.systems@dmarc.ietf.org> wrote:

> 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 th=
e
> 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 tha=
t
> 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 secre=
t
> 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 securit=
y
> 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 tha=
t
> 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 t=
he
> 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 TL=
S
> integration.
>
> > I am not sure what you are talking about, and how this is related to th=
e
> 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 t=
o
> understand: the CSP can mount a hardware attack, which is out of scope fo=
r
> 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
> Sent: Monday, July 27, 2026 1:30 AM
> To: Markus Rudy; seat@ietf.org
> Cc: ufmrg@irtf.org
> Subject: Re: [Seat] Comments on formal analysis of relay attacks in
> attested TLS (CVE-2026-3369)
>
>
> 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).
> Is 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 somethin=
g
> 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:
> 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].
> 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 b=
y
> 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 y=
ou
> want to do is to send application data unencrypted. I don't know how else
> to explain it more intuitively. Maybe someone else can phrase it better
> than me.
> 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 pr=
ove
> 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 explain=
s
> 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 secr=
ets (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
> up
> 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 argume=
nt
> 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 wan=
t
> that LEK in an unrelated server anywhere in the world breaks our
> connection? That is clearly too bad, and the world is probably better wit=
h
> 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 verificatio=
n
> 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 shortcomin=
g
> of remote attestation with current generation of TEEs! It arises due to t=
he
> hardware vendors' threat model which does not cover everything that CC on=
ce
> 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 su=
re
> 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:
> What exactly is the server identity in your view?
> Who assigns this identity?
> How is that identity supplying entity trusted?
> 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 b=
e
> 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 m=
e,
> too.
> Will follow-up off-list
> Best regards,
> Usama, Slava, and Jean-Marie
> [0]
> https://www.researchgate.net/publication/408219182_Intra-handshakefail_CV=
E-2026-33697_High-severity_CVE_in_Attested_TLS
> [1]:
> https://datatracker.ietf.org/meeting/126/materials/slides-126-seat-bindin=
g-properties-of-expat-00
>
> [2]
> https://www.researchgate.net/publication/398839141_Identity_Crisis_in_Con=
fidential_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
>

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

<div dir=3D"ltr"><div dir=3D"ltr">Hello<br><br>Top posting, following up on=
 Markus&#39;s latest comments regarding the counter-examples for &quot;Leve=
l 3&quot; 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&#39;s intuition.<br><br>I recently ev=
aluated a streamlined model that strips out the non-standard dual-signed `C=
V_Ext` construct and the redundant ephemeral self-signatures, reverting to =
a clean, standard TLS 1.3 `CV(sg)` message signed solely by the ephemeral k=
ey. Crucially, it binds the full security context=E2=80=94`(handshake_secre=
t, 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 Intuitio=
n Holds<br><br>When we evaluate the binding properties, the symbolic result=
s diverge noticeably from the negative expectations previously annotated in=
 the repository, without adding any explicit cryptographic caveats about ty=
pical assumptions. Based on this model revision, Goals G1 through G3 are sh=
ow to weakly hold between the traffic keys and the evidence:<br><br><br>```=
ocaml<br>(* Reachability/sanity checks *)<br>Query not (event(ClientStateEv=
(ev,gxy_2)) &amp;&amp; event(ServerStateEv(ev,gxy_2))) is false.<br><br>Que=
ry not (event(ClientStateEvKch(ev,kch_4)) &amp;&amp; event(ServerStateEvKch=
(ev,kch_4))) is false.<br><br>Query not (event(ClientStateEvKc(ev,kc_4)) &a=
mp;&amp; event(ServerStateEvKc(ev,kc_4))) is false. <br><br>(* Binding goal=
s *)<br>Query event(ClientStateEv(ev,gxy1)) &amp;&amp; event(ServerStateEv(=
ev,gxy2)) =3D=3D&gt; gxy1 =3D gxy2 is true.<br><br>Query event(ClientStateE=
vKch(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; ev=
ent(ServerStateEvKc(ev,kc2)) =3D=3D&gt; kc1 =3D kc2 is true.<br>```<br><br>=
<br>Contrary to the assumption that Level 3 binding cannot be achieved with=
out violating protocol boundaries, ProVerif shows that when the handshake s=
ecret and host identity are cryptographically anchored in the TEE quote, en=
dpoints accepting the same evidence are demonstrated to share identical app=
lication traffic keys. Markus&#39;s argument holds: while the binding mater=
ial is generated earlier during the handshake, authenticating the entire ha=
ndshake state after session establishment successfully protects the applica=
tion traffic secrets.<br><br>Furthermore, evaluating Compound Authenticatio=
n (`G-CA1`) in this model reveals that injective agreement holds even when =
ephemeral key leakage (`LeakedEK`) is permitted [1].<br><br><br>## 2. Other=
 non-conformant Key Schedule issues<br><br>When examining how the binder fu=
nctions to correlate these secrets, I found the original model introduces t=
wo explicit key schedule modifications that are completely absent from stan=
dard TLS and would produce non-conformant values the moment they are wired =
up in real implementations:<br><br>* **`kdf_exp` derives an exporter from t=
he Handshake Secret:** =C2=A0The construction derives an exporter directly =
from `hs`. RFC 9846 =C2=A77.5 permits only `early_exporter_secret` or `expo=
rter_secret` as the exporter input, defining a strict two-stage constructio=
n: `Derive-Secret(Secret, label, &quot;&quot;)` followed by `HKDF-Expand-La=
bel(., &quot;exporter&quot;, Hash(context_value))`. The modeled `kdf_exp` i=
nserts a non-standard third stage, chaining `&quot;h exp master&quot;` into=
 an `&quot;ra binder&quot;` intermediate.<br><br>* **`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 e=
arly exporter into a handshake where `psk =3D NoPSK` in both roles=E2=80=94=
violating =C2=A77.5&#39;s requirement that implementations use `exporter_se=
cret` unless explicitly specified by the application. Furthermore, it freez=
es 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. <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 ad=
dition to the non-standard introduction of a dual-signature CV_ext message.=
=C2=A0<br><br>In any case, the demonstrated model uses `kch` and `ksh` dire=
ctly within the rdata field, completely leaving the key schedule entirely u=
ntouched while using something 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 while still holding the tested G1, G2 and G3 goals. =
In the real world, I think it makes architectural sense to establish a dist=
inct proof of liveness tied to the TEE without needing to replace webPKI it=
self, allowing the connection signing key to continue leveraging standard c=
ertificate chains.<br><br>The full set of changes can be found here at [2].=
<br><br>Cheers,<br>Nathanael<br><br><br>[0] <a href=3D"https://github.com/n=
athanaelritz/intra-handshake-paper/commit/b5a79aff30d23c5169578acc92c6d6ff8=
147ed21#diff-31622704269a7b23066be433f93cb8eda0a33d4b793e2d72bc057a85b135f3=
e1">https://github.com/nathanaelritz/intra-handshake-paper/commit/b5a79aff3=
0d23c5169578acc92c6d6ff8147ed21#diff-31622704269a7b23066be433f93cb8eda0a33d=
4b793e2d72bc057a85b135f3e1</a><br><br>[1] <a href=3D"https://github.com/nat=
hanaelritz/intra-handshake-paper/blob/b5a79aff30d23c5169578acc92c6d6ff8147e=
d21/binder6/full_verification_results.txt">https://github.com/nathanaelritz=
/intra-handshake-paper/blob/b5a79aff30d23c5169578acc92c6d6ff8147ed21/binder=
6/full_verification_results.txt</a><br><br>[2] <a href=3D"https://github.co=
m/nathanaelritz/intra-handshake-paper/tree/b5a79aff30d23c5169578acc92c6d6ff=
8147ed21/binder6">https://github.com/nathanaelritz/intra-handshake-paper/tr=
ee/b5a79aff30d23c5169578acc92c6d6ff8147ed21/binder6</a><br></div><br><div c=
lass=3D"gmail_quote gmail_quote_container"><div dir=3D"ltr" class=3D"gmail_=
attr">On Mon, 27 Jul 2026 at 02:32, Markus Rudy &lt;mr=3D<a href=3D"mailto:=
40edgeless.systems@dmarc.ietf.org">40edgeless.systems@dmarc.ietf.org</a>&gt=
; wrote:<br></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">Hi Usam=
a,<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;mi=
ssing&quot; 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 i=
n folder &#39;proposal&#39; of [3].<br>
<br>
Thanks, I don&#39;t know how I managed to miss that, sorry. The paper state=
s:<br>
<br>
&quot;We prove in<br>
ProVerif that it achieves level 2 (G2), as shown in Table 4, whereas G3 eva=
luates<br>
to false. Our observation from the TLS key schedule is that at the point in=
<br>
time 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 believe that =
it<br>
may not be possible to achieve level 3 in intra-HS attestation while preser=
ving<br>
the established security and privacy properties of the TLS protocol.&quot;<=
br>
<br>
If G3 evaluates to false, you should be able to provide a counter-example t=
hat shows how an adversary can come in possession of the traffic secrets wh=
ile the session is bound to the handshake secret. I&#39;d be interested how=
 that vector looks like, because it would contradict 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 think what&#39;s missing in that slide are two observations: <br>
<br>
- If the handshake secret is known to the attacker, that attacker can compr=
omise the application traffic secrets. So the handshake secret security is =
not &quot;irrelevant for security goals&quot;.<br>
- The server may not be authenticated at the point where evidence is genera=
ted, but it is authenticated after the TLS handshake completes. That&#39;s =
my argument: if you look at the entire state of the TLS session, after it&#=
39;s created, it&#39;s enough to observe binding to the handshake secret an=
d authenticating the server as in standard TLS.<br>
<br>
&gt; 3. I&#39;m not sure what question you are trying to settle for SEAT, w=
here the charter says [...]<br>
<br>
This discussion came up several times on the list, and I don&#39;t think &q=
uot;deriving a binder from a TLS key&quot; is considered an extension of th=
e key schedule by everyone. Is EKM an extension of the key schedule, too? D=
eriving another key from the exported key material?<br>
<br>
&gt; Thanks for the clarification. I believe Table 4 in [0] has clear count=
er-examples to your argument. For instance, 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-=
example. You may be aware of the concrete counter examples, but they are no=
t very accessible in their current form. It would be enlightening to see th=
e actual counter-examples, because then we could understand whether we&#39;=
re missing 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 not =
sure why you are mentioning &quot;not part of the TLS key schedule.&quot;<b=
r>
<br>
Sorry for the imprecision, but I was hoping the rest of my mail somehow con=
veyed the message: this is not specific to TLS! Nothing changes in that pic=
ture! 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 there may be other interpretations that make sense.<br>
<br>
&gt; 1. What exactly is the server identity in your view?<br>
<br>
The hardware identity (Platform instance identity for TDX). This is unique,=
 bound to a specific server and can&#39;t be forced by an attacker on diffe=
rent hardware.<br>
<br>
&gt; 2. Who assigns this identity?<br>
<br>
Intel.<br>
<br>
&gt; 3. How is that identity supplying entity trusted?<br>
<br>
I&#39;m going to interpret this as &quot;how is the PIID known to the verif=
ier&quot;, since the ID supplier is trusted anyway in this case. Two ways:<=
br>
<br>
- I&#39;m running my own datacenter, and when I set up a new server I recor=
d the PIID into my verifier database.<br>
- I&#39;m running on hardware provided by my CSP. The CSP can simply publis=
h 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 field=
 in Quote and Report of Intel TDX and AMD SEV-SNP)<br>
<br>
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 m=
itigated in the verifier. It does not need to be considered in the TLS inte=
gration.<br>
<br>
&gt; I am not sure what you are talking about, and how this is related to t=
he 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 n=
eed to trust the cloud provider, and we are saying this is not possible in =
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 d=
oes not need to be trusted to some extent&quot; as a mandatory security pro=
perty, we will not be able to produce any secure protocol. This is very int=
uitive 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&#39;m saying is=
 that trusting the CSP does not defeat the purpose of TEEs (at least not en=
tirely). <br>
<br>
Cheers, Markus<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
________________________________________<br>
From: Muhammad Usama Sardar<br>
Sent: Monday, July 27, 2026 1:30 AM<br>
To: Markus Rudy; <a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ie=
tf.org</a><br>
Cc: <a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">ufmrg@irtf.org</a><=
br>
Subject: Re: [Seat] Comments on formal analysis of relay attacks in atteste=
d TLS (CVE-2026-3369)<br>
<br>
<br>
Hi Markus,<br>
I think we are largely talking past each other.<br>
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 correct?<br>
On the contrary, we show in paper that there four fine-grained levels: leve=
l0 (no binding); level1 (G1); level2 (G2) and level3 (G3). Results in Table=
 4 of [0] provide concrete counter-examples to your levels. We&#39;ll happi=
ly clarify this in the extended technical report with intuition and example=
s.<br>
On 26.07.26 21:42, Markus Rudy wrote:<br>
If someone thinks a specific binding mechanism is missing that might lead t=
o different results for intra-handshake attestation, please let us know, an=
d we will happily share the analysis with the WG.<br>
<br>
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 ana=
lysis - I&#39;ve not seen an argument that would explain that intuitively.<=
br>
Thanks, that is helpful. A few notes:<br>
Unless I am misunderstanding something, that is not really &quot;missing&qu=
ot; 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=
 &#39;proposal&#39; of [3].<br>
I believe I covered a good number of intuitive arguments in slide 2 of my S=
EAT presentation [1]. For example, I removed the whole encryption done by h=
andshake 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 d=
o is to send application data unencrypted. I don&#39;t know how else to exp=
lain it more intuitively. Maybe someone else can phrase it better than me.<=
br>
I&#39;m not sure what question you are trying to settle for SEAT, where the=
 charter says (emphasis my own):<br>
The attested (D)TLS protocol extension will not modify the (D)TLS<br>
protocol itself. It may define (D)TLS extensions to support its goals<br>
but will not modify, add, or remove any existing protocol messages<br>
or modify the key schedule.<br>
=C2=A0=C2=A0=C2=A0 Deriving keys from handshake secret is an extension of t=
he key schedule which would already violate the SEAT charter.<br>
Please see Sec. 6.4 in paper [0] which explicitly proves it cryptographical=
ly, and let us know what specifically you disagree with. Just vaguely disag=
reeing is not very helpful.<br>
<br>
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 contradict your prove, but ma=
kes it more precise.<br>
Thanks for the clarification. I believe Table 4 in [0] has clear counter-ex=
amples to your argument. For instance, there are binders which satisfy G1 b=
ut not G2 and G3.<br>
In the extended technical report, we will add more detailed traces and intu=
itive explanations for each binder, and disprove G1 =3D&gt; G2 =3D&gt; G3.<=
br>
Please see first paragraph of G_3 in Sec. 6.3 in paper [0], which explains =
explicitly why it is an essential goal.<br>
<br>
What I see in the paper is the following paragraph:<br>
<br>
&quot;After establishing an attested TLS connection, the client=E2=80=99s s=
ecrets (such as weights and context<br>
data for inference) are encrypted using a key derived from the client=E2=80=
=99s application<br>
traffic key atsc. Hence, an essential security goal is to analyze the corre=
lation<br>
of Evidence with atsc. The derivation of atsc includes handshake messages u=
p<br>
to the server=E2=80=99s F IN. Hence, G3 is at least as strong as G2.&quot;<=
br>
<br>
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.<br>
As a concrete counter-example, there exists a binder (namely the one propos=
ed 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 presentation [1=
].<br>
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 T=
LS than have such a broken design of attested TLS.<br>
<br>
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 assu=
mption that servers are cattle, and that you can&#39;t tell between a serve=
r compromised in someones basement and a server at your contractual $CSP. T=
hat, however, is not true: I can configure my evidence verification to only=
 consider trusted (known) server hardware in the first place. This is indep=
endent of attested TLS, but a function of the verifier.<br>
I disagree. Developers who are used to TLS must be explicitly given this gu=
idance. Please see the chartering time discussion where IESG explicitly req=
uested operational considerations.<br>
Even if you consider configuration outside the scope of attested TLS, havin=
g configuration is insufficient. Somehow the identity of server hardware mu=
st be sent during the protocol to match against the configured trusted (kno=
wn) server hardware.<br>
We would be happy if you can share precisely what changes in Fig. 3 of [0] =
in the mitigations you have applied.<br>
<br>
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&#39;s a shortcomin=
g of remote attestation with current generation of TEEs! It arises due to t=
he hardware vendors&#39; 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.=C2=A0<br>
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;<br>
Also, as I mentioned, the statements/presentations/answers of Intel and wha=
t is written in their specifications are all very contradictory.<br>
Continuing the idea of the last response above, I would like to see precise=
 answers without handwaving to:<br>
What exactly is the server identity in your view?<br>
Who assigns this identity?<br>
How is that identity supplying entity trusted?<br>
Where in the Evidence is the server identity conveyed? (exact field in Quot=
e and Report of Intel TDX and AMD SEV-SNP)<br>
Second, this requires trusting the cloud provider, contrary to the whole cl=
aim of confidential computing.<br>
<br>
We agree on that in principle, but not everything is so black and white. Ru=
nning in a TEE still reduces the attack surface by a lot. Physical attacks =
in a hyperscaler datacenter are much harder to perform than software attack=
s (bringing a suitcase onto the floor and hooking up a machine vs. SSHing i=
nto it remotely). TEEs still protect from co-tenants that managed to breach=
 their containment and gain software root on the hypervisor.<br>
I am not sure what you are talking about, and how this is related to the pa=
per 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 secur=
ity properties. Confidential computing made a claim that there is no need t=
o trust the cloud provider, and we are saying this is not possible in the c=
urrent technologies.<br>
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.<br>
<br>
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 mathematic=
al arguments for why that holds. These should be countered with examples, r=
ather than beliefs.<br>
Please see my three points in the beginning and please answer them individu=
ally as precisely as possible.<br>
If these CVEs are related to the discussion at hand I&#39;d like to remind =
you: Edgeless uses a scheme you publicly call broken (correct), and I expla=
ined the mitigation we&#39;re using and why I think this invalidates the cl=
aim, looking at the whole picture. If you think this mitigation is not enou=
gh, you are cordially invited to responsibly disclose the reason to me, too=
.<br>
Will follow-up off-list<br>
Best regards,<br>
Usama, Slava, and Jean-Marie<br>
[0] <a href=3D"https://www.researchgate.net/publication/408219182_Intra-han=
dshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS" rel=3D"norefer=
rer" target=3D"_blank">https://www.researchgate.net/publication/408219182_I=
ntra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS</a><br>
[1]: <a href=3D"https://datatracker.ietf.org/meeting/126/materials/slides-1=
26-seat-binding-properties-of-expat-00" rel=3D"noreferrer" target=3D"_blank=
">https://datatracker.ietf.org/meeting/126/materials/slides-126-seat-bindin=
g-properties-of-expat-00</a><br>
<br>
[2] <a href=3D"https://www.researchgate.net/publication/398839141_Identity_=
Crisis_in_Confidential_Computing_Formal_Analysis_of_Attested_TLS" rel=3D"no=
referrer" target=3D"_blank">https://www.researchgate.net/publication/398839=
141_Identity_Crisis_in_Confidential_Computing_Formal_Analysis_of_Attested_T=
LS</a><br>
[3] <a href=3D"https://github.com/muhammad-usama-sardar/intra-handshake.fai=
l" rel=3D"noreferrer" target=3D"_blank">https://github.com/muhammad-usama-s=
ardar/intra-handshake.fail</a><br>
_______________________________________________<br>
Seat mailing list -- <a href=3D"mailto:seat@ietf.org" target=3D"_blank">sea=
t@ietf.org</a><br>
To unsubscribe send an email to <a href=3D"mailto:seat-leave@ietf.org" targ=
et=3D"_blank">seat-leave@ietf.org</a><br>
</blockquote></div></div>

--000000000000930f1a06579668dd--