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

[Songbo Bu <[e-mail]>]

Hi Nathanael, all,

Thank you for the detailed clarification.

I wanted to ask one focused question about the hybrid intra-/post-handshake
direction. Since the active proposals under discussion combine
intra-handshake and post-handshake attestation components, what concrete
security property is achieved by the hybrid design that cannot be achieved
by a simpler post-handshake attestation design under the confidential
computing adversary model?

I am asking narrowly because this seems central to evaluating whether the
added TLS transcript and state-machine complexity is justified. If the
answer depends on a specific compromise setting, such as AK compromise,
TIK/LTK compromise, split deployment, or verifier-oracle behavior, it would
be helpful to identify the corresponding property or query explicitly.

Best,
Songbo

On Sat, 27 Jun 2026 13:18:55 -0600, Nathanael Ritz [e-mail]
wrote:

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:

   -

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

   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

   -

   Meta’s AI
   -

   Cocos AI
   -

   Edgeless Systems
   -

   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:
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:
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]:

   -

   All analyzed binding mechanisms and the corresponding implementations of
   intra-handshake attestation are vulnerable to relay attacks.
   -

   Early exporter helps achieve level 1 binding.
   -

   Our proposed mechanism helps achieve level 2 binding.
   -

   It may not be possible to achieve level 3 binding in intra-handshake
   attestation alone.
   -

   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:

   -

   Meta’s AI
   -

   Cocos AI
   -

   Edgeless Systems
   -

   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