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

[Nathanael Ritz <[e-mail]>]

Hello,

Thank you to Usama and collaborators for bringing their recent work forward
for the SEAT WG and UFMRG to consider [9]. I have independently reviewed
the models and I have a number of concerns regarding the applicability of
the analysis to the current effort of this working group. My concerns are
organized into two main parts, A. and B., along with a few additional
remarks.

My comments are offered below:


## A. Every demonstrated model uses a non-standard dual `CertificateVerify`
construction (`CV_Ext`), in contradiction to the SEAT WG charter

TLS 1.3 (RFC 8446bis) requires a single signature from the endpoint's
identity key over the handshake transcript. However, the models apply
*both* an uncertified ephemeral key (`privEK`) and a CA-backed long-term
key (`privLTK`) to sign the transcript independently of each other.

This is explicitly written in the `Server` process:

```ocaml
let sg     = sign(privEK ,hash(hash_algo,log_CRT)) in
let sg_LTK = sign(privLTK,hash(hash_algo,log_CRT)) in
out(io,CV_Ext(sg,sg_LTK));
```

The `Client` process is then hardcoded to receive and verify this
dual-signature payload:

```ocaml
in(io,CV_Ext(s,s_LTK));
if verify(pubEK,hash(shash_algo,log_CRT),s) = true then
if verify(pubLTK,hash(shash_algo,log_CRT),s_LTK) = true then
```

In case it is not apparent, this dual-signature `CV_Ext` mechanism has no
basis in any IETF proposed standard.

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.


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

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

Looking at the `Server` process across the binder folders, the exact
definitions for `rdata` across all the evaluated mechanisms are:

```
* **Binder 1:** `let rdata = rand2bs(cr)`
  (Client's TLS nonce)

* **Binder 2:** `let rdata = rand2bs(ar)`
  (Client's attestation nonce)

* **Binder 3:** `let rdata = exp0`
  (Early exporter)

* **Binder 4:** `let rdata = pub2bs(pubEK)`
  (Ephemeral public key)

* **Binder 5:** `let rdata = (ar,exp0)`
  (Attestation nonce + Early exporter)

* **Binder 6:** `let rdata = (ar,pubEK)`
  (Attestation nonce + Ephemeral public key)

* **Binder 7:** `let rdata = (ar,exp0,pubEK)`
  (Attestation nonce + Early exporter + Ephemeral public key)

* **Aggregate:** `let rdata = (cb,pubEK)`
  (Custom HS-derived exporter + Ephemeral public key)

* **Proposal:** `let cb = kdf_exp(hs,log_SH) in let rdata = (ar,cb,pubEK)`
  (Attestation nonce + Custom HS-derived exporter + Ephemeral public key)

```

Not one of these definitions in the published folders includes an rdata
construction where a CA-backed `pubLTK` is included. Therefore, the
attestation Evidence generated in these models completely fails to
cryptographically bind to a trusted 3rd party to validate the identity
associated with the given TLS connection.

I do not believe it is necessary to evaluate the merits of how values like
`cb` are derived when none of the models can even stand up to single key
compromise -- of which -- binding a CA-backed `pubLTK` with the session is
what would be required.

As of the currently published commit (#f96761d) in the shared repo [11],
the vulnerability analysis in the public release relies on an architecture
that is fundamentally misaligned with the recommendations discussed in both
of the most recent revisions for the current front-running individual I-Ds:
`draft-fossati-seat-early-attestation` and `draft-fossati-seat-expat`.

## Other remarks

While formal methods are an invaluable tool for our process, their utility
depends entirely on the accuracy of the models themselves.

>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] Furthermore, I do
not believe repeating such statements serves the SEAT WG's best interests
unless concrete evidence for those claims can be brought forward and
examined independently.

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.

With all of that said, I strongly believe this effort unequivocally
demonstrates and makes clear that no further consideration of the
long-expired `draft-fossati-tls-attestation` I-D is necessary effort in
this WG. I would strongly recommend that any vendors still deploying
systems based on that old specification make immediate plans to transition
away, in order to avoid well-known vulnerabilities such as CVE-2026-3369,
which Usama and collaborators had previously responsibly disclosed.

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

Authors (all): Please feel free to correct me if I've missed a substantive
detail, though nits are also okay!

Cheers,
Nathanael

---

[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

-----------------------------------------------
From: Muhammad Usama Sardar <[e-mail]>
Date: Thu, 25 Jun 2026 at 16:19
Subject: [Seat] Re: Relay Attacks in Intra-handshake Attestation for
Confidential Agentic AI Systems
To: [e-mail] <[e-mail]>, UFMRG IRTF <[e-mail]>

Hi SEAT and UFMRG,

In line with the SEAT charter (*emphasis* our own):

The working group will engage with the research community on the
evaluation and formal analysis of the protocol artifacts *in parallel*
with the specification work.

and the required property in the SEAT charter (*emphasis* our own):

The attested D(TLS) protocol extension will also describe a minimum
subset of properties that the attested state must convey in order
to *bind the Evidence* and Attestation Results *to the TLS connection*.

we (I, Slava, and Jean-Marie) would like to share the concrete technical
results for binding mechanisms of the intra-handshake attestation from our
formal analysis in ProVerif [9]:


   1. All analyzed binding mechanisms and the corresponding implementations
   of intra-handshake attestation are vulnerable to relay attacks.
   2. Early exporter helps achieve level 1 binding.
   3. Our proposed mechanism helps achieve level 2 binding.
   4. It may not be possible to achieve level 3 binding in intra-handshake
   attestation alone.
   5. The research suggests that more recent proposals
   draft-fossati-seat-early-attestation and draft-ritz-seat-facts add
   complexity of intra-handshake attestation relative to
   draft-fossati-seat-expat without offering additional security benefits.

To support independent review, further research and development by the
RG/WG, we have released the ProVerif artifacts [9] under Apache-2.0
License. We hope these artifacts provide useful input for SEAT.

There is also a paper-and-pen proof in the corresponding paper supporting
the above results, which we will share soon with the WG/RG.

We welcome any constructive and technical feedback from the WG/RG and will
be happy to address it.

Best regards,

Usama, Slava, and Jean-Marie

-----------------------------------------------
From: Nathanael Ritz <[e-mail]>
Date: Mon, 22 Jun 2026 at 11:12
Subject: Re: [Seat] Re: Relay Attacks in Intra-handshake Attestation for
Confidential Agentic AI Systems
To: [e-mail] <[e-mail]>

Hi SEAT,

I have some additional comments to offer in this thread.

Comments are offered below with [NR]:

On Thu, 18 Jun 2026 at 15:58, Muhammad Usama Sardar <
[e-mail]> wrote:

> Hi Paul,
> [...] Formal (Symbolic and paper-and-pen) analyses is *the most* serious
> thing we could do. Let us know if you had/have something else in mind.
>

[NR] I generally agree with Usama's sentiment regarding the merits of
additional formal analysis work, which he shared with me at [2]. Of course,
understanding the context helps interpret any formal analysis to evaluate
how and why certain query results relate to the present work.

> Technically, we do not believe we have missed any binding mechanism for
> intra-handshake attestation that might lead to different results.
>
[NR] My current understanding of this statement is that the paper and/or
artifacts may not directly analyze the unique binding of either of the "two
[3,4] out of three current proposals under discussion in the WG." While
formal analysis of real-world implementations may be useful for some
vendors still deploying old, unstable specs (resulting in high-severity
CVEs), I believe that the current work proposed to this WG has moved well
beyond the limitations originally found in the expired
`draft-fossati-tls-attestation` I-D, for example.

> We would be happy if you could tell from the email in the thread which
> binding mechanism or point us to any missing real-world implementation for
> intra-handshake attestation you would like us to check. Formal analysis
> artifacts are easily extensible.
>
 [NR] In my view, the binding mechanism the WG should evaluate, if not done
already, is found in draft-fossati-seat-early-attestation-04 as defined by
section 5.1.1.

> One can check additional binding mechanisms by just changing the value of
> a single variable: rdata. Everything else is automated.
>
[NR] Depending on the model's construction, merely changing the input to
`rdata` may not yield new results, as that modification alone would be
insufficient without also incorporating a CA-backed certificate into the
same model. I don't think anyone in this WG will argue that any concrete
protocol proposals submitted to the list should not produce a usable second
trust anchor. Usama also noted this sentiment in his IETF-125 follow-up to
the CFRG mailing list regarding his presentation about composing remote
attestation with TLS [5]. I agree that providing two independent trust
anchors seems to be the general point of the exercise.

[NR] Furthermore, both `draft-fossati-seat-expat-02` and
`draft-fossati-seat-early-attestation-04`
acknowledge the risks of so-called "split deployments," where the TLS stack
does not reside inside the TEE [6, 7]. This kind of split deployment can
occur when CV is checked against a standard CA-backed webPKI certificate
whose private key resides outside the TEE.

[NR] Therefore, beyond merely updating the single `rdata` value -- the
formal model needs to evaluate the security properties when a CA-backed
signing key (LTK) is composed with Evidence signed over by the attestation
signing key (AK) present inside the attesting environment. In a follow-up
to Usama's request [2] for my own formal analysis work on
`draft-fossati-seat-expat-02`,
I did just that [8], and found that while the ephemeral signing key inside
the TEE provided no independent security fallbacks on it's own (pending
critical feedback on my model), I still found that both the AK and LTK
independently provided resilience against single key compromise.

[NR] My models for `draft-fossati-seat-early-attestation-03` (extended from
Sardar et al.'s Identity Crisis research) also indicated the same to me: both
the AK and LTK (TIK) appear to provide independent, trust-anchor redundancy
in the case the AK might be abused as a signing oracle, or separately in
the case where the AK is assumed fine, but LTK has been stolen or otherwise
compromised itself.

[NR] In short, while it's hard to be sure about the full scope of the
forthcoming work for now, I would like to see Usama and collaborators share
a model that explicitly evaluates the binder mechanism from
`draft-fossati-seat-early-attestation-04`,
where the assumptions align with that draft's security model: modeling a
TEE-resident TIK that is provisioned with a CA-backed certificate alongside
the novel binder mechanism. I would be very interested to see the results
of such a direct analysis, regardless of opinions regarding the status of
the draft's apparent scope within the SEAT charter.

Sincerely,
Nathanael

[0]
> https://github.com/CCC-Attestation/formal-spec-KBS#upcoming-and-recent-talks-and-research-visits
>
> [1] https://datatracker.ietf.org/doc/draft-usama-seat-intra-vs-post/
>
[2] https://mailarchive.ietf.org/arch/msg/seat/VEgdWuRdOq0YwGV6OUTWUp5ShWM/

[3] https://datatracker.ietf.org/doc/draft-fossati-seat-early-attestation/

[4] https://datatracker.ietf.org/doc/draft-ritz-seat-facts/

[5] https://mailarchive.ietf.org/arch/msg/cfrg/sUQnF1KOL5XsvCwY0VRASICk3T4/
[6]
https://www.ietf.org/archive/id/draft-fossati-seat-expat-02.html#section-5.2-2

[7]
https://www.ietf.org/archive/id/draft-fossati-seat-early-attestation-04.html#section-5.2-2

[8] https://mailarchive.ietf.org/arch/msg/seat/zD1NTnUEdRM5SayHxXfuO9robTA/

On Thu, 18 Jun 2026 at 15:58, Muhammad Usama Sardar <
[e-mail]> wrote:

> Hi Paul,
> On 18.06.26 22:45, Paul Wouters wrote:
>
> On Jun 16, 2026, at 17:02, Muhammad Usama Sardar
> <[e-mail]>
> <[e-mail]> wrote:
>
> Respectfully, just to clarify: as the email mentions, the work was
> requested by Paul, the AD at that time.
>
> i have not requested any formal verification papers.
>
> I meant to refer to the protocol design and analysis work, not the paper.
> This is what we (Slava, Jean-Marie, and I) understood you to be requesting.
>
> I am not aware of any one beyond 2-3 participants who can review the code.
> Since this WG does not have the blessing of FATT, we believe writing paper
> and getting it reviewed at conferences helps in independent evaluation of
> the design approach and artifacts, in addition to WG participants' review.
>
> I have asked the WG in the past to seriously look at intra handshake
> options with offering a straw man idea,
>
> Formal (Symbolic and paper-and-pen) analyses is *the most* serious thing
> we could do. Let us know if you had/have something else in mind.
>
> but you seem mostly interested in disproving your own versions of
> intra-handshake in favour of your preferred solution.
>
> I don't think they are *my* versions. We have collected the binding
> mechanisms from existing real-world implementations of intra-handshake
> attestation, including:
>
>    1. Meta's AI
>    2. Cocos AI
>    3. Edgeless Systems
>    4. CCC proof-of-concept
>
> and discussions with the community, i.e., several research and industry
> consortia [0], including the Confidential Computing Consortium.
>
> Technically, we do not believe we have missed any binding mechanism for
> intra-handshake attestation that might lead to different results. We would
> be happy if you could tell from the email in the thread which binding
> mechanism or point us to any missing real-world implementation for
> intra-handshake attestation you would like us to check. Formal analysis
> artifacts are easily extensible. One can check additional binding
> mechanisms by just changing the value of a single variable: rdata.
> Everything else is automated.
>
> I also do not believe post-handshake is *my* preferred solution. It was
> recommended by TLS WG back then, and several developers have shown their
> preference because of security, privacy and unnecessary complexity issues
> with intra-handshake attestation [1].
>
> I still haven't seen, or missed in the many emails, of why binding TEE PKI
> evidence and web server tls WebPKI cannot be done with some DNS/SAN binding
> signed by the TEE, to ensure the integrity of the TLS server by the TEE
> (even if that is not a confidential cloud computing use case) and avoiding
> rebinding attacks by using a different compromised TEE
> via the SAN reference of the TEE.
>
> We did not understand how to formalize that. If you could write a draft
> clarifying the protocol spec, we'll happily do the analysis for you and
> help you move the idea forward.
>
> Best regards,
>
> -Usama
>