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

[Songbo Bu <[e-mail]>]

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