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

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

Hi Nathanael,

Thank you for your detailed comments. First, we updated the subject, 
which was mistakenly mentioning an irrelevant CVE instead of the one we 
discovered.

The key point is that as already discussed (e.g., [16]), we believe 
draft-fossati-seat-early-attestation itself contradicts SEAT charter, 
and hence any reasonable formal analysis related to this draft will do so.

Moreover, we would like to clarify the following and welcome 
constructive feedback as a minimal PR:

On 26.06.26 09:08, Nathanael Ritz wrote:
> ## A. Every demonstrated model uses a non-standard dual 
> `CertificateVerify` construction (`CV_Ext`), in contradiction to the 
> SEAT WG charter
We believe the model section [13] is sufficiently clear on this but we 
will clarify it further in the repo. We considered it more useful to 
show the added value of this contribution to the WG by using the fixed 
version of diversion attacks as the baseline, rather than showing the 
same old attacks from ID-Crisis paper, and the discovered CVE 
(CVE-2026-33697) -- which the previous analysis could not find -- 
practically demonstrates that. This modeling choice makes it clear that 
even with the diversion attacks fixed, high-severity relay attacks would 
still remain in intra-handshake attestation.

The pre-print (which will be added soon [15]) makes this clear as well.

This is also reflected in acknowledgments, where folks who contributed 
to the previous formal modeling effort are acknowledged with an explicit 
split [14]. (Thank you all once again)

> Therefore, I propose that if Usama and collaborators are serious about 
> exploring a dual-signature variation of CertificateVerify as a genuine 
> solution for composing remote attestation with TLS, they perhaps 
> consider continued collaboration with the authors of 
> `draft-yusef-tls-pqt-dual-certs` [10], or with others in the TLS WG, 
> to bring forward their case for novel modifications to the TLS state 
> machine. Otherwise, just as the authors of 
> `draft-fossati-seat-early-attestation` did when moving from revision 
> -02 to -03, I suggest that Sardar et al. consider bringing forward 
> novel proposals or formal analysis for intra-handshake attestation 
> that conform to the SEAT charter.

Thanks. We will share the analysis with the TLS WG as well and as 
already clarified, draft-fossati-seat-early-attestation is technically a 
hybrid with a combination of intra- and post-handshake attestation and 
our formal analysis contribution to the WG questions the claim on the 
need for intra-handshake attestation in this combination.

> ## B. The CA-backed key (`pubLTK`) is never bound into the attestation 
> evidence (`rdata`)

Sure, things are a bit more subtle. There are several open questions 
here based on confidential computing (CC) threat model on how to do that 
with the cloud provider out of TCB and we welcome your thoughts on those:

 1. What is the "long-term identity" of the CC workload? How is
    "long-term identity" assigned to the CC workload? Which entity
    supplies this "long-term identity"? How is that Identity Supplier
    trusted?
 2. How is CA-certified Long-Term Key (LTK) injected in the Confidential
    Computing workload in the first place?

> In every single model (`binder1` through `binder7`, `aggregate`, and 
> `proposal`), the `rdata` value—which is what the Attestation Key 
> (`privAK`) actually signs to generate the evidence—is restricted to 
> nonces, session-derived values, and the uncertified ephemeral key 
> (`pubEK`).

That's how we understand the four analyzed real-world practical 
implementations are doing it

 1. Meta's AI
 2. Cocos AI
 3. Edgeless Systems
 4. CCC proof-of-concept

and they have acknowledged it.

If your understanding of any of the analyzed implementations is 
different, we would appreciate a minimal possible PR for the respective 
binding mechanism that we will be happy to concretely discuss.

> ## Other remarks
>
> From careful review, and based on what has been published to-date, /I 
> have personally found no merit to the claims/ that the main results 
> "suggest that more recent proposals 
> draft-fossati-seat-early-attestation and draft-ritz-seat-facts add 
> unnecessary complexity of intra-handshake attestation without adding 
> any security benefit". [12]
One aspect missing here is that both mentioned drafts are hybrids 
(combination of intra- and post-handshake attestation). Could you please 
identify a concrete security property which is achieved by the 
combination of intra- and post-handshake attestation but not by simple 
post-handshake attestation?
> I respectfully request that the authors update their ProVerif 
> artifacts to accurately reflect the actual binder derivations (such as 
> the `HKDF-Expand-Label` derivation in Section 5.1.1) and the standard 
> `CertificateVerify` boundaries established by the WG's drafts if they 
> have not already done so, and present that work here.

There are no WG's drafts in SEAT as of today. All are /individual/ I-Ds.

> Finally and to that end, I suggest this working group focus its future 
> energy on carefully considering the merits of active indivual I-Ds 
> such as `draft-fossati-seat-expat` or 
> `draft-fossati-seat-early-attestation`. Both are designed to provide 
> resilience against single-key compromise and neither has any known 
> attacks (beyond typical cryptographic assumptions).

We disagree with your assessment of 
draft-fossati-seat-early-attestation. We believe the design in 
draft-fossati-seat-early-attestation is vulnerable to CVE.

Even if you disagree with it, additional code is additional complexity 
and thus additional attack surface. We would like to see much stronger 
arguments than have been presented to date before we absorb this complexity.

Best regards,

Usama, Slava, and Jean-Marie

> [9] https://github.com/CCC-Attestation/formal-spec-KBS
>
> [10] 
> https://mailarchive.ietf.org/arch/msg/tls/amNYPs3eV3a-l5bFQtUDGx4fU24/
>
> [11] 
> https://github.com/CCC-Attestation/formal-spec-KBS/tree/f96761deeee3b7574959eec9f44fe940b33dcbde
>
> [12] 
> https://github.com/CCC-Attestation/formal-spec-KBS/blob/f96761deeee3b7574959eec9f44fe940b33dcbde/README.md?plain=1#L58

[13] https://github.com/CCC-Attestation/formal-spec-KBS#modeling

[14] https://github.com/CCC-Attestation/formal-spec-KBS#acknowledgments

[15] https://github.com/CCC-Attestation/formal-spec-KBS#pre-print

[16] https://mailarchive.ietf.org/arch/msg/seat/2HfF4JjZbJhw-HJo1GbVTkUmeVU/