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

[Nathanael Ritz <[e-mail]>]

Hi Songbo, Usama, all

I have additional comments to share regarding the recent formal analysis
put foward by Sardar et al., which evaluates relay attacks in attested TLS
such as CVE-2026-33697, as well some of the proposed mitigations.

Comments are offered below with [NR]:

On Sat, 27 Jun 2026 at 09:02, Songbo Bu <[e-mail]> wrote:

> Hi all,
>
> I would like to add an independent reproducibility data point for the
> public artifact.
>
> [...]
>
> The artifact provides a reproducible and formal way to compare different
> authentication-binding strengths in TLS.
>

[NR] I can confirm that the artifacts presented are reproducible and align
with the inline commentary included in the ProVerif source.

[NR] That being said, it's worth noting that the authors of the models have
made efforts to clarify [13] that their analysis cannot provide structural
analysis of the entire design space, as neither of the three active I-Ds
with concrete protocol specifications previously presented to the SEAT WG
includes a dual-signature CV (`CV_Ext`).

[NR] This makes the models put presented by Usama and collaborators
fundamentally incompatible with those drafts, meaning they cannot provide
concrete counter-examples to any of the security claims or properties
mentioned in the individual I-Ds from
either draft-fossati-seat-early-attestation-04 or draft-ritz-seat-facts-00.
This is a meaningful limitation of the formal analysis within the
intra-handshake attestation design space.

This is useful for the SEAT discussion because it distinguishes binding
> evidence to early/DH-derived state, handshake traffic-key state, and
> application traffic-key state under the confidential computing adversary
> model.
>

[NR] The work is useful to the SEAT discussion because it affirms our
understanding that current implementations based on the unadopted, and
expired individual Internet-Draft [17] are insecure and exclude a number of
possible designs that have also been formally proven to be insecure.
Therefore, as I mentioned previously, I **strongly advise** against
introducing concrete designs or specifications in any active Internet-Draft
that reflects any of the binders proposed by Sardar et al. in their most
recent work.

I also think the artifact is valuable input for evaluating whether
> intra-handshake attestation adds security benefit commensurate with its
> protocol complexity. Extra code paths, transcript interactions, and TLS
> state-machine changes increase implementation and review burden. Before
> absorbing that complexity into protocol design, it seems useful to make
> explicit which security property an intra-handshake component achieves, and
> whether that property cannot be achieved by a simpler post-handshake design.
>

[NR] I agree completely. For example, I understand that much of the
concrete specification I proposed in my own individual
I-D, draft-ritz-seat-facts-00 is more complex than necessary compared to
draft-fossati-seat-early-attestation-03 released the same day. This
complexity is even more apparent when compared to the changes published in
their recent -04 revision.

[NR] I am hopeful that such evaluations on concrete proposals based on
**active** Internet-Drafts under discussion with the SEAT WG will continue,
especially if the WG has concensus towards formal adoption
of draft-mihalcea-seat-use-cases.


> If a proposed construction is believed to bind attestation state to TLS in
> a way that differs from the current artifact, a minimal model change or PR
> would make the comparison easier to evaluate.
>

[NR] Agreed. However, I'm not convinced a minimal model change is possible
given the fundamental incompatibility between how the current models under
discussion are constructed and the specifications and security
considerations outlined in the active drafts discussed with the SEAT WG. For
those curious, I outlined the necessary model changes that might be
necessary in order to properly evaluate
draft-fossati-seat-early-attestation-03 at [18], (also copied below in this
thread). I have also proposed a model that demonstrates proper mitigation
of the flaw, as I understand it, at both [19] and [20].

On Fri, 26 Jun 2026 at 05:41, Muhammad Usama Sardar <
[e-mail]> wrote:

> Hi Nathanael,
>
> [...]
>
> 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.
>
[NR] Thanks for clarifying that important detail. The request respectfully
still stands for the *individual* I-Ds I suggested earlier.

> 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.
>
[NR]  Once again, the claim that active individual I-Ds such as
draft-fossati-seat-early-attestation are potentially vulnerable to
CVE-2026-33697 continues to persist without clear demonstrable evidence.
The claim appears to be framed as informed intuition [21], but I don't
think the models’ applicability to inform such intuition has been backed by
their technical merits. As mentioned earlier, I identified two constructive
elements causing the models to strictly fall out of alignment with the
drafts' specifications, and the authors have not disputed this
misalignment.

[NR] I believe that repeated claims of attacks on active drafts under
discussion within any WG ought to be supported by published evidence or
concrete testable arguments, as I largely suggested the same on-list a few
months back [22].

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
>
> [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/
>
>
[17] https://datatracker.ietf.org/doc/draft-fossati-tls-attestation/

[18] https://mailarchive.ietf.org/arch/msg/seat/U-0qtLpaFqQ7MDq-ArRflnEe-rE/


[19] https://mailarchive.ietf.org/arch/msg/seat/-_ljx07LGlxvVtNaKQfKKcUEuhw/

[20] https://mailarchive.ietf.org/arch/msg/seat/bdLxj7cMeRaSgtppKek8uVXHSjA/

[21] https://mailarchive.ietf.org/arch/msg/seat/6P_1jR-fylM9WCOGGTgaVEQ0Khc/

[22] https://mailarchive.ietf.org/arch/msg/seat/J3-2ivC7smo2qNpK6SMP-rKKAjU/

-----------------------------------------------
From: Songbo Bu <[e-mail]>
Date: Sat, 27 Jun 2026 at 09:02
Subject: [Seat] Re: Comments on formal analysis of relay attacks in
attested TLS
To: <[e-mail]>, <[e-mail]>, Muhammad Usama Sardar <
[e-mail]>


Hi all,

I would like to add an independent reproducibility data point for the
public artifact.

I ran the formal-spec-KBS ProVerif artifact at commit:

f96761deeee3b7574959eec9f44fe940b33dcbde

Environment:

ProVerif 2.05
OPAM switch: default
OCaml 5.5.0
Command used in each model directory:
proverif -lib tls-lib-simple.pvl tls13-multiagent.pv

I ran all seven candidate binding mechanisms, binder1 through binder7, and
the proposed mechanism, proposal. All eight runs completed successfully. I
also extracted the Verification summary from each run and compared it
against the log.txt files in the repository; the summaries matched exactly
in all eight cases.

For the three correlation goals, my reproduced results are:

Mechanism | G1: evidence to DH shared secret | G2: evidence to client
handshake traffic key | G3: evidence to client application traffic key
binder1 | false | false | false
binder2 | false | false | false
binder3 | true | false | false
binder4 | false | false | false
binder5 | true | false | false
binder6 | false | false | false
binder7 | true | false | false
proposal | true | true | false

The artifact provides a reproducible and formal way to compare different
authentication-binding strengths in TLS. This is useful for the SEAT
discussion because it distinguishes binding evidence to early/DH-derived
state, handshake traffic-key state, and application traffic-key state under
the confidential computing adversary model.

I also think the artifact is valuable input for evaluating whether
intra-handshake attestation adds security benefit commensurate with its
protocol complexity. Extra code paths, transcript interactions, and TLS
state-machine changes increase implementation and review burden. Before
absorbing that complexity into protocol design, it seems useful to make
explicit which security property an intra-handshake component achieves, and
whether that property cannot be achieved by a simpler post-handshake design.

If a proposed construction is believed to bind attestation state to TLS in
a way that differs from the current artifact, a minimal model change or PR
would make the comparison easier to evaluate.

I am continuing to investigate implementation evidence and can update later
if I obtain additional reproducible results.

Best,
Songbo

_______________________________________________
Seat mailing list -- [e-mail]
To unsubscribe send an email to [e-mail]

-----------------------------------------------
From: Muhammad Usama Sardar <[e-mail]>
Date: Fri, 26 Jun 2026 at 05:41
Subject: Re: [Seat] Comments on formal analysis of relay attacks in
attested TLS (CVE-2026-33697)
To: Nathanael Ritz <[e-mail]>, [e-mail] <[e-mail]>
Cc: <[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/

-----------------------------------------------
From: Nathanael Ritz <[e-mail]>
Date: Fri, 26 Jun 2026 at 01:08
Subject: Comments on formal analysis of relay attacks in attested TLS
(CVE-2026-3369)
To: [e-mail] <[e-mail]>
Cc: <[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
>