[Ufmrg] Re: [Seat] Comments on formal analysis of relay attacks in attested TLS (CVE-2026-3369)

[Markus Rudy <[e-mail]>]

Hi Usama,

These are indeed the questions I'm trying to wrap my head around. Question (1) is probably less interesting for SEAT immediately, but should be very interesting to RATS if I'm not mistaken, which again makes it important for SEAT, but passively.

Thanks, looking forward to your next paper!

Cheers, Markus


________________________________
From: Muhammad Usama Sardar
Sent: Monday, July 27, 2026 5:38 PM
To: Markus Rudy; [e-mail]
Cc: [e-mail]
Subject: Re: [Seat] Comments on formal analysis of relay attacks in attested TLS (CVE-2026-3369)


Hi Markus,

To help keep this discussion more focused, here is my understanding of the points where you would like to see more details:

  1.  Is binder#6 insecure if LEK of some specific servers (identified by PIID in Intel TDX) is somehow ruled out?
  2.  Why our proposed binder in Sec. 7.2 of [0] is insufficient to achieve level 3 security? You would like to see concrete counter-example trace with intuitive explanation for the attack.
     *   OR you would like to see disproof of G1 <=> G2 <=> G3
  3.  Why Intel's POE is insufficient for security?

Is there something I have missed? I believe it is much more organized to have them answered in detailed technical report. So more important than the discussion below is the correction/addition/edits in above questions. We will then work on it and share with the WG/RG.

On 27.07.26 10:32, Markus Rudy wrote:

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.

No worries; I realize that the paper is quite dense. Please take your time to read it.

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 first statement is correct but it addresses a different point. Also, I do not see how the second follows from the first and hence I disagree with the second one.

Please note that I talked about handshake traffic keys and not handshake secret. They are both different. When one dives into the subtleties of key schedule, one realizes how important the distinction is.

There is no direct dependency for application traffic keys on the handshake traffic keys. Please see figure 2 of [4]. Handshake traffic keys may be leaked/compromised independent of application traffic keys.

- 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.

Please note that unlike TLS threat model, in addition to the network, Server is malicious here.

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.

I don't think it is "deriving a binder from a TLS key," rather extending the TLS key schedule to derive a key which is then used in the binder.

My worry is that the TLS WG agreed to do this work under certain conditions. If we go to TLS WG asking this, probably the first question they will ask is why the well-established and formally verified mechanisms like RFC9261/RFC9266 are insufficient. It has lesser complexity and more security. Above that, one needs post-handshake attestation for continuous attestation in any case. The key schedule complexity seems very hard to justify.

Alternatively, we can ignore these conditions. I am not sure that would be productive, because it will ultimately be raised at the IETF LC.

 Is EKM an extension of the key schedule, too?

I don't understand why would it be. It is a part of Sec. 7.5 of the standard RFC9846.

 Deriving another key from the exported key material?

Could you please share a concrete example to understand better? and why such a key is required?

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.

Sec. 7.1 of [0] is intuitively explaining all the seven cases with two of the traces in Fig. 5 and explaining what would change in other cases. I'd like to understand which one you disagree with and the rationale. So could you point me to the specific case or trace that you believe is insufficient or incorrect? That would help me understand where our interpretations differ.

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!

To me, this seems analogous to saying: I was guaranteed out of band that I am talking to an uncompromised endpoint. If I have that guarantee, then it is not clear to me why I would use attestation at all. With that guarantee, I could use standard TLS.

3. How is that identity supplying entity trusted?


[...]
- 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).

I am not aware of any list of known PIIDs published by any CSP. If someone knows, please share a link.

So I assume your parenthesis text refers to cross-sign. Certificates are typically signed just once by the CA. I don't believe I've heard the term "cross-sign" in the context of certificates before. So could you please elaborate this part; as in what exactly does CSP sign? If the CSP does not sign a connection-specific transcript, it is still vulnerable to relay attacks. Moreover, how does the other endpoint (verifying relying party) get the public key of CSP?

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).

Thanks, and good to know that we largely agree on the marketing and reality of confidential computing.

Best,

-Usama


[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-binding-properties-of-expat-00

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

[4] https://www.researchgate.net/publication/385384309_Towards_Validation_of_TLS_13_Formal_Model_and_Vulnerabilities_in_Intel's_RA-TLS_Protocol