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

[Nathanael Ritz <[e-mail]>]

Hi everyone,

I have some additional thoughts to offer in this thread.

My thoughts are offered below with [NR]:

On Tue, 30 Jun 2026 at 19:28, Songbo Bu <[e-mail]> wrote:

> Hi all,
>
> [...] I think it would help the SEAT/UFMRG review to keep four items
> explicit for each proposed design:
>
> - what channel/evidence binding goal is being checked;
> - whether the claim is unconditional in the stated model, or
> conditional on excluding named bad events;
> - what concrete value binds Evidence or an Attestation Result to the
> TLS channel and endpoint identity; and
> - what verifier and application-data release behavior is required when
> that value is absent, stale, malformed, or mismatched.
>

[NR]  I don't have much to add on the considerations above for now; however
I do think they are reasonable. As is the discussion with Markus recently
speaking to similiar topics, including pros and cons for the various
attestation timings [30].

On Wed, 1 Jul 2026 at 02:25, Muhammad Usama Sardar <
[e-mail]> wrote:

> Hi Nathanael,
>
> [NR] I am aware of existential quantification, and you are correct that
> placing the unbound `cr'` and `sr'` variables on the right side of the
> implication arrow evaluates the condition globally rather than scoping it
> to the specific session.
>
> Great. We are finally on the same page.
>
> [NR]  [...] I updated the state events to explicitly bind the session
> nonces on the left side of the query [28]. By introducing
> `ClientStateEvCV2(ev, kc1, cr_c, sr_c)` and `ServerStateEvCV2(ev, kc2,
> cr_s, sr_s)`, we can tie the weak-crypto conditions strictly to the active
> session parameters being evaluated. I am curious if you would disagree with
> this approach.
>
> Thanks for sharing this property. Unfortunately, we don't like this
> property and approach because it checks only for limited traces. We believe
> our property is stronger than this.
>
> As Sec. 6.3 of paper [25] mentions, the goal of the property is to check
> how strongly Evidence is bound to the connection.
>
> Would you like to give it another try by proposing a better property?
>
[NR] While I think it's unfortunate that my demonstrated property may not
meet everyone's apparent tastes; since the property already shows that the
examined localized attack can be mitigated by compliant TLS 1.3
implementations (along with the usual caveats that come from symbolic
analysis -- I think there *are* better binder choices than the Early
Exporter to chose from in practice)... I really don't think any further
effort from me is necessary right now.

> We have practical proof of concept of attacks for a few binders and some
> are in progress. We will document the detailed analysis and exploits in a
> separate paper and then share with the WG/RG.
>
[NR] Sure. I think it will be interesting to see where the boundaries lie
and what assumptions are granted or not granted in each case, of course.

Cheers,
Nathanael

[25]
https://www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS

[30] https://mailarchive.ietf.org/arch/msg/seat/fTvLgg27YGQUaCWDh-gnhSgnHz4/


On Wed, 1 Jul 2026 at 02:25, Muhammad Usama Sardar <
[e-mail]> wrote:

> Hi Nathanael,
> On 01.07.26 02:27, Nathanael Ritz wrote:
>
> On Tue, 30 Jun 2026 at 14:11, Muhammad Usama Sardar <
> [e-mail]> wrote:
>
> Also, please note that in ProVerif, variables that appear only after the
>> arrow (==>) are existentially quantified.
>>
>> Hope that helps.
>>
> [NR] I am aware of existential quantification, and you are correct that
> placing the unbound `cr'` and `sr'` variables on the right side of the
> implication arrow evaluates the condition globally rather than scoping it
> to the specific session.
>
> Great. We are finally on the same page.
>
> [NR]  [...] I updated the state events to explicitly bind the session
> nonces on the left side of the query [28]. By introducing
> `ClientStateEvCV2(ev, kc1, cr_c, sr_c)` and `ServerStateEvCV2(ev, kc2,
> cr_s, sr_s)`, we can tie the weak-crypto conditions strictly to the active
> session parameters being evaluated. I am curious if you would disagree with
> this approach.
>
> Thanks for sharing this property. Unfortunately, we don't like this
> property and approach because it checks only for limited traces. We believe
> our property is stronger than this.
>
> As Sec. 6.3 of paper [25] mentions, the goal of the property is to check
> how strongly Evidence is bound to the connection.
>
> Would you like to give it another try by proposing a better property?
>
> We have practical proof of concept of attacks for a few binders and some
> are in progress. We will document the detailed analysis and exploits in a
> separate paper and then share with the WG/RG.
>
> ===
>
> In the mean time, we would love to hear some feedback from the formal
> methods experts in UFMRG.
>
> Best regards,
>
> Usama, Slava, and Jean-Marie
>
>
> [25]
> https://www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS
>

On Tue, 30 Jun 2026 at 19:28, Songbo Bu <[e-mail]> wrote:

> Hi all,
>
> I want to add a short implementer-side point, because it affects how I
> read the current disagreement.
>
> My reading is that the useful distinction is between (1) a security
> goal stated for the attested TLS construction and (2) extra conditions
> that remove weak hashes, weak DH shares, bad elements, missing or
> malformed binders, or stale or mismatched evidence from the execution
> space. In implementation work, those are not just background facts we
> can assume for every connection. They are adversarial or invalid cases
> that a protocol stack must reject, or handle fail-closed, before any
> relying party treats the attestation result as binding to the channel.
>
> So I think it would help the SEAT/UFMRG review to keep four items
> explicit for each proposed design:
>
> - what channel/evidence binding goal is being checked;
> - whether the claim is unconditional in the stated model, or
> conditional on excluding named bad events;
> - what concrete value binds Evidence or an Attestation Result to the
> TLS channel and endpoint identity; and
> - what verifier and application-data release behavior is required when
> that value is absent, stale, malformed, or mismatched.
>
> This is also why I think the long-term identity / CA-backed key
> question should remain explicit rather than implicit. If a design
> relies on a CA-backed LTK/TIK inside a confidential workload, the
> review still needs to state how that identity is assigned, provisioned
> into the workload, and bound to attestation evidence under the
> confidential-computing threat model. Otherwise an implementer may pass
> a formal condition while still leaving unclear which trust anchor or
> workload identity the relying party is accepting.
>
> I am not trying to settle all of the formal-model questions in this
> email. My narrower point is that, from an implementation perspective,
> "the connection does not use weak parameters / malformed state /
> mismatched evidence" is a property that the protocol and verifier have
> to enforce or check. It should not silently become a global
> precondition outside the review boundary.
>
> Best,
> Songbo
>
> On Tue, 30 Jun 2026 18:27:57 -0600, Nathanael Ritz <[e-mail]>
> wrote:
> > Hi everyone,
> >
> > I have additional feedback to share regarding some of the new comments
> in this thread.
> >
> > My thoughts are offered below with [NR]:
> >
> > On Tue, 30 Jun 2026 at 14:11, Muhammad Usama Sardar <
> [e-mail]> wrote:
> >
> > On 28.06.26 22:32, Nathanael Ritz wrote:
> >
> > ## Regarding correlation goals (G3 => G2 => G1)
> >
> > As presented in Sec. 6.4 in paper [0], this proof is paper-and-pen
> based, and not ProVerif based. Please clarify your concern precisely. Thank
> you!
> >
> > [NR] I am pretty confident this is entirely non-responsive. I encourage
> the authors to carefully consider the context of the discussion before
> asking other participants for what some may consider excessive and
> redundant requests to clarify one's "concern precisely", when the authors'
> own source code already should already make such distinctions clear [27] .
> >
> > [NR] For those not following every citation, I mean "Goal G1" through
> "Goal G3" across 3 levels of binding to TLS session:
> >
> > ~~~
> > L1. gxy (gx,gy)
> > L2. kch (up to ServerHello)
> > L3. kc (up to ServerFinished): may include ID_S in Certificate message
> > L1 <= L2 <= L3
> >
> > ~~~
> >
> > On Tue, 30 Jun 2026 at 14:11, Muhammad Usama Sardar <
> [e-mail]> wrote:
> >
> > We would like to clarify a couple of misunderstandings to avoid talking
> past each other:
> >
> > - What you are proposing adding as conditions actually seems to
> translate to the assumption 'there exists no connection in the world that
> ever uses weak hashes, weak DH or bad element.' So your proposed property
> appears to be saying something like: my connection is secure if every
> connection in the world is secure. If every connection in the world is
> secure, then my connection is secure too; so could you clarify the point of
> your proposed property?
> >
> > - We believe you can agree that achieving a property without additional
> assumptions is stronger than achieving a property with the additional
> assumptions that every connection in the world is secure. It's as simple as
> that.
> >
> > Because of above reasons, we disagree with you.
> >
> > [NR] I believe a technically responsive reply to my earlier comments,
> (or to these) would be to follow-up with a model and trace of a concrete
> counter-example that demonstrates a correlation failure for G2 or G3 with
> mechanism #3 *without* relying on an explicit cryptographic downgrade.
> >
> > In any case, Sec. 6.1 in the paper [25] is clear on the threat model,
> and for TLS, it is typical to consider weak hashes, weak DH, or bad element
> (e.g., as Sec. 6.1 clearly cites Bhargavan et al.'s foundational paper for
> TLS 1.3 [26]).
> >
> > Also, please note that in ProVerif, variables that appear only after the
> arrow (==>) are existentially quantified.
> >
> > Hope that helps.
> >
> > [NR] I am aware of existential quantification, and you are correct that
> placing the unbound `cr'` and `sr'` variables on the right side of the
> implication arrow evaluates the condition globally rather than scoping it
> to the specific session. It makes no material difference in this case, as
> far as I have tested. Have the authors tried, do they have a concrete
> counter-example to share? These are the kinds of questions I wonder about
> during these exchanges.
> >
> > However, the models reveal that if a mechanism achieves "Level 1" (G1)
> binding or higher (as seen in mechanisms #3, 5, 7, and the proposal),
> correlation to "Level 2" (G2) and "Level 3" (G3) naturally follows under
> the standard cryptographic assumptions of TLS 1.3.Please see #1 and #2
> above.
> >
> > ## Minimal demonstration under standard cryptographic assumptions
> >
> > In the current models, the G2 and G3 queries return false. However, when
> queries are conditioned to exclude the model's own weak-cryptography
> events, they return true.
> > Please see #1 and #2 above.
> >
> > We welcome any constructive technical feedback.
> >
> > [NR] I believe I have offered the authors plenty of constructive
> feedback, but since they appear to emphatically ask: I updated the state
> events to explicitly bind the session nonces on the left side of the query
> [28]. By introducing `ClientStateEvCV2(ev, kc1, cr_c, sr_c)` and
> `ServerStateEvCV2(ev, kc2, cr_s, sr_s)`, we can tie the weak-crypto
> conditions strictly to the active session parameters being evaluated. I am
> curious if you would disagree with this approach.
> >
> > [NR] To precisely identify the root cause of the key correlation failure
> for Mechanism #3, I ran a systematic minimal cut analysis using these
> constrained queries. By isolating each downgrade atom independently, the
> results were definitive: When the query is conditioned *solely* on the
> server's key exchange choice:
> >
> > ~~~
> > `kc1 = kc2 || event(ServerChoosesKEX(cr_s,sr_s,DHE_13(WeakDH,badEl)))`
> > ~~~~
> >
> > [NR] ProVerif evaluates the "G1" and "G3" properties as **true**.
> Conversely, isolating client-side KEX downgrades, hash downgrades, or the
> `SentBadElement` event alone all evaluate to **false**. [29]
> >
> > [NR] To explain in plain terms as I understand it: This mathematically
> proves there is no structural state-routing or relay flaw in the protocol
> design. The only way the automated solver can force the session keys to
> diverge is by explicitly forcing the server to negotiate a weak
> Diffie-Hellman group and ingest a malicious group element during the active
> session. This is a localized KEX downgrade attack, entirely mitigated by
> compliant TLS 1.3 implementations.
> >
> > We would love to hear from the formal methods experts in UFMRG. We also
> warmly welcome future collaborators moving forward. Thank you!
> >
> > Best regards,
> >
> > Usama, Slava, and Jean-Marie
> >
> > [NR] Trailing thought: I wonder (mostly rhetorically, to be clear) if
> perhaps the ProVerif queries are meant to have no association with [12] at
> all? In that case, perhaps the authors would like to clarify the exact
> relationship between the paper at [25] and what the proverif model at [27]
> is trying to prove and why they are being shared concurrently.
> >
> > Cheers,
> > Nathanael
> >
> > [12]
> https://github.com/CCC-Attestation/formal-spec-KBS/blob/f96761deeee3b7574959eec9f44fe940b33dcbde/README.md?plain=1#L58
> >
> > [25]
> https://www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS
> >
> > [26] https://ieeexplore.ieee.org/document/7958594/
> >
> > [27]
> https://github.com/CCC-Attestation/formal-spec-KBS/blob/188409b866b8fc0210c8e5d9579e441aa91ce326/binder3/tls-lib-simple.pvl#L582-L638
> >
> > [28]
> https://github.com/nathanaelritz/relay-attacks-in-attested-tls/tree/binder3-sca-demo/binder3/sca
> >
> > [29]
> https://raw.githubusercontent.com/nathanaelritz/relay-attacks-in-attested-tls/refs/heads/binder3-sca-demo/binder3/sca/log-binder3-sca.txt
> >
> > On Tue, 30 Jun 2026 at 14:11, Muhammad Usama Sardar <
> [e-mail]> wrote:
> >
> > Hi Nathanael,
> >
> > Thank you for your feedback.
> >
> > We would like to clarify a couple of misunderstandings to avoid talking
> past each other:
> >
> > - What you are proposing adding as conditions actually seems to
> translate to the assumption 'there exists no connection in the world that
> ever uses weak hashes, weak DH or bad element.' So your proposed property
> appears to be saying something like: my connection is secure if every
> connection in the world is secure. If every connection in the world is
> secure, then my connection is secure too; so could you clarify the point of
> your proposed property?
> >
> > - We believe you can agree that achieving a property without additional
> assumptions is stronger than achieving a property with the additional
> assumptions that every connection in the world is secure. It's as simple as
> that.
> >
> > Because of above reasons, we disagree with you.
> >
> > In any case, Sec. 6.1 in the paper [25] is clear on the threat model,
> and for TLS, it is typical to consider weak hashes, weak DH, or bad element
> (e.g., as Sec. 6.1 clearly cites Bhargavan et al.'s foundational paper for
> TLS 1.3 [26]).
> >
> > Also, please note that in ProVerif, variables that appear only after the
> arrow (==>) are existentially quantified.
> >
> > Hope that helps.
> >
> > On 28.06.26 22:32, Nathanael Ritz wrote:
> >
> > ## Regarding correlation goals (G3 => G2 => G1)
> >
> > As presented in Sec. 6.4 in paper [0], this proof is paper-and-pen
> based, and not ProVerif based. Please clarify your concern precisely. Thank
> you!
> >
> > However, the models reveal that if a mechanism achieves "Level 1" (G1)
> binding or higher (as seen in mechanisms #3, 5, 7, and the proposal),
> correlation to "Level 2" (G2) and "Level 3" (G3) naturally follows under
> the standard cryptographic assumptions of TLS 1.3.Please see #1 and #2
> above.
> >
> > ## Minimal demonstration under standard cryptographic assumptions
> >
> > In the current models, the G2 and G3 queries return false. However, when
> queries are conditioned to exclude the model's own weak-cryptography
> events, they return true.
> > Please see #1 and #2 above.
> >
> > We welcome any constructive technical feedback.
> >
> > We would love to hear from the formal methods experts in UFMRG. We also
> warmly welcome future collaborators moving forward. Thank you!
> >
> > Best regards,
> >
> > Usama, Slava, and Jean-Marie
> >
> > [25]
> https://www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS
> >
> > [26] https://ieeexplore.ieee.org/document/7958594/
> >
> > -----------------------------------------------
> >
> > From: Nathanael Ritz <[e-mail]>
> > Date: Sun, 28 Jun 2026 at 14:32
> > Subject: Re: [Seat] Comments on formal analysis of relay attacks in
> attested TLS (CVE-2026-33697)
> > To: Songbo Bu <[e-mail]>
> > Cc: <[e-mail]>, <[e-mail]>, Muhammad Usama Sardar <
> [e-mail]>
> >
> > Hi Songbo, all,
> >
> > On Sat, 27 Jun 2026 at 21:28, Songbo Bu wrote:
> > >
> > > 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
> > >
> >
> > I appreciate the focused question, although I believe it may distract
> from the topic at hand. However, I am happy to briefly touch on that topic
> here: before we can fully evaluate the two, we face a benchmarking
> challenge. The formal analysis of the post-handshake attestation is
> currently a "work-in-progress," as noted in the Appendix of
> `draft-fossati-seat-expat-02` [23].
> >
> > For example, a unique design for post-handshake attestation presented by
> Usama to the CFRG introduces multiple exported authenticators (`EKM_RD`,
> `EKM_HC`, and `EKM_FK`) [24]. This approach appears to represent a material
> shift from the single-exporter design specified in Section 5.1 of the
> `draft-fossati-seat-expat-02` draft. Perhaps you may agree, then, that
> until the benchmark formal model for `draft-fossati-seat-expat` is
> published, it is difficult to explicitly identify a comparative property
> that we might all find satisfactory.
> >
> > I believe that the discussion evaluating the architectural merits
> between pure intra-, post-, or hybrid compositions is an important one, but
> different from the technical evaluation of the formal model discussed here.
> If you agree, I believe that raising this question to a fresh, narrowly
> scoped thread would allow the WG to keep both important discussions clear
> and distinct from one another. I would be happy to continue discussing the
> topic in more detail with you there, and feel free to reference this thread
> if you do go ahead.
> >
> > ---
> >
> > ## Regarding correlation goals (G3 => G2 => G1)
> >
> > On that note, I would like to bring the WG's focus back to the technical
> discussion regarding the ProVerif models at hand. Specifically, I want to
> address the "Main Results" and their claimed implications [12], which I
> have previously contested.
> >
> > I have repeated before, and will clarify again, that the flaws
> responsibly disclosed in CVE-2026-33697 are not under dispute by me.
> Furthermore, I believe that the analysis helps us understand that based on
> these models, it is not possible to achieve even "Level 1" (G1) binding (to
> use the author's taxonomy) without some kind of session material that can
> help bind the Evidence and Attestation Results to the TLS connection.
> >
> > However, the models reveal that if a mechanism achieves "Level 1" (G1)
> binding or higher (as seen in mechanisms #3, 5, 7, and the proposal),
> correlation to "Level 2" (G2) and "Level 3" (G3) naturally follows under
> the standard cryptographic assumptions of TLS 1.3.
> >
> > ## Minimal demonstration under standard cryptographic assumptions
> >
> > In the current models, the G2 and G3 queries return false. However, when
> queries are conditioned to exclude the model's own weak-cryptography
> events, they return true. For example, the model demonstrating Binder 3
> (Early exporter `exp0`) shows binding to both G2 and G3 binding under
> standard assumptions. E.g.:
> >
> > **Baseline query (returns false):**
> >
> > ~~~ocaml
> > query ev:bitstring, kc1:ae_key, kc2:ae_key;
> > event(ClientStateEvKc(ev,kc1)) &&
> > event(ServerStateEvKc(ev,kc2)) ==> (kc1 = kc2).
> > ~~~
> >
> > **Conditioned query under strong crypto (returns true):**
> >
> > ~~~ocaml
> > query ev:bitstring, kc1:ae_key, kc2:ae_key,
> > cr:random, sr:random, cr':random, sr':random, e:element;
> > event(ClientStateEvKc(ev,kc1)) &&
> > event(ServerStateEvKc(ev,kc2)) ==> (kc1 = kc2) ||
> > event(ServerChoosesKEX(cr,sr,DHE_13(WeakDH,e))) ||
> > event(ServerChoosesHash(cr',sr',WeakHash)) ||
> > event(SentBadElement).
> > ~~~
> >
> > It appears that the result generalizes: any mechanism achieving G1
> demonstrates the ability to achieve G3 under standard assumptions. That is,
> by excluding weak DH groups, weak hash algorithms, or a bad group element
> -- all of which are already prohibited in compliant TLS 1.3 implementations
> per RFC 8446(bis), each demonstrates full G3 binding properties, based on
> the authors' formal models. In contrast, attempting the same against
> Binder2 did not achieve G3, G2 or even G1 binding even with standard
> cryptographic assumptions.
> >
> > Therefore, I believe this is further indication that the broad claims
> repeatedly made against those active drafts lack sufficient technical
> evidence based on the current models to sustain them. Of course, authors
> are implicitly and explicitly welcome to follow up with a substantive
> response rooted in the technical merits of their presented work.
> >
> > ---
> >
> > Songbo, given your focus on evaluating the added complexity versus
> security benefits, would you be willing to initiate the new thread on the
> architectural comparison? I look forward to diving into that discussion
> with you.
> >
> > Respectfully,
> > Nathanael Ritz
> >
> > [23]
> https://datatracker.ietf.org/meeting/125/materials/slides-125-cfrg-relay-attacks-00 -
> slide 15/18
> >
> > [24]
> https://www.ietf.org/archive/id/draft-fossati-seat-expat-02.html#name-post-handshake-vs-intra-hand
> >
> > -----------------------------------------------
> >
> > From: Nathanael Ritz <[e-mail]>
> > Date: Sat, 27 Jun 2026 at 13:18
> > Subject: Re: [Seat] Comments on formal analysis of relay attacks in
> attested TLS (CVE-2026-33697)
> > To: [e-mail] <[e-mail]>
> > Cc: <[e-mail]>, Songbo Bu <[e-mail]>, Muhammad Usama
> Sardar <[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:
> >
> > - 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:
> >
> > ```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]:
> >
> > - 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]>](mailto:
> [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