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

[Nathanael Ritz <[e-mail]>]

Hi Songbo,

Below with [NR]

On Thu, Jul 2, 2026 at 7:55 AM Songbo Bu <[e-mail]> wrote:

> Hi Nathanael,
>
> Thanks for the clarification. My current understanding is that adding
> extra assumptions usually weakens the protocol-level claim, even if it
> makes a proof go through.


[NR] To be very clear about my stance, I think "typical cryptographic
assumptions" is exactly the opposite of "extra assumptions". I am not
advocating for anything more than securely composing *compliant* TLS 1.3
implementations with remote attestation architecture. My point is that if
we **exclusively** evaluate a protocol design against non-compliant
implementations that intentionally break standard cryptographic guarantees
only, I don’t really think we are analyzing RA composition with
RFC8446(bis) anymore.

[NR] By all means, if a use-case and threat model requires a team to assume
the secure transport protocol they've chosen to compose with cannot be
deemed trustworthy, then they are absolutely encouraged to take the
appropriate defense-in-depth approaches that suits their specific
requirements or deployment policies. And of course -- there is absolutely
nothing wrong with formal analysis that helps expose the total surface area
of assumptions one is required to take when trusting a cryptographic
protocol. There are always trade-offs.

[NR] Sardar et al.’s work made it very clear that some binder compositions
in their evaluation suite cannot even survive standard TLS assumptions
(which is the heart of the CVE finding, as I understand it). That’s an
undeniably valuable contribution to the community. I believe another
valuable service to the community is scientific curiosity that explores
reasonable constructive mitigations. That’s my position.

So the key question for me is: under the standard TLS / attacker
> model, what property does the intra-handshake attestation path provide
> that a simpler post-handshake attestation path with a strict
> application-data release gate does not provide?


[NR] I don’t believe “release gate” is a standard protocol term; what I
believe you are describing structurally translates to an application-layer
proxy or a sidecar deployment pattern. While a post-handshake window can
use an external sidecar to withhold or buffer application data until an
attestation credential (such as Evidence or an Attestation Result) is
appraised, it represents uniquely architectural boundaries than an
intra-handshake path (and I would caution against a blanket assessment of
“simpler” as a blanket assessment). I believe Markus already explained this
in the other thread, but to share some examples in “my own words”:

[NR] *Proactive Prevention vs. Exposure Boundary*: Intra-handshake
attestation ensures that the transport state machine explicitly withholds
the progression to application data exchange until the Relying Party is
satisfied. If validation fails, it triggers a fatal handshake error before
a single byte of application data is ever processed. Post-handshake
attestation, by definition, operates within an already-established session
where application data may technically already be flowing at the network
layer. A "release gate" sidecar can mitigate exposure going forward, but it
cannot retroactively protect application data or prevent the initial
handshake state from completing, although this can also potentially be
addressed with a shim.

[NR] *Fault handling considerations*: When remote attestation is integrated
into the intra-handshake window, a verification failure maps natively to
standard transport protocol handshake-failure handling. In a post-handshake
model, failure handling must occur entirely outside the transport
handshake, where an appraisal policy is used to determine whether to tear
down an active session or perhaps dynamically restrict it to a subset of
functionality.

[NR] Ultimately, I view the two timing models as unique approaches that can
address specific requirements that they naturally lend their strengths
towards. Intra-handshake can be used to establish baseline assurance (under
typical TLS assumptions) before the session becomes usable (structurally
avoiding race conditions), whereas post-handshake handles dynamic state
tracking and periodic re-attestation over long-lived connections. I believe
they are complementary controls, not mutually exclusive alternatives.

[NR] Again, my perspective is that most of this is actually architectural
considerations for SEAT — not cryptographic. I hope that helps clarify my
point of view, but I encourage the WG to review the thread I linked at [30]
for input from other participant's besides myself.

Best,
> Songbo


Cheers,
Nathanael

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

On Wed, 1 Jul 2026 20:22:13 -0600, Nathanael Ritz <[e-mail]>
> wrote:
> > 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
>