[Seat] Re: Comments on formal analysis of relay attacks in intra-handshake attestation (CVE-2026-33697)

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

Hi Nathanael,

We will be happy to review your artifacts if you would be more precise. 
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 
in your code. Something useful may be to revert #1, and show a fix for 
#2 that 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-signatures, 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—`(handshake_secret, 
> ID_S, pubLTK, pubEK)`—directly 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 
> modifications that are completely absent from standard TLS and would 
> produce non-conformant values the moment they are wired up in real 
> implementations:

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 §7.5 
> permits 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.

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? 
What 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 likely 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 and 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 
as wrong.
> While the shape resembles §7.5, it forces the early exporter into a 
> handshake where `psk = NoPSK` in both roles—violating §7.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 has 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 so 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/b5a79aff30d23c5169578acc92c6d6ff8147ed21#diff-31622704269a7b23066be433f93cb8eda0a33d4b793e2d72bc057a85b135f3e1
>
> [1] 
> https://github.com/nathanaelritz/intra-handshake-paper/blob/b5a79aff30d23c5169578acc92c6d6ff8147ed21/binder6/full_verification_results.txt
>
> [2] 
> https://github.com/nathanaelritz/intra-handshake-paper/tree/b5a79aff30d23c5169578acc92c6d6ff8147ed21/binder6

[3] 
https://www.researchgate.net/publication/398839141_Identity_Crisis_in_Confidential_Computing_Formal_Analysis_of_Attested_TLS

[4] https://github.com/CCC-Attestation/formal-spec-id-crisis