MIME-Version: 1.0
References: <5f361893-bc32-4737-9578-fdb3ad7be3f9@tu-dresden.de>
 <9F03163D-B0F9-40DD-A4AB-69C151B872D6@aiven.io>
 <c4a0c433-173d-44ac-bd48-eed642a674d3@tu-dresden.de>
 <CAHxYnaOBMnPp7EiRLNYWX8AQDc2zYoBL226nfeBiPXsyii7Now@mail.gmail.com>
 <CAHxYnaOFWQBLf0Pn8bY=CMx7ytSEkTbvj7xp-s0GCHJohRh5xg@mail.gmail.com>
 <2b53d833-51b8-4915-82b0-ac3305e89528@tu-dresden.de>
 <CAHxYnaPDTzHuXyeC06bKWNOQ+wYfc-02AVyDETveL7dTteYURA@mail.gmail.com>
 <CAK08nYaQb6tQzy_nZrJbGbyu1oLuFpAEjTWqe_hY6cmmGzJFvA@mail.gmail.com>
 <CAHxYnaPyD+mFBgk-axNXCS+9qob-nhF_+Y6eqz9fgPnDvNF5Nw@mail.gmail.com>
 <34201e80-edb7-4f99-afa2-0d5b5799c6da@tu-dresden.de>
 <CAHxYnaOUyvMrMRN2C4wjO_s3hpqXDDMJAOAUYyGVt0JRu4RSQQ@mail.gmail.com>
 <3f87fe50-f0bc-45f7-8ed5-0a7cc7cf975c@tu-dresden.de>
 <CAHxYnaOsUBJF1+dkhEuPdhExNmk14cWcauxEw-zo6TotWzxsHQ@mail.gmail.com>
 <CAK08nYZH=Qb5OcdoVhXKn5=hHGS1k-GHisLg--heK=d3W55sxw@mail.gmail.com>
In-Reply-To: 
 <CAK08nYZH=Qb5OcdoVhXKn5=hHGS1k-GHisLg--heK=d3W55sxw@mail.gmail.com>
From: Nathanael Ritz <nathanritz@gmail.com>
Date: Thu, 2 Jul 2026 17:14:58 -0600
Message-ID: 
 <CAHxYnaN_3kC4M0a+M=3SocsLBVs6RiUCtg0J4UaVb1jTMhp64g@mail.gmail.com>
To: Songbo Bu <bluedognull@gmail.com>
Content-Type: multipart/alternative; boundary="000000000000cbc0e50655a8fab7"
Message-ID-Hash: 7M2SOPYQLT6Q5IWPN4EUQHUBHDMFP646
CC: UFMRG IRTF <ufmrg@irtf.org>, "seat@ietf.org" <seat@ietf.org>
Precedence: list
Subject: =?utf-8?q?=5BUfmrg=5D_Re=3A_=5BSeat=5D_Comments_on_formal_analysis_of_relay_?=
 =?utf-8?q?attacks_in_attested_TLS_=28CVE-2026-33697=29?=
Archived-At: 
 <https://mailarchive.ietf.org/arch/msg/ufmrg/-TEtlo3M0qnchWV28dw60sDEZBw>

--000000000000cbc0e50655a8fab7
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Hi Songbo,

Below with [NR]

On Thu, Jul 2, 2026 at 7:55=E2=80=AFAM Songbo Bu <bluedognull@gmail.com> wr=
ote:

> 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=E2=80=99t 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.=E2=80=99s work made it very clear that some binder compo=
sitions
in their evaluation suite cannot even survive standard TLS assumptions
(which is the heart of the CVE finding, as I understand it). That=E2=80=99s=
 an
undeniably valuable contribution to the community. I believe another
valuable service to the community is scientific curiosity that explores
reasonable constructive mitigations. That=E2=80=99s 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=E2=80=99t believe =E2=80=9Crelease gate=E2=80=9D is a standard p=
rotocol 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
=E2=80=9Csimpler=E2=80=9D as a blanket assessment). I believe Markus alread=
y explained this
in the other thread, but to share some examples in =E2=80=9Cmy own words=E2=
=80=9D:

[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 =E2=80=94 not cryptographic. I hope that helps clar=
ify 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 <nathanritz@gmail.com>
> 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 <bluedognull@gmail.com> 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 <
> muhammad_usama.sardar@tu-dresden.de> 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 activ=
e
> session parameters being evaluated. I am curious if you would disagree wi=
th
> this approach.
> >
> > Thanks for sharing this property. Unfortunately, we don't like this
> property and approach because it checks only for limited traces. We belie=
ve
> our property is stronger than this.
> >
> > As Sec. 6.3 of paper [25] mentions, the goal of the property is to chec=
k
> 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 tha=
t
> 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 som=
e
> 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 cour=
se.
> >
> > Cheers,
> >
> > Nathanael
> >
> > [25]
> https://www.researchgate.net/publication/408219182_Intra-handshakefail_CV=
E-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 <
> muhammad_usama.sardar@tu-dresden.de> wrote:
> >
> > Hi Nathanael,
> > On 01.07.26 02:27, Nathanael Ritz wrote:
> >
> > On Tue, 30 Jun 2026 at 14:11, Muhammad Usama Sardar <
> muhammad_usama.sardar@tu-dresden.de> wrote:
> >
> > Also, please note that in ProVerif, variables that appear only after th=
e
> arrow (=3D=3D>) 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 activ=
e
> session parameters being evaluated. I am curious if you would disagree wi=
th
> this approach.
> >
> > Thanks for sharing this property. Unfortunately, we don't like this
> property and approach because it checks only for limited traces. We belie=
ve
> our property is stronger than this.
> >
> > As Sec. 6.3 of paper [25] mentions, the goal of the property is to chec=
k
> 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 som=
e
> are in progress. We will document the detailed analysis and exploits in a
> separate paper and then share with the WG/RG.
> >
> > =3D=3D=3D
> >
> > 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_CV=
E-2026-33697_High-severity_CVE_in_Attested_TLS
> >
> > On Tue, 30 Jun 2026 at 19:28, Songbo Bu <bluedognull@gmail.com> 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 <nathanritz@gmail.co=
m>
> wrote:
> > > Hi everyone,
> > >
> > > I have additional feedback to share regarding some of the new comment=
s
> in this thread.
> > >
> > > My thoughts are offered below with [NR]:
> > >
> > > On Tue, 30 Jun 2026 at 14:11, Muhammad Usama Sardar <
> muhammad_usama.sardar@tu-dresden.de> wrote:
> > >
> > > On 28.06.26 22:32, Nathanael Ritz wrote:
> > >
> > > ## Regarding correlation goals (G3 =3D> G2 =3D> 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. Tha=
nk
> 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 messag=
e
> > > L1 <=3D L2 <=3D L3
> > >
> > > ~~~
> > >
> > > On Tue, 30 Jun 2026 at 14:11, Muhammad Usama Sardar <
> muhammad_usama.sardar@tu-dresden.de> 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 eleme=
nt
> (e.g., as Sec. 6.1 clearly cites Bhargavan et al.'s foundational paper fo=
r
> TLS 1.3 [26]).
> > >
> > > Also, please note that in ProVerif, variables that appear only after
> the arrow (=3D=3D>) 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 t=
he
> 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 quer=
y
> [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 a=
m
> 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 th=
e
> server's key exchange choice:
> > >
> > > ~~~
> > > `kc1 =3D 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 mathematicall=
y
> 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 acti=
ve
> 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] a=
t
> 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/f96761deeee3b7574=
959eec9f44fe940b33dcbde/README.md?plain=3D1#L58
> > >
> > > [25]
> https://www.researchgate.net/publication/408219182_Intra-handshakefail_CV=
E-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/188409b866b8fc021=
0c8e5d9579e441aa91ce326/binder3/tls-lib-simple.pvl#L582-L638
> > >
> > > [28]
> https://github.com/nathanaelritz/relay-attacks-in-attested-tls/tree/binde=
r3-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 <
> muhammad_usama.sardar@tu-dresden.de> 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 eleme=
nt
> (e.g., as Sec. 6.1 clearly cites Bhargavan et al.'s foundational paper fo=
r
> TLS 1.3 [26]).
> > >
> > > Also, please note that in ProVerif, variables that appear only after
> the arrow (=3D=3D>) are existentially quantified.
> > >
> > > Hope that helps.
> > >
> > > On 28.06.26 22:32, Nathanael Ritz wrote:
> > >
> > > ## Regarding correlation goals (G3 =3D> G2 =3D> 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. Tha=
nk
> 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_CV=
E-2026-33697_High-severity_CVE_in_Attested_TLS
> > >
> > > [26] https://ieeexplore.ieee.org/document/7958594/
> > >
> > > -----------------------------------------------
> > >
> > > From: Nathanael Ritz <nathanritz@gmail.com>
> > > 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 <bluedognull@gmail.com>
> > > Cc: <seat@ietf.org>, <ufmrg@irtf.org>, Muhammad Usama Sardar <
> muhammad_usama.sardar@tu-dresden.de>
> > >
> > > 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 justifie=
d.
> 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 topi=
c
> 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 materi=
al
> 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, b=
ut
> different from the technical evaluation of the formal model discussed her=
e.
> 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 th=
e
> topic in more detail with you there, and feel free to reference this thre=
ad
> if you do go ahead.
> > >
> > > ---
> > >
> > > ## Regarding correlation goals (G3 =3D> G2 =3D> 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 o=
n
> 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)) =3D=3D> (kc1 =3D 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)) =3D=3D> (kc1 =3D 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 i=
s,
> by excluding weak DH groups, weak hash algorithms, or a bad group element
> -- all of which are already prohibited in compliant TLS 1.3 implementatio=
ns
> 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-pos=
t-handshake-vs-intra-hand
> > >
> > > -----------------------------------------------
> > >
> > > From: Nathanael Ritz <nathanritz@gmail.com>
> > > 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: seat@ietf.org <seat@ietf.org>
> > > Cc: <ufmrg@irtf.org>, Songbo Bu <bluedognull@gmail.com>, Muhammad
> Usama Sardar <muhammad_usama.sardar@tu-dresden.de>
> > >
> > > 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 <bluedognull@gmail.com> 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 model=
s
> 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-Dra=
ft
> 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, a=
nd
> whether that property cannot be achieved by a simpler post-handshake desi=
gn.
> > >
> > > [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 i=
n
> their recent -04 revision.
> > >
> > > [NR] I am hopeful that such evaluations on concrete proposals based o=
n
> **active** Internet-Drafts under discussion with the SEAT WG will continu=
e,
> 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 chan=
ge
> 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 securi=
ty
> 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 th=
is
> 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 <
> muhammad_usama.sardar@tu-dresden.de> wrote:
> > >
> > > Hi Nathanael,
> > >
> > > [...]
> > >
> > > I respectfully request that the authors update their ProVerif
> artifacts to accurately reflect the actual binder derivations (such as th=
e
> `HKDF-Expand-Label` derivation in Section 5.1.1) and the standard
> `CertificateVerify` boundaries established by the WG's drafts if they hav=
e
> 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 futur=
e
> energy on carefully considering the merits of active indivual I-Ds such a=
s
> `draft-fossati-seat-expat` or `draft-fossati-seat-early-attestation`. Bot=
h
> 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=E2=80=99 applicability to inform such intuition has been=
 backed by
> their technical merits. As mentioned earlier, I identified two constructi=
ve
> elements causing the models to strictly fall out of alignment with the
> drafts' specifications, and the authors have not disputed this misalignme=
nt.
> > >
> > > [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 fe=
w
> 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/f96761deeee3b7574=
959eec9f44fe940b33dcbde
> > >
> > > [12]
> https://github.com/CCC-Attestation/formal-spec-KBS/blob/f96761deeee3b7574=
959eec9f44fe940b33dcbde/README.md?plain=3D1#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 <bluedognull@gmail.com>
> > > Date: Sat, 27 Jun 2026 at 09:02
> > > Subject: [Seat] Re: Comments on formal analysis of relay attacks in
> attested TLS
> > > To: <seat@ietf.org>, <ufmrg@irtf.org>, Muhammad Usama Sardar <
> muhammad_usama.sardar@tu-dresden.de>
> > >
> > > 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, a=
nd
> whether that property cannot be achieved by a simpler post-handshake desi=
gn.
> > >
> > > If a proposed construction is believed to bind attestation state to
> TLS in a way that differs from the current artifact, a minimal model chan=
ge
> 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 -- seat@ietf.org
> > > To unsubscribe send an email to seat-leave@ietf.org
> > >
> > > -----------------------------------------------
> > >
> > > From: Muhammad Usama Sardar <muhammad_usama.sardar@tu-dresden.de>
> > > 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 <nathanritz@gmail.com>, seat@ietf.org <
> seat@ietf.org>
> > > Cc: <ufmrg@irtf.org>
> > >
> > > 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 w=
e
> 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 wel=
l.
> > >
> > > This is also reflected in acknowledgments, where folks who contribute=
d
> 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 abou=
t
> 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 ou=
r
> formal analysis contribution to the WG questions the claim on the need fo=
r
> intra-handshake attestation in this combination.
> > >
> > > ## B. The CA-backed key (`pubLTK`) is never bound into the attestatio=
n
> 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 Confidentia=
l
> Computing workload in the first place?
> > >
> > > In every single model (`binder1` through `binder7`, `aggregate`, and
> `proposal`), the `rdata` value=E2=80=94which is what the Attestation Key =
(`privAK`)
> actually signs to generate the evidence=E2=80=94is 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 "sugge=
st
> 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 combinatio=
n
> 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 th=
e
> `HKDF-Expand-Label` derivation in Section 5.1.1) and the standard
> `CertificateVerify` boundaries established by the WG's drafts if they hav=
e
> 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 futur=
e
> energy on carefully considering the merits of active indivual I-Ds such a=
s
> `draft-fossati-seat-expat` or `draft-fossati-seat-early-attestation`. Bot=
h
> 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 complexit=
y
> and thus additional attack surface. We would like to see much stronger
> arguments than have been presented to date before we absorb this complexi=
ty.
> > >
> > > 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/f96761deeee3b7574=
959eec9f44fe940b33dcbde
> > >
> > > [12]
> https://github.com/CCC-Attestation/formal-spec-KBS/blob/f96761deeee3b7574=
959eec9f44fe940b33dcbde/README.md?plain=3D1#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 <nathanritz@gmail.com>
> > > Date: Fri, 26 Jun 2026 at 01:08
> > > Subject: Comments on formal analysis of relay attacks in attested TLS
> (CVE-2026-3369)
> > > To: seat@ietf.org <seat@ietf.org>
> > > Cc: <ufmrg@irtf.org>
> > >
> > > 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 fe=
w
> 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 =3D sign(privEK ,hash(hash_algo,log_CRT)) in
> > > let sg_LTK =3D 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) =3D true then
> > > if verify(pubLTK,hash(shash_algo,log_CRT),s_LTK) =3D true then
> > > ```
> > >
> > > In case it is not apparent, this dual-signature `CV_Ext` mechanism ha=
s
> no basis in any IETF proposed standard.
> > >
> > > Therefore, I propose that if Usama and collaborators are serious abou=
t
> 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 attestatio=
n
> evidence (`rdata`)
> > >
> > > In every single model (`binder1` through `binder7`, `aggregate`, and
> `proposal`), the `rdata` value=E2=80=94which is what the Attestation Key =
(`privAK`)
> actually signs to generate the evidence=E2=80=94is 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 =3D rand2bs(cr)`
> > > (Client's TLS nonce)
> > >
> > > * **Binder 2:** `let rdata =3D rand2bs(ar)`
> > > (Client's attestation nonce)
> > >
> > > * **Binder 3:** `let rdata =3D exp0`
> > > (Early exporter)
> > >
> > > * **Binder 4:** `let rdata =3D pub2bs(pubEK)`
> > > (Ephemeral public key)
> > >
> > > * **Binder 5:** `let rdata =3D (ar,exp0)`
> > > (Attestation nonce + Early exporter)
> > >
> > > * **Binder 6:** `let rdata =3D (ar,pubEK)`
> > > (Attestation nonce + Ephemeral public key)
> > >
> > > * **Binder 7:** `let rdata =3D (ar,exp0,pubEK)`
> > > (Attestation nonce + Early exporter + Ephemeral public key)
> > >
> > > * **Aggregate:** `let rdata =3D (cb,pubEK)`
> > > (Custom HS-derived exporter + Ephemeral public key)
> > >
> > > * **Proposal:** `let cb =3D kdf_exp(hs,log_SH) in let rdata =3D
> (ar,cb,pubEK)`
> > > (Attestation nonce + Custom HS-derived exporter + Ephemeral public ke=
y)
> > >
> > > ```
> > >
> > > 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 sessi=
on
> 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 "sugge=
st
> 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 th=
e
> `HKDF-Expand-Label` derivation in Section 5.1.1) and the standard
> `CertificateVerify` boundaries established by the WG's drafts if they hav=
e
> 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 transitio=
n
> 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 futur=
e
> energy on carefully considering the merits of active indivual I-Ds such a=
s
> `draft-fossati-seat-expat` or `draft-fossati-seat-early-attestation`. Bot=
h
> 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/f96761deeee3b7574=
959eec9f44fe940b33dcbde
> > >
> > > [12]
> https://github.com/CCC-Attestation/formal-spec-KBS/blob/f96761deeee3b7574=
959eec9f44fe940b33dcbde/README.md?plain=3D1#L58
> > >
> > > -----------------------------------------------
> > >
> > > From: Muhammad Usama Sardar <muhammad_usama.sardar@tu-dresden.de>
> > > Date: Thu, 25 Jun 2026 at 16:19
> > > Subject: [Seat] Re: Relay Attacks in Intra-handshake Attestation for
> Confidential Agentic AI Systems
> > > To: seat@ietf.org <seat@ietf.org>, UFMRG IRTF <ufmrg@irtf.org>
> > >
> > > 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 attestati=
on
> 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-handshak=
e
> 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 th=
e
> 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 <nathanritz@gmail.com>
> > > Date: Mon, 22 Jun 2026 at 11:12
> > > Subject: Re: [Seat] Re: Relay Attacks in Intra-handshake Attestation
> for Confidential Agentic AI Systems
> > > To: seat@ietf.org <seat@ietf.org>
> > >
> > > 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 <
> muhammad_usama.sardar@tu-dresden.de> wrote:
> > >
> > > Hi Paul,
> > >
> > > [...] Formal (Symbolic and paper-and-pen) analyses is the most seriou=
s
> 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 cours=
e,
> 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 som=
e
> 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 whic=
h
> binding mechanism or point us to any missing real-world implementation fo=
r
> 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 valu=
e
> 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 seco=
nd
> trust anchor. Usama also noted this sentiment in his IETF-125 follow-up t=
o
> 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 checke=
d
> against a standard CA-backed webPKI certificate whose private key resides
> outside the TEE.
> > >
> > > [NR] Therefore, beyond merely updating the single `rdata` value -- th=
e
> formal model needs to evaluate the security properties when a CA-backed
> signing key (LTK) is composed with Evidence signed over by the attestatio=
n
> 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` (extende=
d
> 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 sha=
re
> a model that explicitly evaluates the binder mechanism from
> `draft-fossati-seat-early-attestation-04`, where the assumptions align wi=
th
> 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-ta=
lks-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.h=
tml#section-5.2-2
> > >
> > > [8]
> https://mailarchive.ietf.org/arch/msg/seat/zD1NTnUEdRM5SayHxXfuO9robTA/
> > >
> > > On Thu, 18 Jun 2026 at 15:58, Muhammad Usama Sardar <
> muhammad_usama.sardar@tu-dresden.de> wrote:
> > >
> > > Hi Paul,
> > >
> > > On 18.06.26 22:45, Paul Wouters wrote:
> > >
> > > On Jun 16, 2026, at 17:02, Muhammad Usama Sardar [<
> muhammad_usama.sardar@tu-dresden.de>](mailto:
> muhammad_usama.sardar@tu-dresden.de) 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 writin=
g
> 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 thin=
g
> 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 bindi=
ng
> 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 TE=
E
> 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 t=
he
> 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
>

--000000000000cbc0e50655a8fab7
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div dir=3D"ltr"><div><div><div dir=3D"auto">Hi Songbo,</d=
iv><div dir=3D"auto"><br></div><div dir=3D"auto">Below with [NR]</div><div>=
<br><div class=3D"gmail_quote"></div></div></div></div><div><div><div dir=
=3D"ltr" class=3D"gmail_attr">On Thu, Jul 2, 2026 at 7:55=E2=80=AFAM Songbo=
 Bu &lt;<a href=3D"mailto:bluedognull@gmail.com" target=3D"_blank">bluedogn=
ull@gmail.com</a>&gt; wrote:<br></div><blockquote class=3D"gmail_quote" sty=
le=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);paddi=
ng-left:1ex">Hi Nathanael,<br>
<br>
Thanks for the clarification. My current understanding is that adding<br>
extra assumptions usually weakens the protocol-level claim, even if it<br>
makes a proof go through.</blockquote><div dir=3D"auto"><br></div></div></d=
iv><div><div><div dir=3D"auto"><div style=3D"font-size:inherit" dir=3D"auto=
">[NR] To be very clear about my stance, I think &quot;typical cryptographi=
c assumptions&quot; is exactly the opposite of &quot;extra assumptions&quot=
;. 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-complian=
t implementations that intentionally break standard cryptographic guarantee=
s only, I don=E2=80=99t really think=C2=A0we are analyzing=C2=A0RA composit=
ion with RFC8446(bis) anymore.=C2=A0</div><div style=3D"font-size:inherit" =
dir=3D"auto"><br></div><div style=3D"font-size:inherit" dir=3D"auto">[NR] B=
y all means, if a use-case and threat model requires a team to assume the s=
ecure transport protocol they&#39;ve chosen to compose with cannot be deeme=
d trustworthy, then they are absolutely encouraged to take the appropriate =
defense-in-depth approaches that suits their specific requirements or deplo=
yment policies. And of course -- there is absolutely nothing wrong with for=
mal 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.=C2=A0=C2=A0</div><div style=3D"font-size:inherit" dir=3D"auto">=
<br></div><div style=3D"font-size:inherit" dir=3D"auto">[NR] Sardar et al.=
=E2=80=99s work made it very clear that some binder compositions in their e=
valuation suite cannot even survive standard TLS assumptions (which is the =
heart of the CVE finding, as I understand it). That=E2=80=99s an undeniably=
 valuable contribution to the community. I believe another valuable service=
 to the community is scientific curiosity that explores reasonable construc=
tive mitigations. That=E2=80=99s my position.=C2=A0</div><div style=3D"font=
-size:inherit" dir=3D"auto"><br></div></div></div></div><div><div><blockquo=
te class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px =
solid rgb(204,204,204);padding-left:1ex" dir=3D"auto">
So the key question for me is: under the standard TLS / attacker<br>
model, what property does the intra-handshake attestation path provide<br>
that a simpler post-handshake attestation path with a strict<br>
application-data release gate does not provide?</blockquote><div dir=3D"aut=
o"><br></div></div></div><div><div><div dir=3D"auto"><div style=3D"font-siz=
e:inherit" dir=3D"auto">[NR] I don=E2=80=99t believe =E2=80=9Crelease gate=
=E2=80=9D is a standard protocol term; what I believe you are describing st=
ructurally translates to an application-layer proxy or a sidecar deployment=
 pattern. While a post-handshake window can use an external sidecar to with=
hold or buffer application data until an attestation credential (such as Ev=
idence or an Attestation Result) is appraised, it represents uniquely archi=
tectural boundaries than an intra-handshake path (and I would caution again=
st a blanket assessment of =E2=80=9Csimpler=E2=80=9D as a blanket assessmen=
t). I believe Markus already explained this in the other thread, but to sha=
re some examples in =E2=80=9Cmy own words=E2=80=9D:<br style=3D"font-size:i=
nherit"> <br style=3D"font-size:inherit">[NR] *Proactive Prevention vs. Exp=
osure Boundary*: Intra-handshake attestation ensures that the transport sta=
te machine explicitly withholds the progression to application data exchang=
e until the Relying Party is satisfied. If validation fails, it triggers a =
fatal handshake error before a single byte of application data is ever proc=
essed. Post-handshake attestation, by definition, operates within an alread=
y-established session where application data may technically already be flo=
wing at the network layer. A &quot;release gate&quot; sidecar can mitigate =
exposure going forward, but it cannot retroactively protect application dat=
a or prevent the initial handshake state from completing, although this can=
 also potentially be addressed with a shim. <br style=3D"font-size:inherit"=
><br style=3D"font-size:inherit">[NR] *Fault handling considerations*: When=
 remote attestation is integrated into the intra-handshake window, a verifi=
cation failure maps natively to standard transport protocol handshake-failu=
re handling. In a post-handshake model, failure handling must occur entirel=
y outside the transport handshake, where an appraisal policy is used to det=
ermine whether to tear down an active session or perhaps dynamically restri=
ct it to a subset of functionality.<br style=3D"font-size:inherit"><br styl=
e=3D"font-size:inherit">[NR] Ultimately, I view the two timing models as un=
ique approaches that can address specific requirements that they naturally =
lend their strengths towards. Intra-handshake can be used to establish base=
line assurance (under typical TLS assumptions) before the session becomes u=
sable (structurally avoiding race conditions), whereas post-handshake handl=
es dynamic state tracking and periodic re-attestation over long-lived conne=
ctions. I believe they are complementary controls, not mutually exclusive a=
lternatives.<br style=3D"font-size:inherit"><br style=3D"font-size:inherit"=
>[NR] Again, my perspective is that most of this is actually architectural =
considerations for SEAT =E2=80=94 not cryptographic. I hope that helps clar=
ify my point of view, but I encourage the WG to review the thread I linked =
at [30] for input from other participant&#39;s besides myself.</div><div st=
yle=3D"font-size:inherit" dir=3D"auto"><br></div></div><blockquote class=3D=
"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(2=
04,204,204);padding-left:1ex" dir=3D"auto">
Best,<br>
Songbo</blockquote><div dir=3D"auto"><br></div><div dir=3D"auto">Cheers,</d=
iv><div dir=3D"auto">Nathanael</div></div></div><div dir=3D"auto"><br></div=
><div dir=3D"auto">[30]=C2=A0<a href=3D"https://mailarchive.ietf.org/arch/m=
sg/seat/fTvLgg27YGQUaCWDh-gnhSgnHz4/" rel=3D"noreferrer" target=3D"_blank">=
https://mailarchive.ietf.org/arch/msg/seat/fTvLgg27YGQUaCWDh-gnhSgnHz4/</a>=
</div><div dir=3D"auto"><br></div></div><div><div><div><div class=3D"gmail_=
quote"><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;=
border-left:1px solid rgb(204,204,204);padding-left:1ex" dir=3D"auto">
On Wed, 1 Jul 2026 20:22:13 -0600, Nathanael Ritz &lt;<a href=3D"mailto:nat=
hanritz@gmail.com" target=3D"_blank">nathanritz@gmail.com</a>&gt; wrote:<br=
>
&gt; Hi everyone,<br>
&gt;<br>
&gt; I have some additional thoughts to offer in this thread.<br>
&gt;<br>
&gt; My thoughts are offered below with [NR]:<br>
&gt;<br>
&gt; On Tue, 30 Jun 2026 at 19:28, Songbo Bu &lt;<a href=3D"mailto:bluedogn=
ull@gmail.com" target=3D"_blank">bluedognull@gmail.com</a>&gt; wrote:<br>
&gt;<br>
&gt; Hi all,<br>
&gt;<br>
&gt; [...] I think it would help the SEAT/UFMRG review to keep four items<b=
r>
&gt; explicit for each proposed design:<br>
&gt;<br>
&gt; - what channel/evidence binding goal is being checked;<br>
&gt; - whether the claim is unconditional in the stated model, or<br>
&gt; conditional on excluding named bad events;<br>
&gt; - what concrete value binds Evidence or an Attestation Result to the<b=
r>
&gt; TLS channel and endpoint identity; and<br>
&gt; - what verifier and application-data release behavior is required when=
<br>
&gt; that value is absent, stale, malformed, or mismatched.<br>
&gt;<br>
&gt; [NR] I don&#39;t have much to add on the considerations above for now;=
 however I do think they are reasonable. As is the discussion with Markus r=
ecently speaking to similiar topics, including pros and cons for the variou=
s attestation timings [30].<br>
&gt;<br>
&gt; On Wed, 1 Jul 2026 at 02:25, Muhammad Usama Sardar &lt;<a href=3D"mail=
to:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_usama.sa=
rdar@tu-dresden.de</a>&gt; wrote:<br>
&gt;<br>
&gt; Hi Nathanael,<br>
&gt;<br>
&gt; [NR] I am aware of existential quantification, and you are correct tha=
t placing the unbound `cr&#39;` and `sr&#39;` variables on the right side o=
f the implication arrow evaluates the condition globally rather than scopin=
g it to the specific session.<br>
&gt;<br>
&gt; Great. We are finally on the same page.<br>
&gt;<br>
&gt; [NR] [...] I updated the state events to explicitly bind the session n=
onces 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 t=
ie the weak-crypto conditions strictly to the active session parameters bei=
ng evaluated. I am curious if you would disagree with this approach.<br>
&gt;<br>
&gt; Thanks for sharing this property. Unfortunately, we don&#39;t like thi=
s property and approach because it checks only for limited traces. We belie=
ve our property is stronger than this.<br>
&gt;<br>
&gt; As Sec. 6.3 of paper [25] mentions, the goal of the property is to che=
ck how strongly Evidence is bound to the connection.<br>
&gt;<br>
&gt; Would you like to give it another try by proposing a better property?<=
br>
&gt;<br>
&gt; [NR] While I think it&#39;s unfortunate that my demonstrated property =
may not meet everyone&#39;s apparent tastes; since the property already sho=
ws that the examined localized attack can be mitigated by compliant TLS 1.3=
 implementations (along with the usual caveats that come from symbolic anal=
ysis -- I think there *are* better binder choices than the Early Exporter t=
o chose from in practice)... I really don&#39;t think any further effort fr=
om me is necessary right now.<br>
&gt;<br>
&gt; We have practical proof of concept of attacks for a few binders and so=
me are in progress. We will document the detailed analysis and exploits in =
a separate paper and then share with the WG/RG.<br>
&gt;<br>
&gt; [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=
.<br>
&gt;<br>
&gt; Cheers,<br>
&gt;<br>
&gt; Nathanael<br>
&gt;<br>
&gt; [25] <a href=3D"https://www.researchgate.net/publication/408219182_Int=
ra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS" rel=3D"n=
oreferrer" target=3D"_blank">https://www.researchgate.net/publication/40821=
9182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS</=
a><br>
&gt;<br>
&gt; [30] <a href=3D"https://mailarchive.ietf.org/arch/msg/seat/fTvLgg27YGQ=
UaCWDh-gnhSgnHz4/" rel=3D"noreferrer" target=3D"_blank">https://mailarchive=
.ietf.org/arch/msg/seat/fTvLgg27YGQUaCWDh-gnhSgnHz4/</a><br>
&gt;<br>
&gt; On Wed, 1 Jul 2026 at 02:25, Muhammad Usama Sardar &lt;<a href=3D"mail=
to:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_usama.sa=
rdar@tu-dresden.de</a>&gt; wrote:<br>
&gt;<br>
&gt; Hi Nathanael,<br>
&gt; On 01.07.26 02:27, Nathanael Ritz wrote:<br>
&gt;<br>
&gt; On Tue, 30 Jun 2026 at 14:11, Muhammad Usama Sardar &lt;<a href=3D"mai=
lto:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_usama.s=
ardar@tu-dresden.de</a>&gt; wrote:<br>
&gt;<br>
&gt; Also, please note that in ProVerif, variables that appear only after t=
he arrow (=3D=3D&gt;) are existentially quantified.<br>
&gt;<br>
&gt; Hope that helps.<br>
&gt;<br>
&gt; [NR] I am aware of existential quantification, and you are correct tha=
t placing the unbound `cr&#39;` and `sr&#39;` variables on the right side o=
f the implication arrow evaluates the condition globally rather than scopin=
g it to the specific session.<br>
&gt;<br>
&gt; Great. We are finally on the same page.<br>
&gt;<br>
&gt; [NR] [...] I updated the state events to explicitly bind the session n=
onces 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 t=
ie the weak-crypto conditions strictly to the active session parameters bei=
ng evaluated. I am curious if you would disagree with this approach.<br>
&gt;<br>
&gt; Thanks for sharing this property. Unfortunately, we don&#39;t like thi=
s property and approach because it checks only for limited traces. We belie=
ve our property is stronger than this.<br>
&gt;<br>
&gt; As Sec. 6.3 of paper [25] mentions, the goal of the property is to che=
ck how strongly Evidence is bound to the connection.<br>
&gt;<br>
&gt; Would you like to give it another try by proposing a better property?<=
br>
&gt;<br>
&gt; We have practical proof of concept of attacks for a few binders and so=
me are in progress. We will document the detailed analysis and exploits in =
a separate paper and then share with the WG/RG.<br>
&gt;<br>
&gt; =3D=3D=3D<br>
&gt;<br>
&gt; In the mean time, we would love to hear some feedback from the formal =
methods experts in UFMRG.<br>
&gt;<br>
&gt; Best regards,<br>
&gt;<br>
&gt; Usama, Slava, and Jean-Marie<br>
&gt;<br>
&gt; [25] <a href=3D"https://www.researchgate.net/publication/408219182_Int=
ra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS" rel=3D"n=
oreferrer" target=3D"_blank">https://www.researchgate.net/publication/40821=
9182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS</=
a><br>
&gt;<br>
&gt; On Tue, 30 Jun 2026 at 19:28, Songbo Bu &lt;<a href=3D"mailto:bluedogn=
ull@gmail.com" target=3D"_blank">bluedognull@gmail.com</a>&gt; wrote:<br>
&gt;<br>
&gt; Hi all,<br>
&gt;<br>
&gt; I want to add a short implementer-side point, because it affects how I=
<br>
&gt; read the current disagreement.<br>
&gt;<br>
&gt; My reading is that the useful distinction is between (1) a security<br=
>
&gt; goal stated for the attested TLS construction and (2) extra conditions=
<br>
&gt; that remove weak hashes, weak DH shares, bad elements, missing or<br>
&gt; malformed binders, or stale or mismatched evidence from the execution<=
br>
&gt; space. In implementation work, those are not just background facts we<=
br>
&gt; can assume for every connection. They are adversarial or invalid cases=
<br>
&gt; that a protocol stack must reject, or handle fail-closed, before any<b=
r>
&gt; relying party treats the attestation result as binding to the channel.=
<br>
&gt;<br>
&gt; So I think it would help the SEAT/UFMRG review to keep four items<br>
&gt; explicit for each proposed design:<br>
&gt;<br>
&gt; - what channel/evidence binding goal is being checked;<br>
&gt; - whether the claim is unconditional in the stated model, or<br>
&gt; conditional on excluding named bad events;<br>
&gt; - what concrete value binds Evidence or an Attestation Result to the<b=
r>
&gt; TLS channel and endpoint identity; and<br>
&gt; - what verifier and application-data release behavior is required when=
<br>
&gt; that value is absent, stale, malformed, or mismatched.<br>
&gt;<br>
&gt; This is also why I think the long-term identity / CA-backed key<br>
&gt; question should remain explicit rather than implicit. If a design<br>
&gt; relies on a CA-backed LTK/TIK inside a confidential workload, the<br>
&gt; review still needs to state how that identity is assigned, provisioned=
<br>
&gt; into the workload, and bound to attestation evidence under the<br>
&gt; confidential-computing threat model. Otherwise an implementer may pass=
<br>
&gt; a formal condition while still leaving unclear which trust anchor or<b=
r>
&gt; workload identity the relying party is accepting.<br>
&gt;<br>
&gt; I am not trying to settle all of the formal-model questions in this<br=
>
&gt; email. My narrower point is that, from an implementation perspective,<=
br>
&gt; &quot;the connection does not use weak parameters / malformed state /<=
br>
&gt; mismatched evidence&quot; is a property that the protocol and verifier=
 have<br>
&gt; to enforce or check. It should not silently become a global<br>
&gt; precondition outside the review boundary.<br>
&gt;<br>
&gt; Best,<br>
&gt; Songbo<br>
&gt;<br>
&gt; On Tue, 30 Jun 2026 18:27:57 -0600, Nathanael Ritz &lt;<a href=3D"mail=
to:nathanritz@gmail.com" target=3D"_blank">nathanritz@gmail.com</a>&gt; wro=
te:<br>
&gt; &gt; Hi everyone,<br>
&gt; &gt;<br>
&gt; &gt; I have additional feedback to share regarding some of the new com=
ments in this thread.<br>
&gt; &gt;<br>
&gt; &gt; My thoughts are offered below with [NR]:<br>
&gt; &gt;<br>
&gt; &gt; On Tue, 30 Jun 2026 at 14:11, Muhammad Usama Sardar &lt;<a href=
=3D"mailto:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_=
usama.sardar@tu-dresden.de</a>&gt; wrote:<br>
&gt; &gt;<br>
&gt; &gt; On 28.06.26 22:32, Nathanael Ritz wrote:<br>
&gt; &gt;<br>
&gt; &gt; ## Regarding correlation goals (G3 =3D&gt; G2 =3D&gt; G1)<br>
&gt; &gt;<br>
&gt; &gt; As presented in Sec. 6.4 in paper [0], this proof is paper-and-pe=
n based, and not ProVerif based. Please clarify your concern precisely. Tha=
nk you!<br>
&gt; &gt;<br>
&gt; &gt; [NR] I am pretty confident this is entirely non-responsive. I enc=
ourage the authors to carefully consider the context of the discussion befo=
re asking other participants for what some may consider excessive and redun=
dant requests to clarify one&#39;s &quot;concern precisely&quot;, when the =
authors&#39; own source code already should already make such distinctions =
clear [27] .<br>
&gt; &gt;<br>
&gt; &gt; [NR] For those not following every citation, I mean &quot;Goal G1=
&quot; through &quot;Goal G3&quot; across 3 levels of binding to TLS sessio=
n:<br>
&gt; &gt;<br>
&gt; &gt; ~~~<br>
&gt; &gt; L1. gxy (gx,gy)<br>
&gt; &gt; L2. kch (up to ServerHello)<br>
&gt; &gt; L3. kc (up to ServerFinished): may include ID_S in Certificate me=
ssage<br>
&gt; &gt; L1 &lt;=3D L2 &lt;=3D L3<br>
&gt; &gt;<br>
&gt; &gt; ~~~<br>
&gt; &gt;<br>
&gt; &gt; On Tue, 30 Jun 2026 at 14:11, Muhammad Usama Sardar &lt;<a href=
=3D"mailto:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_=
usama.sardar@tu-dresden.de</a>&gt; wrote:<br>
&gt; &gt;<br>
&gt; &gt; We would like to clarify a couple of misunderstandings to avoid t=
alking past each other:<br>
&gt; &gt;<br>
&gt; &gt; - What you are proposing adding as conditions actually seems to t=
ranslate to the assumption &#39;there exists no connection in the world tha=
t ever uses weak hashes, weak DH or bad element.&#39; So your proposed prop=
erty 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 secu=
re, then my connection is secure too; so could you clarify the point of you=
r proposed property?<br>
&gt; &gt;<br>
&gt; &gt; - We believe you can agree that achieving a property without addi=
tional assumptions is stronger than achieving a property with the additiona=
l assumptions that every connection in the world is secure. It&#39;s as sim=
ple as that.<br>
&gt; &gt;<br>
&gt; &gt; Because of above reasons, we disagree with you.<br>
&gt; &gt;<br>
&gt; &gt; [NR] I believe a technically responsive reply to my earlier comme=
nts, (or to these) would be to follow-up with a model and trace of a concre=
te counter-example that demonstrates a correlation failure for G2 or G3 wit=
h mechanism #3 *without* relying on an explicit cryptographic downgrade.<br=
>
&gt; &gt;<br>
&gt; &gt; In any case, Sec. 6.1 in the paper [25] is clear on the threat mo=
del, and for TLS, it is typical to consider weak hashes, weak DH, or bad el=
ement (e.g., as Sec. 6.1 clearly cites Bhargavan et al.&#39;s foundational =
paper for TLS 1.3 [26]).<br>
&gt; &gt;<br>
&gt; &gt; Also, please note that in ProVerif, variables that appear only af=
ter the arrow (=3D=3D&gt;) are existentially quantified.<br>
&gt; &gt;<br>
&gt; &gt; Hope that helps.<br>
&gt; &gt;<br>
&gt; &gt; [NR] I am aware of existential quantification, and you are correc=
t that placing the unbound `cr&#39;` and `sr&#39;` variables on the right s=
ide of the implication arrow evaluates the condition globally rather than s=
coping 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 concr=
ete counter-example to share? These are the kinds of questions I wonder abo=
ut during these exchanges.<br>
&gt; &gt;<br>
&gt; &gt; However, the models reveal that if a mechanism achieves &quot;Lev=
el 1&quot; (G1) binding or higher (as seen in mechanisms #3, 5, 7, and the =
proposal), correlation to &quot;Level 2&quot; (G2) and &quot;Level 3&quot; =
(G3) naturally follows under the standard cryptographic assumptions of TLS =
1.3.Please see #1 and #2 above.<br>
&gt; &gt;<br>
&gt; &gt; ## Minimal demonstration under standard cryptographic assumptions=
<br>
&gt; &gt;<br>
&gt; &gt; In the current models, the G2 and G3 queries return false. Howeve=
r, when queries are conditioned to exclude the model&#39;s own weak-cryptog=
raphy events, they return true.<br>
&gt; &gt; Please see #1 and #2 above.<br>
&gt; &gt;<br>
&gt; &gt; We welcome any constructive technical feedback.<br>
&gt; &gt;<br>
&gt; &gt; [NR] I believe I have offered the authors plenty of constructive =
feedback, but since they appear to emphatically ask: I updated the state ev=
ents to explicitly bind the session nonces on the left side of the query [2=
8]. By introducing `ClientStateEvCV2(ev, kc1, cr_c, sr_c)` and `ServerState=
EvCV2(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 woul=
d disagree with this approach.<br>
&gt; &gt;<br>
&gt; &gt; [NR] To precisely identify the root cause of the key correlation =
failure for Mechanism #3, I ran a systematic minimal cut analysis using the=
se constrained queries. By isolating each downgrade atom independently, the=
 results were definitive: When the query is conditioned *solely* on the ser=
ver&#39;s key exchange choice:<br>
&gt; &gt;<br>
&gt; &gt; ~~~<br>
&gt; &gt; `kc1 =3D kc2 || event(ServerChoosesKEX(cr_s,sr_s,DHE_13(WeakDH,ba=
dEl)))`<br>
&gt; &gt; ~~~~<br>
&gt; &gt;<br>
&gt; &gt; [NR] ProVerif evaluates the &quot;G1&quot; and &quot;G3&quot; pro=
perties as **true**. Conversely, isolating client-side KEX downgrades, hash=
 downgrades, or the `SentBadElement` event alone all evaluate to **false**.=
 [29]<br>
&gt; &gt;<br>
&gt; &gt; [NR] To explain in plain terms as I understand it: This mathemati=
cally proves there is no structural state-routing or relay flaw in the prot=
ocol design. The only way the automated solver can force the session keys t=
o diverge is by explicitly forcing the server to negotiate a weak Diffie-He=
llman 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.<br>
&gt; &gt;<br>
&gt; &gt; We would love to hear from the formal methods experts in UFMRG. W=
e also warmly welcome future collaborators moving forward. Thank you!<br>
&gt; &gt;<br>
&gt; &gt; Best regards,<br>
&gt; &gt;<br>
&gt; &gt; Usama, Slava, and Jean-Marie<br>
&gt; &gt;<br>
&gt; &gt; [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.<br>
&gt; &gt;<br>
&gt; &gt; Cheers,<br>
&gt; &gt; Nathanael<br>
&gt; &gt;<br>
&gt; &gt; [12] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S/blob/f96761deeee3b7574959eec9f44fe940b33dcbde/README.md?plain=3D1#L58" re=
l=3D"noreferrer" target=3D"_blank">https://github.com/CCC-Attestation/forma=
l-spec-KBS/blob/f96761deeee3b7574959eec9f44fe940b33dcbde/README.md?plain=3D=
1#L58</a><br>
&gt; &gt;<br>
&gt; &gt; [25] <a href=3D"https://www.researchgate.net/publication/40821918=
2_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS" rel=
=3D"noreferrer" target=3D"_blank">https://www.researchgate.net/publication/=
408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_=
TLS</a><br>
&gt; &gt;<br>
&gt; &gt; [26] <a href=3D"https://ieeexplore.ieee.org/document/7958594/" re=
l=3D"noreferrer" target=3D"_blank">https://ieeexplore.ieee.org/document/795=
8594/</a><br>
&gt; &gt;<br>
&gt; &gt; [27] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S/blob/188409b866b8fc0210c8e5d9579e441aa91ce326/binder3/tls-lib-simple.pvl#=
L582-L638" rel=3D"noreferrer" target=3D"_blank">https://github.com/CCC-Atte=
station/formal-spec-KBS/blob/188409b866b8fc0210c8e5d9579e441aa91ce326/binde=
r3/tls-lib-simple.pvl#L582-L638</a><br>
&gt; &gt;<br>
&gt; &gt; [28] <a href=3D"https://github.com/nathanaelritz/relay-attacks-in=
-attested-tls/tree/binder3-sca-demo/binder3/sca" rel=3D"noreferrer" target=
=3D"_blank">https://github.com/nathanaelritz/relay-attacks-in-attested-tls/=
tree/binder3-sca-demo/binder3/sca</a><br>
&gt; &gt;<br>
&gt; &gt; [29] <a href=3D"https://raw.githubusercontent.com/nathanaelritz/r=
elay-attacks-in-attested-tls/refs/heads/binder3-sca-demo/binder3/sca/log-bi=
nder3-sca.txt" rel=3D"noreferrer" target=3D"_blank">https://raw.githubuserc=
ontent.com/nathanaelritz/relay-attacks-in-attested-tls/refs/heads/binder3-s=
ca-demo/binder3/sca/log-binder3-sca.txt</a><br>
&gt; &gt;<br>
&gt; &gt; On Tue, 30 Jun 2026 at 14:11, Muhammad Usama Sardar &lt;<a href=
=3D"mailto:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_=
usama.sardar@tu-dresden.de</a>&gt; wrote:<br>
&gt; &gt;<br>
&gt; &gt; Hi Nathanael,<br>
&gt; &gt;<br>
&gt; &gt; Thank you for your feedback.<br>
&gt; &gt;<br>
&gt; &gt; We would like to clarify a couple of misunderstandings to avoid t=
alking past each other:<br>
&gt; &gt;<br>
&gt; &gt; - What you are proposing adding as conditions actually seems to t=
ranslate to the assumption &#39;there exists no connection in the world tha=
t ever uses weak hashes, weak DH or bad element.&#39; So your proposed prop=
erty 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 secu=
re, then my connection is secure too; so could you clarify the point of you=
r proposed property?<br>
&gt; &gt;<br>
&gt; &gt; - We believe you can agree that achieving a property without addi=
tional assumptions is stronger than achieving a property with the additiona=
l assumptions that every connection in the world is secure. It&#39;s as sim=
ple as that.<br>
&gt; &gt;<br>
&gt; &gt; Because of above reasons, we disagree with you.<br>
&gt; &gt;<br>
&gt; &gt; In any case, Sec. 6.1 in the paper [25] is clear on the threat mo=
del, and for TLS, it is typical to consider weak hashes, weak DH, or bad el=
ement (e.g., as Sec. 6.1 clearly cites Bhargavan et al.&#39;s foundational =
paper for TLS 1.3 [26]).<br>
&gt; &gt;<br>
&gt; &gt; Also, please note that in ProVerif, variables that appear only af=
ter the arrow (=3D=3D&gt;) are existentially quantified.<br>
&gt; &gt;<br>
&gt; &gt; Hope that helps.<br>
&gt; &gt;<br>
&gt; &gt; On 28.06.26 22:32, Nathanael Ritz wrote:<br>
&gt; &gt;<br>
&gt; &gt; ## Regarding correlation goals (G3 =3D&gt; G2 =3D&gt; G1)<br>
&gt; &gt;<br>
&gt; &gt; As presented in Sec. 6.4 in paper [0], this proof is paper-and-pe=
n based, and not ProVerif based. Please clarify your concern precisely. Tha=
nk you!<br>
&gt; &gt;<br>
&gt; &gt; However, the models reveal that if a mechanism achieves &quot;Lev=
el 1&quot; (G1) binding or higher (as seen in mechanisms #3, 5, 7, and the =
proposal), correlation to &quot;Level 2&quot; (G2) and &quot;Level 3&quot; =
(G3) naturally follows under the standard cryptographic assumptions of TLS =
1.3.Please see #1 and #2 above.<br>
&gt; &gt;<br>
&gt; &gt; ## Minimal demonstration under standard cryptographic assumptions=
<br>
&gt; &gt;<br>
&gt; &gt; In the current models, the G2 and G3 queries return false. Howeve=
r, when queries are conditioned to exclude the model&#39;s own weak-cryptog=
raphy events, they return true.<br>
&gt; &gt; Please see #1 and #2 above.<br>
&gt; &gt;<br>
&gt; &gt; We welcome any constructive technical feedback.<br>
&gt; &gt;<br>
&gt; &gt; We would love to hear from the formal methods experts in UFMRG. W=
e also warmly welcome future collaborators moving forward. Thank you!<br>
&gt; &gt;<br>
&gt; &gt; Best regards,<br>
&gt; &gt;<br>
&gt; &gt; Usama, Slava, and Jean-Marie<br>
&gt; &gt;<br>
&gt; &gt; [25] <a href=3D"https://www.researchgate.net/publication/40821918=
2_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS" rel=
=3D"noreferrer" target=3D"_blank">https://www.researchgate.net/publication/=
408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_=
TLS</a><br>
&gt; &gt;<br>
&gt; &gt; [26] <a href=3D"https://ieeexplore.ieee.org/document/7958594/" re=
l=3D"noreferrer" target=3D"_blank">https://ieeexplore.ieee.org/document/795=
8594/</a><br>
&gt; &gt;<br>
&gt; &gt; -----------------------------------------------<br>
&gt; &gt;<br>
&gt; &gt; From: Nathanael Ritz &lt;<a href=3D"mailto:nathanritz@gmail.com" =
target=3D"_blank">nathanritz@gmail.com</a>&gt;<br>
&gt; &gt; Date: Sun, 28 Jun 2026 at 14:32<br>
&gt; &gt; Subject: Re: [Seat] Comments on formal analysis of relay attacks =
in attested TLS (CVE-2026-33697)<br>
&gt; &gt; To: Songbo Bu &lt;<a href=3D"mailto:bluedognull@gmail.com" target=
=3D"_blank">bluedognull@gmail.com</a>&gt;<br>
&gt; &gt; Cc: &lt;<a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@i=
etf.org</a>&gt;, &lt;<a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">uf=
mrg@irtf.org</a>&gt;, Muhammad Usama Sardar &lt;<a href=3D"mailto:muhammad_=
usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_usama.sardar@tu-dres=
den.de</a>&gt;<br>
&gt; &gt;<br>
&gt; &gt; Hi Songbo, all,<br>
&gt; &gt;<br>
&gt; &gt; On Sat, 27 Jun 2026 at 21:28, Songbo Bu wrote:<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; Hi Nathanael, all,<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; Thank you for the detailed clarification.<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; I wanted to ask one focused question about the hybrid intra-=
/post-handshake direction. Since the active proposals under discussion comb=
ine intra-handshake and post-handshake attestation components, what concret=
e security property is achieved by the hybrid design that cannot be achieve=
d by a simpler post-handshake attestation design under the confidential com=
puting adversary model?<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; I am asking narrowly because this seems central to evaluatin=
g whether the added TLS transcript and state-machine complexity is justifie=
d. If the answer depends on a specific compromise setting, such as AK compr=
omise, TIK/LTK compromise, split deployment, or verifier-oracle behavior, i=
t would be helpful to identify the corresponding property or query explicit=
ly.<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; Best,<br>
&gt; &gt; &gt; Songbo<br>
&gt; &gt; &gt;<br>
&gt; &gt;<br>
&gt; &gt; I appreciate the focused question, although I believe it may dist=
ract from the topic at hand. However, I am happy to briefly touch on that t=
opic here: before we can fully evaluate the two, we face a benchmarking cha=
llenge. The formal analysis of the post-handshake attestation is currently =
a &quot;work-in-progress,&quot; as noted in the Appendix of `draft-fossati-=
seat-expat-02` [23].<br>
&gt; &gt;<br>
&gt; &gt; For example, a unique design for post-handshake attestation prese=
nted by Usama to the CFRG introduces multiple exported authenticators (`EKM=
_RD`, `EKM_HC`, and `EKM_FK`) [24]. This approach appears to represent a ma=
terial shift from the single-exporter design specified in Section 5.1 of th=
e `draft-fossati-seat-expat-02` draft. Perhaps you may agree, then, that un=
til the benchmark formal model for `draft-fossati-seat-expat` is published,=
 it is difficult to explicitly identify a comparative property that we migh=
t all find satisfactory.<br>
&gt; &gt;<br>
&gt; &gt; I believe that the discussion evaluating the architectural merits=
 between pure intra-, post-, or hybrid compositions is an important one, bu=
t different from the technical evaluation of the formal model discussed her=
e. 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 a=
nd distinct from one another. I would be happy to continue discussing the t=
opic in more detail with you there, and feel free to reference this thread =
if you do go ahead.<br>
&gt; &gt;<br>
&gt; &gt; ---<br>
&gt; &gt;<br>
&gt; &gt; ## Regarding correlation goals (G3 =3D&gt; G2 =3D&gt; G1)<br>
&gt; &gt;<br>
&gt; &gt; On that note, I would like to bring the WG&#39;s focus back to th=
e technical discussion regarding the ProVerif models at hand. Specifically,=
 I want to address the &quot;Main Results&quot; and their claimed implicati=
ons [12], which I have previously contested.<br>
&gt; &gt;<br>
&gt; &gt; I have repeated before, and will clarify again, that the flaws re=
sponsibly disclosed in CVE-2026-33697 are not under dispute by me. Furtherm=
ore, I believe that the analysis helps us understand that based on these mo=
dels, it is not possible to achieve even &quot;Level 1&quot; (G1) binding (=
to use the author&#39;s taxonomy) without some kind of session material tha=
t can help bind the Evidence and Attestation Results to the TLS connection.=
<br>
&gt; &gt;<br>
&gt; &gt; However, the models reveal that if a mechanism achieves &quot;Lev=
el 1&quot; (G1) binding or higher (as seen in mechanisms #3, 5, 7, and the =
proposal), correlation to &quot;Level 2&quot; (G2) and &quot;Level 3&quot; =
(G3) naturally follows under the standard cryptographic assumptions of TLS =
1.3.<br>
&gt; &gt;<br>
&gt; &gt; ## Minimal demonstration under standard cryptographic assumptions=
<br>
&gt; &gt;<br>
&gt; &gt; In the current models, the G2 and G3 queries return false. Howeve=
r, when queries are conditioned to exclude the model&#39;s own weak-cryptog=
raphy events, they return true. For example, the model demonstrating Binder=
 3 (Early exporter `exp0`) shows binding to both G2 and G3 binding under st=
andard assumptions. E.g.:<br>
&gt; &gt;<br>
&gt; &gt; **Baseline query (returns false):**<br>
&gt; &gt;<br>
&gt; &gt; ~~~ocaml<br>
&gt; &gt; query ev:bitstring, kc1:ae_key, kc2:ae_key;<br>
&gt; &gt; event(ClientStateEvKc(ev,kc1)) &amp;&amp;<br>
&gt; &gt; event(ServerStateEvKc(ev,kc2)) =3D=3D&gt; (kc1 =3D kc2).<br>
&gt; &gt; ~~~<br>
&gt; &gt;<br>
&gt; &gt; **Conditioned query under strong crypto (returns true):**<br>
&gt; &gt;<br>
&gt; &gt; ~~~ocaml<br>
&gt; &gt; query ev:bitstring, kc1:ae_key, kc2:ae_key,<br>
&gt; &gt; cr:random, sr:random, cr&#39;:random, sr&#39;:random, e:element;<=
br>
&gt; &gt; event(ClientStateEvKc(ev,kc1)) &amp;&amp;<br>
&gt; &gt; event(ServerStateEvKc(ev,kc2)) =3D=3D&gt; (kc1 =3D kc2) ||<br>
&gt; &gt; event(ServerChoosesKEX(cr,sr,DHE_13(WeakDH,e))) ||<br>
&gt; &gt; event(ServerChoosesHash(cr&#39;,sr&#39;,WeakHash)) ||<br>
&gt; &gt; event(SentBadElement).<br>
&gt; &gt; ~~~<br>
&gt; &gt;<br>
&gt; &gt; It appears that the result generalizes: any mechanism achieving G=
1 demonstrates the ability to achieve G3 under standard assumptions. That i=
s, by excluding weak DH groups, weak hash algorithms, or a bad group elemen=
t -- all of which are already prohibited in compliant TLS 1.3 implementatio=
ns per RFC 8446(bis), each demonstrates full G3 binding properties, based o=
n the authors&#39; formal models. In contrast, attempting the same against =
Binder2 did not achieve G3, G2 or even G1 binding even with standard crypto=
graphic assumptions.<br>
&gt; &gt;<br>
&gt; &gt; Therefore, I believe this is further indication that the broad cl=
aims repeatedly made against those active drafts lack sufficient technical =
evidence based on the current models to sustain them. Of course, authors ar=
e implicitly and explicitly welcome to follow up with a substantive respons=
e rooted in the technical merits of their presented work.<br>
&gt; &gt;<br>
&gt; &gt; ---<br>
&gt; &gt;<br>
&gt; &gt; Songbo, given your focus on evaluating the added complexity versu=
s security benefits, would you be willing to initiate the new thread on the=
 architectural comparison? I look forward to diving into that discussion wi=
th you.<br>
&gt; &gt;<br>
&gt; &gt; Respectfully,<br>
&gt; &gt; Nathanael Ritz<br>
&gt; &gt;<br>
&gt; &gt; [23] <a href=3D"https://datatracker.ietf.org/meeting/125/material=
s/slides-125-cfrg-relay-attacks-00" rel=3D"noreferrer" target=3D"_blank">ht=
tps://datatracker.ietf.org/meeting/125/materials/slides-125-cfrg-relay-atta=
cks-00</a> - slide 15/18<br>
&gt; &gt;<br>
&gt; &gt; [24] <a href=3D"https://www.ietf.org/archive/id/draft-fossati-sea=
t-expat-02.html#name-post-handshake-vs-intra-hand" rel=3D"noreferrer" targe=
t=3D"_blank">https://www.ietf.org/archive/id/draft-fossati-seat-expat-02.ht=
ml#name-post-handshake-vs-intra-hand</a><br>
&gt; &gt;<br>
&gt; &gt; -----------------------------------------------<br>
&gt; &gt;<br>
&gt; &gt; From: Nathanael Ritz &lt;<a href=3D"mailto:nathanritz@gmail.com" =
target=3D"_blank">nathanritz@gmail.com</a>&gt;<br>
&gt; &gt; Date: Sat, 27 Jun 2026 at 13:18<br>
&gt; &gt; Subject: Re: [Seat] Comments on formal analysis of relay attacks =
in attested TLS (CVE-2026-33697)<br>
&gt; &gt; To: <a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.=
org</a> &lt;<a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.or=
g</a>&gt;<br>
&gt; &gt; Cc: &lt;<a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">ufmrg=
@irtf.org</a>&gt;, Songbo Bu &lt;<a href=3D"mailto:bluedognull@gmail.com" t=
arget=3D"_blank">bluedognull@gmail.com</a>&gt;, Muhammad Usama Sardar &lt;<=
a href=3D"mailto:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muh=
ammad_usama.sardar@tu-dresden.de</a>&gt;<br>
&gt; &gt;<br>
&gt; &gt; Hi Songbo, Usama, all<br>
&gt; &gt;<br>
&gt; &gt; I have additional comments to share regarding the recent formal a=
nalysis put foward by Sardar et al., which evaluates relay attacks in attes=
ted TLS such as CVE-2026-33697, as well some of the proposed mitigations.<b=
r>
&gt; &gt;<br>
&gt; &gt; Comments are offered below with [NR]:<br>
&gt; &gt;<br>
&gt; &gt; On Sat, 27 Jun 2026 at 09:02, Songbo Bu &lt;<a href=3D"mailto:blu=
edognull@gmail.com" target=3D"_blank">bluedognull@gmail.com</a>&gt; wrote:<=
br>
&gt; &gt;<br>
&gt; &gt; Hi all,<br>
&gt; &gt;<br>
&gt; &gt; I would like to add an independent reproducibility data point for=
 the public artifact.<br>
&gt; &gt;<br>
&gt; &gt; [...]<br>
&gt; &gt;<br>
&gt; &gt; The artifact provides a reproducible and formal way to compare di=
fferent authentication-binding strengths in TLS.<br>
&gt; &gt;<br>
&gt; &gt; [NR] I can confirm that the artifacts presented are reproducible =
and align with the inline commentary included in the ProVerif source.<br>
&gt; &gt;<br>
&gt; &gt; [NR] That being said, it&#39;s worth noting that the authors of t=
he models have made efforts to clarify [13] that their analysis cannot prov=
ide 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`).<br>
&gt; &gt;<br>
&gt; &gt; [NR] This makes the models put presented by Usama and collaborato=
rs fundamentally incompatible with those drafts, meaning they cannot provid=
e concrete counter-examples to any of the security claims or properties men=
tioned in the individual I-Ds from either draft-fossati-seat-early-attestat=
ion-04 or draft-ritz-seat-facts-00. This is a meaningful limitation of the =
formal analysis within the intra-handshake attestation design space.<br>
&gt; &gt;<br>
&gt; &gt; This is useful for the SEAT discussion because it distinguishes b=
inding evidence to early/DH-derived state, handshake traffic-key state, and=
 application traffic-key state under the confidential computing adversary m=
odel.<br>
&gt; &gt;<br>
&gt; &gt; [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 o=
f possible designs that have also been formally proven to be insecure. Ther=
efore, as I mentioned previously, I **strongly advise** against introducing=
 concrete designs or specifications in any active Internet-Draft that refle=
cts any of the binders proposed by Sardar et al. in their most recent work.=
<br>
&gt; &gt;<br>
&gt; &gt; I also think the artifact is valuable input for evaluating whethe=
r intra-handshake attestation adds security benefit commensurate with its p=
rotocol complexity. Extra code paths, transcript interactions, and TLS stat=
e-machine changes increase implementation and review burden. Before absorbi=
ng that complexity into protocol design, it seems useful to make explicit w=
hich security property an intra-handshake component achieves, and whether t=
hat property cannot be achieved by a simpler post-handshake design.<br>
&gt; &gt;<br>
&gt; &gt; [NR] I agree completely. For example, I understand that much of t=
he concrete specification I proposed in my own individual I-D, draft-ritz-s=
eat-facts-00 is more complex than necessary compared to draft-fossati-seat-=
early-attestation-03 released the same day. This complexity is even more ap=
parent when compared to the changes published in their recent -04 revision.=
<br>
&gt; &gt;<br>
&gt; &gt; [NR] I am hopeful that such evaluations on concrete proposals bas=
ed on **active** Internet-Drafts under discussion with the SEAT WG will con=
tinue, especially if the WG has concensus towards formal adoption of draft-=
mihalcea-seat-use-cases.<br>
&gt; &gt;<br>
&gt; &gt; If a proposed construction is believed to bind attestation state =
to TLS in a way that differs from the current artifact, a minimal model cha=
nge or PR would make the comparison easier to evaluate.<br>
&gt; &gt;<br>
&gt; &gt; [NR] Agreed. However, I&#39;m not convinced a minimal model chang=
e is possible given the fundamental incompatibility between how the current=
 models under discussion are constructed and the specifications and securit=
y considerations outlined in the active drafts discussed with the SEAT WG. =
For those curious, I outlined the necessary model changes that might be nec=
essary in order to properly evaluate draft-fossati-seat-early-attestation-0=
3 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 bo=
th [19] and [20].<br>
&gt; &gt;<br>
&gt; &gt; On Fri, 26 Jun 2026 at 05:41, Muhammad Usama Sardar &lt;<a href=
=3D"mailto:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_=
usama.sardar@tu-dresden.de</a>&gt; wrote:<br>
&gt; &gt;<br>
&gt; &gt; Hi Nathanael,<br>
&gt; &gt;<br>
&gt; &gt; [...]<br>
&gt; &gt;<br>
&gt; &gt; I respectfully request that the authors update their ProVerif art=
ifacts to accurately reflect the actual binder derivations (such as the `HK=
DF-Expand-Label` derivation in Section 5.1.1) and the standard `Certificate=
Verify` boundaries established by the WG&#39;s drafts if they have not alre=
ady done so, and present that work here.<br>
&gt; &gt;<br>
&gt; &gt; There are no WG&#39;s drafts in SEAT as of today. All are individ=
ual I-Ds.<br>
&gt; &gt;<br>
&gt; &gt; [NR] Thanks for clarifying that important detail. The request res=
pectfully still stands for the individual I-Ds I suggested earlier.<br>
&gt; &gt;<br>
&gt; &gt; Finally and to that end, I suggest this working group focus its f=
uture energy on carefully considering the merits of active indivual I-Ds su=
ch 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).<b=
r>
&gt; &gt;<br>
&gt; &gt; We disagree with your assessment of draft-fossati-seat-early-atte=
station. We believe the design in draft-fossati-seat-early-attestation is v=
ulnerable to CVE.<br>
&gt; &gt;<br>
&gt; &gt; [NR] Once again, the claim that active individual I-Ds such as dr=
aft-fossati-seat-early-attestation are potentially vulnerable to CVE-2026-3=
3697 continues to persist without clear demonstrable evidence. The claim ap=
pears to be framed as informed intuition [21], but I don&#39;t think the mo=
dels=E2=80=99 applicability to inform such intuition has been backed by the=
ir technical merits. As mentioned earlier, I identified two constructive el=
ements causing the models to strictly fall out of alignment with the drafts=
&#39; specifications, and the authors have not disputed this misalignment.<=
br>
&gt; &gt;<br>
&gt; &gt; [NR] I believe that repeated claims of attacks on active drafts u=
nder discussion within any WG ought to be supported by published evidence o=
r concrete testable arguments, as I largely suggested the same on-list a fe=
w months back [22].<br>
&gt; &gt;<br>
&gt; &gt; Cheers,<br>
&gt; &gt;<br>
&gt; &gt; Nathanael<br>
&gt; &gt;<br>
&gt; &gt; [9] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KBS=
" rel=3D"noreferrer" target=3D"_blank">https://github.com/CCC-Attestation/f=
ormal-spec-KBS</a><br>
&gt; &gt;<br>
&gt; &gt; [10] <a href=3D"https://mailarchive.ietf.org/arch/msg/tls/amNYPs3=
eV3a-l5bFQtUDGx4fU24/" rel=3D"noreferrer" target=3D"_blank">https://mailarc=
hive.ietf.org/arch/msg/tls/amNYPs3eV3a-l5bFQtUDGx4fU24/</a><br>
&gt; &gt;<br>
&gt; &gt; [11] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S/tree/f96761deeee3b7574959eec9f44fe940b33dcbde" rel=3D"noreferrer" target=
=3D"_blank">https://github.com/CCC-Attestation/formal-spec-KBS/tree/f96761d=
eeee3b7574959eec9f44fe940b33dcbde</a><br>
&gt; &gt;<br>
&gt; &gt; [12] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S/blob/f96761deeee3b7574959eec9f44fe940b33dcbde/README.md?plain=3D1#L58" re=
l=3D"noreferrer" target=3D"_blank">https://github.com/CCC-Attestation/forma=
l-spec-KBS/blob/f96761deeee3b7574959eec9f44fe940b33dcbde/README.md?plain=3D=
1#L58</a><br>
&gt; &gt;<br>
&gt; &gt; [13] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S#modeling" rel=3D"noreferrer" target=3D"_blank">https://github.com/CCC-Att=
estation/formal-spec-KBS#modeling</a><br>
&gt; &gt;<br>
&gt; &gt; [14] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S#acknowledgments" rel=3D"noreferrer" target=3D"_blank">https://github.com/=
CCC-Attestation/formal-spec-KBS#acknowledgments</a><br>
&gt; &gt;<br>
&gt; &gt; [15] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S#pre-print" rel=3D"noreferrer" target=3D"_blank">https://github.com/CCC-At=
testation/formal-spec-KBS#pre-print</a><br>
&gt; &gt;<br>
&gt; &gt; [16] <a href=3D"https://mailarchive.ietf.org/arch/msg/seat/2HfF4J=
jZbJhw-HJo1GbVTkUmeVU/" rel=3D"noreferrer" target=3D"_blank">https://mailar=
chive.ietf.org/arch/msg/seat/2HfF4JjZbJhw-HJo1GbVTkUmeVU/</a><br>
&gt; &gt;<br>
&gt; &gt; [17] <a href=3D"https://datatracker.ietf.org/doc/draft-fossati-tl=
s-attestation/" rel=3D"noreferrer" target=3D"_blank">https://datatracker.ie=
tf.org/doc/draft-fossati-tls-attestation/</a><br>
&gt; &gt;<br>
&gt; &gt; [18] <a href=3D"https://mailarchive.ietf.org/arch/msg/seat/U-0qtL=
paFqQ7MDq-ArRflnEe-rE/" rel=3D"noreferrer" target=3D"_blank">https://mailar=
chive.ietf.org/arch/msg/seat/U-0qtLpaFqQ7MDq-ArRflnEe-rE/</a><br>
&gt; &gt;<br>
&gt; &gt; [19] <a href=3D"https://mailarchive.ietf.org/arch/msg/seat/-_ljx0=
7LGlxvVtNaKQfKKcUEuhw/" rel=3D"noreferrer" target=3D"_blank">https://mailar=
chive.ietf.org/arch/msg/seat/-_ljx07LGlxvVtNaKQfKKcUEuhw/</a><br>
&gt; &gt;<br>
&gt; &gt; [20] <a href=3D"https://mailarchive.ietf.org/arch/msg/seat/bdLxj7=
cMeRaSgtppKek8uVXHSjA/" rel=3D"noreferrer" target=3D"_blank">https://mailar=
chive.ietf.org/arch/msg/seat/bdLxj7cMeRaSgtppKek8uVXHSjA/</a><br>
&gt; &gt;<br>
&gt; &gt; [21] <a href=3D"https://mailarchive.ietf.org/arch/msg/seat/6P_1jR=
-fylM9WCOGGTgaVEQ0Khc/" rel=3D"noreferrer" target=3D"_blank">https://mailar=
chive.ietf.org/arch/msg/seat/6P_1jR-fylM9WCOGGTgaVEQ0Khc/</a><br>
&gt; &gt;<br>
&gt; &gt; [22] <a href=3D"https://mailarchive.ietf.org/arch/msg/seat/J3-2iv=
C7smo2qNpK6SMP-rKKAjU/" rel=3D"noreferrer" target=3D"_blank">https://mailar=
chive.ietf.org/arch/msg/seat/J3-2ivC7smo2qNpK6SMP-rKKAjU/</a><br>
&gt; &gt;<br>
&gt; &gt; -----------------------------------------------<br>
&gt; &gt;<br>
&gt; &gt; From: Songbo Bu &lt;<a href=3D"mailto:bluedognull@gmail.com" targ=
et=3D"_blank">bluedognull@gmail.com</a>&gt;<br>
&gt; &gt; Date: Sat, 27 Jun 2026 at 09:02<br>
&gt; &gt; Subject: [Seat] Re: Comments on formal analysis of relay attacks =
in attested TLS<br>
&gt; &gt; To: &lt;<a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@i=
etf.org</a>&gt;, &lt;<a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">uf=
mrg@irtf.org</a>&gt;, Muhammad Usama Sardar &lt;<a href=3D"mailto:muhammad_=
usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_usama.sardar@tu-dres=
den.de</a>&gt;<br>
&gt; &gt;<br>
&gt; &gt; Hi all,<br>
&gt; &gt;<br>
&gt; &gt; I would like to add an independent reproducibility data point for=
 the public artifact.<br>
&gt; &gt;<br>
&gt; &gt; I ran the formal-spec-KBS ProVerif artifact at commit:<br>
&gt; &gt;<br>
&gt; &gt; f96761deeee3b7574959eec9f44fe940b33dcbde<br>
&gt; &gt;<br>
&gt; &gt; Environment:<br>
&gt; &gt;<br>
&gt; &gt; ProVerif 2.05<br>
&gt; &gt; OPAM switch: default<br>
&gt; &gt; OCaml 5.5.0<br>
&gt; &gt; Command used in each model directory:<br>
&gt; &gt; proverif -lib tls-lib-simple.pvl tls13-multiagent.pv<br>
&gt; &gt;<br>
&gt; &gt; I ran all seven candidate binding mechanisms, binder1 through bin=
der7, and the proposed mechanism, proposal. All eight runs completed succes=
sfully. I also extracted the Verification summary from each run and compare=
d it against the log.txt files in the repository; the summaries matched exa=
ctly in all eight cases.<br>
&gt; &gt;<br>
&gt; &gt; For the three correlation goals, my reproduced results are:<br>
&gt; &gt;<br>
&gt; &gt; Mechanism | G1: evidence to DH shared secret | G2: evidence to cl=
ient handshake traffic key | G3: evidence to client application traffic key=
<br>
&gt; &gt; binder1 | false | false | false<br>
&gt; &gt; binder2 | false | false | false<br>
&gt; &gt; binder3 | true | false | false<br>
&gt; &gt; binder4 | false | false | false<br>
&gt; &gt; binder5 | true | false | false<br>
&gt; &gt; binder6 | false | false | false<br>
&gt; &gt; binder7 | true | false | false<br>
&gt; &gt; proposal | true | true | false<br>
&gt; &gt;<br>
&gt; &gt; The artifact provides a reproducible and formal way to compare di=
fferent authentication-binding strengths in TLS. This is useful for the SEA=
T 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.<br>
&gt; &gt;<br>
&gt; &gt; I also think the artifact is valuable input for evaluating whethe=
r intra-handshake attestation adds security benefit commensurate with its p=
rotocol complexity. Extra code paths, transcript interactions, and TLS stat=
e-machine changes increase implementation and review burden. Before absorbi=
ng that complexity into protocol design, it seems useful to make explicit w=
hich security property an intra-handshake component achieves, and whether t=
hat property cannot be achieved by a simpler post-handshake design.<br>
&gt; &gt;<br>
&gt; &gt; If a proposed construction is believed to bind attestation state =
to TLS in a way that differs from the current artifact, a minimal model cha=
nge or PR would make the comparison easier to evaluate.<br>
&gt; &gt;<br>
&gt; &gt; I am continuing to investigate implementation evidence and can up=
date later if I obtain additional reproducible results.<br>
&gt; &gt;<br>
&gt; &gt; Best,<br>
&gt; &gt; Songbo<br>
&gt; &gt;<br>
&gt; &gt; _______________________________________________<br>
&gt; &gt; Seat mailing list -- <a href=3D"mailto:seat@ietf.org" target=3D"_=
blank">seat@ietf.org</a><br>
&gt; &gt; To unsubscribe send an email to <a href=3D"mailto:seat-leave@ietf=
.org" target=3D"_blank">seat-leave@ietf.org</a><br>
&gt; &gt;<br>
&gt; &gt; -----------------------------------------------<br>
&gt; &gt;<br>
&gt; &gt; From: Muhammad Usama Sardar &lt;<a href=3D"mailto:muhammad_usama.=
sardar@tu-dresden.de" target=3D"_blank">muhammad_usama.sardar@tu-dresden.de=
</a>&gt;<br>
&gt; &gt; Date: Fri, 26 Jun 2026 at 05:41<br>
&gt; &gt; Subject: Re: [Seat] Comments on formal analysis of relay attacks =
in attested TLS (CVE-2026-33697)<br>
&gt; &gt; To: Nathanael Ritz &lt;<a href=3D"mailto:nathanritz@gmail.com" ta=
rget=3D"_blank">nathanritz@gmail.com</a>&gt;, <a href=3D"mailto:seat@ietf.o=
rg" target=3D"_blank">seat@ietf.org</a> &lt;<a href=3D"mailto:seat@ietf.org=
" target=3D"_blank">seat@ietf.org</a>&gt;<br>
&gt; &gt; Cc: &lt;<a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">ufmrg=
@irtf.org</a>&gt;<br>
&gt; &gt;<br>
&gt; &gt; Hi Nathanael,<br>
&gt; &gt;<br>
&gt; &gt; Thank you for your detailed comments. First, we updated the subje=
ct, which was mistakenly mentioning an irrelevant CVE instead of the one we=
 discovered.<br>
&gt; &gt;<br>
&gt; &gt; The key point is that as already discussed (e.g., [16]), we belie=
ve draft-fossati-seat-early-attestation itself contradicts SEAT charter, an=
d hence any reasonable formal analysis related to this draft will do so.<br=
>
&gt; &gt;<br>
&gt; &gt; Moreover, we would like to clarify the following and welcome cons=
tructive feedback as a minimal PR:<br>
&gt; &gt;<br>
&gt; &gt; On 26.06.26 09:08, Nathanael Ritz wrote:<br>
&gt; &gt;<br>
&gt; &gt; ## A. Every demonstrated model uses a non-standard dual `Certific=
ateVerify` construction (`CV_Ext`), in contradiction to the SEAT WG charter=
<br>
&gt; &gt;<br>
&gt; &gt; We believe the model section [13] is sufficiently clear on this b=
ut 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 vers=
ion of diversion attacks as the baseline, rather than showing the same old =
attacks from ID-Crisis paper, and the discovered CVE (CVE-2026-33697) -- wh=
ich the previous analysis could not find -- practically demonstrates that. =
This modeling choice makes it clear that even with the diversion attacks fi=
xed, high-severity relay attacks would still remain in intra-handshake atte=
station.<br>
&gt; &gt;<br>
&gt; &gt; The pre-print (which will be added soon [15]) makes this clear as=
 well.<br>
&gt; &gt;<br>
&gt; &gt; This is also reflected in acknowledgments, where folks who contri=
buted to the previous formal modeling effort are acknowledged with an expli=
cit split [14]. (Thank you all once again)<br>
&gt; &gt;<br>
&gt; &gt; Therefore, I propose that if Usama and collaborators are serious =
about exploring a dual-signature variation of CertificateVerify as a genuin=
e solution for composing remote attestation with TLS, they perhaps consider=
 continued collaboration with the authors of `draft-yusef-tls-pqt-dual-cert=
s` [10], or with others in the TLS WG, to bring forward their case for nove=
l modifications to the TLS state machine. Otherwise, just as the authors of=
 `draft-fossati-seat-early-attestation` did when moving from revision -02 t=
o -03, I suggest that Sardar et al. consider bringing forward novel proposa=
ls or formal analysis for intra-handshake attestation that conform to the S=
EAT charter.<br>
&gt; &gt;<br>
&gt; &gt; Thanks. We will share the analysis with the TLS WG as well and as=
 already clarified, draft-fossati-seat-early-attestation is technically a h=
ybrid with a combination of intra- and post-handshake attestation and our f=
ormal analysis contribution to the WG questions the claim on the need for i=
ntra-handshake attestation in this combination.<br>
&gt; &gt;<br>
&gt; &gt; ## B. The CA-backed key (`pubLTK`) is never bound into the attest=
ation evidence (`rdata`)<br>
&gt; &gt;<br>
&gt; &gt; Sure, things are a bit more subtle. There are several open questi=
ons here based on confidential computing (CC) threat model on how to do tha=
t with the cloud provider out of TCB and we welcome your thoughts on those:=
<br>
&gt; &gt;<br>
&gt; &gt; - What is the &quot;long-term identity&quot; of the CC workload? =
How is &quot;long-term identity&quot; assigned to the CC workload? Which en=
tity supplies this &quot;long-term identity&quot;? How is that Identity Sup=
plier trusted?<br>
&gt; &gt;<br>
&gt; &gt; - How is CA-certified Long-Term Key (LTK) injected in the Confide=
ntial Computing workload in the first place?<br>
&gt; &gt;<br>
&gt; &gt; In every single model (`binder1` through `binder7`, `aggregate`, =
and `proposal`), the `rdata` value=E2=80=94which is what the Attestation Ke=
y (`privAK`) actually signs to generate the evidence=E2=80=94is restricted =
to nonces, session-derived values, and the uncertified ephemeral key (`pubE=
K`).<br>
&gt; &gt;<br>
&gt; &gt; That&#39;s how we understand the four analyzed real-world practic=
al implementations are doing it<br>
&gt; &gt;<br>
&gt; &gt; - Meta&#39;s AI<br>
&gt; &gt;<br>
&gt; &gt; - Cocos AI<br>
&gt; &gt;<br>
&gt; &gt; - Edgeless Systems<br>
&gt; &gt;<br>
&gt; &gt; - CCC proof-of-concept<br>
&gt; &gt;<br>
&gt; &gt; and they have acknowledged it.<br>
&gt; &gt;<br>
&gt; &gt; If your understanding of any of the analyzed implementations is d=
ifferent, we would appreciate a minimal possible PR for the respective bind=
ing mechanism that we will be happy to concretely discuss.<br>
&gt; &gt;<br>
&gt; &gt; ## Other remarks<br>
&gt; &gt;<br>
&gt; &gt; 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 &quo=
t;suggest that more recent proposals draft-fossati-seat-early-attestation a=
nd draft-ritz-seat-facts add unnecessary complexity of intra-handshake atte=
station without adding any security benefit&quot;. [12]<br>
&gt; &gt;<br>
&gt; &gt; One aspect missing here is that both mentioned drafts are hybrids=
 (combination of intra- and post-handshake attestation). Could you please i=
dentify a concrete security property which is achieved by the combination o=
f intra- and post-handshake attestation but not by simple post-handshake at=
testation?<br>
&gt; &gt;<br>
&gt; &gt; I respectfully request that the authors update their ProVerif art=
ifacts to accurately reflect the actual binder derivations (such as the `HK=
DF-Expand-Label` derivation in Section 5.1.1) and the standard `Certificate=
Verify` boundaries established by the WG&#39;s drafts if they have not alre=
ady done so, and present that work here.<br>
&gt; &gt;<br>
&gt; &gt; There are no WG&#39;s drafts in SEAT as of today. All are individ=
ual I-Ds.<br>
&gt; &gt;<br>
&gt; &gt; Finally and to that end, I suggest this working group focus its f=
uture energy on carefully considering the merits of active indivual I-Ds su=
ch 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).<b=
r>
&gt; &gt;<br>
&gt; &gt; We disagree with your assessment of draft-fossati-seat-early-atte=
station. We believe the design in draft-fossati-seat-early-attestation is v=
ulnerable to CVE.<br>
&gt; &gt;<br>
&gt; &gt; Even if you disagree with it, additional code is additional compl=
exity and thus additional attack surface. We would like to see much stronge=
r arguments than have been presented to date before we absorb this complexi=
ty.<br>
&gt; &gt;<br>
&gt; &gt; Best regards,<br>
&gt; &gt;<br>
&gt; &gt; Usama, Slava, and Jean-Marie<br>
&gt; &gt;<br>
&gt; &gt; [9] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KBS=
" rel=3D"noreferrer" target=3D"_blank">https://github.com/CCC-Attestation/f=
ormal-spec-KBS</a><br>
&gt; &gt;<br>
&gt; &gt; [10] <a href=3D"https://mailarchive.ietf.org/arch/msg/tls/amNYPs3=
eV3a-l5bFQtUDGx4fU24/" rel=3D"noreferrer" target=3D"_blank">https://mailarc=
hive.ietf.org/arch/msg/tls/amNYPs3eV3a-l5bFQtUDGx4fU24/</a><br>
&gt; &gt;<br>
&gt; &gt; [11] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S/tree/f96761deeee3b7574959eec9f44fe940b33dcbde" rel=3D"noreferrer" target=
=3D"_blank">https://github.com/CCC-Attestation/formal-spec-KBS/tree/f96761d=
eeee3b7574959eec9f44fe940b33dcbde</a><br>
&gt; &gt;<br>
&gt; &gt; [12] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S/blob/f96761deeee3b7574959eec9f44fe940b33dcbde/README.md?plain=3D1#L58" re=
l=3D"noreferrer" target=3D"_blank">https://github.com/CCC-Attestation/forma=
l-spec-KBS/blob/f96761deeee3b7574959eec9f44fe940b33dcbde/README.md?plain=3D=
1#L58</a><br>
&gt; &gt;<br>
&gt; &gt; [13] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S#modeling" rel=3D"noreferrer" target=3D"_blank">https://github.com/CCC-Att=
estation/formal-spec-KBS#modeling</a><br>
&gt; &gt;<br>
&gt; &gt; [14] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S#acknowledgments" rel=3D"noreferrer" target=3D"_blank">https://github.com/=
CCC-Attestation/formal-spec-KBS#acknowledgments</a><br>
&gt; &gt;<br>
&gt; &gt; [15] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S#pre-print" rel=3D"noreferrer" target=3D"_blank">https://github.com/CCC-At=
testation/formal-spec-KBS#pre-print</a><br>
&gt; &gt;<br>
&gt; &gt; [16] <a href=3D"https://mailarchive.ietf.org/arch/msg/seat/2HfF4J=
jZbJhw-HJo1GbVTkUmeVU/" rel=3D"noreferrer" target=3D"_blank">https://mailar=
chive.ietf.org/arch/msg/seat/2HfF4JjZbJhw-HJo1GbVTkUmeVU/</a><br>
&gt; &gt;<br>
&gt; &gt; -----------------------------------------------<br>
&gt; &gt;<br>
&gt; &gt; From: Nathanael Ritz &lt;<a href=3D"mailto:nathanritz@gmail.com" =
target=3D"_blank">nathanritz@gmail.com</a>&gt;<br>
&gt; &gt; Date: Fri, 26 Jun 2026 at 01:08<br>
&gt; &gt; Subject: Comments on formal analysis of relay attacks in attested=
 TLS (CVE-2026-3369)<br>
&gt; &gt; To: <a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.=
org</a> &lt;<a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.or=
g</a>&gt;<br>
&gt; &gt; Cc: &lt;<a href=3D"mailto:ufmrg@irtf.org" target=3D"_blank">ufmrg=
@irtf.org</a>&gt;<br>
&gt; &gt;<br>
&gt; &gt; Hello,<br>
&gt; &gt;<br>
&gt; &gt; Thank you to Usama and collaborators for bringing their recent wo=
rk 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 applicabi=
lity of the analysis to the current effort of this working group. My concer=
ns are organized into two main parts, A. and B., along with a few additiona=
l remarks.<br>
&gt; &gt;<br>
&gt; &gt; My comments are offered below:<br>
&gt; &gt;<br>
&gt; &gt; ## A. Every demonstrated model uses a non-standard dual `Certific=
ateVerify` construction (`CV_Ext`), in contradiction to the SEAT WG charter=
<br>
&gt; &gt;<br>
&gt; &gt; TLS 1.3 (RFC 8446bis) requires a single signature from the endpoi=
nt&#39;s identity key over the handshake transcript. However, the models ap=
ply *both* an uncertified ephemeral key (`privEK`) and a CA-backed long-ter=
m key (`privLTK`) to sign the transcript independently of each other.<br>
&gt; &gt;<br>
&gt; &gt; This is explicitly written in the `Server` process:<br>
&gt; &gt;<br>
&gt; &gt; ```ocaml<br>
&gt; &gt; let sg =3D sign(privEK ,hash(hash_algo,log_CRT)) in<br>
&gt; &gt; let sg_LTK =3D sign(privLTK,hash(hash_algo,log_CRT)) in<br>
&gt; &gt; out(io,CV_Ext(sg,sg_LTK));<br>
&gt; &gt; ```<br>
&gt; &gt;<br>
&gt; &gt; The `Client` process is then hardcoded to receive and verify this=
 dual-signature payload:<br>
&gt; &gt;<br>
&gt; &gt; ```ocaml<br>
&gt; &gt; in(io,CV_Ext(s,s_LTK));<br>
&gt; &gt; if verify(pubEK,hash(shash_algo,log_CRT),s) =3D true then<br>
&gt; &gt; if verify(pubLTK,hash(shash_algo,log_CRT),s_LTK) =3D true then<br=
>
&gt; &gt; ```<br>
&gt; &gt;<br>
&gt; &gt; In case it is not apparent, this dual-signature `CV_Ext` mechanis=
m has no basis in any IETF proposed standard.<br>
&gt; &gt;<br>
&gt; &gt; Therefore, I propose that if Usama and collaborators are serious =
about exploring a dual-signature variation of CertificateVerify as a genuin=
e solution for composing remote attestation with TLS, they perhaps consider=
 continued collaboration with the authors of `draft-yusef-tls-pqt-dual-cert=
s` [10], or with others in the TLS WG, to bring forward their case for nove=
l modifications to the TLS state machine. Otherwise, just as the authors of=
 `draft-fossati-seat-early-attestation` did when moving from revision -02 t=
o -03, I suggest that Sardar et al. consider bringing forward novel proposa=
ls or formal analysis for intra-handshake attestation that conform to the S=
EAT charter.<br>
&gt; &gt;<br>
&gt; &gt; ## B. The CA-backed key (`pubLTK`) is never bound into the attest=
ation evidence (`rdata`)<br>
&gt; &gt;<br>
&gt; &gt; In every single model (`binder1` through `binder7`, `aggregate`, =
and `proposal`), the `rdata` value=E2=80=94which is what the Attestation Ke=
y (`privAK`) actually signs to generate the evidence=E2=80=94is restricted =
to nonces, session-derived values, and the uncertified ephemeral key (`pubE=
K`).<br>
&gt; &gt;<br>
&gt; &gt; Looking at the `Server` process across the binder folders, the ex=
act definitions for `rdata` across all the evaluated mechanisms are:<br>
&gt; &gt;<br>
&gt; &gt; ```<br>
&gt; &gt; * **Binder 1:** `let rdata =3D rand2bs(cr)`<br>
&gt; &gt; (Client&#39;s TLS nonce)<br>
&gt; &gt;<br>
&gt; &gt; * **Binder 2:** `let rdata =3D rand2bs(ar)`<br>
&gt; &gt; (Client&#39;s attestation nonce)<br>
&gt; &gt;<br>
&gt; &gt; * **Binder 3:** `let rdata =3D exp0`<br>
&gt; &gt; (Early exporter)<br>
&gt; &gt;<br>
&gt; &gt; * **Binder 4:** `let rdata =3D pub2bs(pubEK)`<br>
&gt; &gt; (Ephemeral public key)<br>
&gt; &gt;<br>
&gt; &gt; * **Binder 5:** `let rdata =3D (ar,exp0)`<br>
&gt; &gt; (Attestation nonce + Early exporter)<br>
&gt; &gt;<br>
&gt; &gt; * **Binder 6:** `let rdata =3D (ar,pubEK)`<br>
&gt; &gt; (Attestation nonce + Ephemeral public key)<br>
&gt; &gt;<br>
&gt; &gt; * **Binder 7:** `let rdata =3D (ar,exp0,pubEK)`<br>
&gt; &gt; (Attestation nonce + Early exporter + Ephemeral public key)<br>
&gt; &gt;<br>
&gt; &gt; * **Aggregate:** `let rdata =3D (cb,pubEK)`<br>
&gt; &gt; (Custom HS-derived exporter + Ephemeral public key)<br>
&gt; &gt;<br>
&gt; &gt; * **Proposal:** `let cb =3D kdf_exp(hs,log_SH) in let rdata =3D (=
ar,cb,pubEK)`<br>
&gt; &gt; (Attestation nonce + Custom HS-derived exporter + Ephemeral publi=
c key)<br>
&gt; &gt;<br>
&gt; &gt; ```<br>
&gt; &gt;<br>
&gt; &gt; 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 cryptogr=
aphically bind to a trusted 3rd party to validate the identity associated w=
ith the given TLS connection.<br>
&gt; &gt;<br>
&gt; &gt; I do not believe it is necessary to evaluate the merits of how va=
lues like `cb` are derived when none of the models can even stand up to sin=
gle key compromise -- of which -- binding a CA-backed `pubLTK` with the ses=
sion is what would be required.<br>
&gt; &gt;<br>
&gt; &gt; As of the currently published commit (#f96761d) in the shared rep=
o [11], the vulnerability analysis in the public release relies on an archi=
tecture that is fundamentally misaligned with the recommendations discussed=
 in both of the most recent revisions for the current front-running individ=
ual I-Ds: `draft-fossati-seat-early-attestation` and `draft-fossati-seat-ex=
pat`.<br>
&gt; &gt;<br>
&gt; &gt; ## Other remarks<br>
&gt; &gt;<br>
&gt; &gt; While formal methods are an invaluable tool for our process, thei=
r utility depends entirely on the accuracy of the models themselves.<br>
&gt; &gt;<br>
&gt; &gt; 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 &quo=
t;suggest that more recent proposals draft-fossati-seat-early-attestation a=
nd draft-ritz-seat-facts add unnecessary complexity of intra-handshake atte=
station without adding any security benefit&quot;. [12] Furthermore, I do n=
ot believe repeating such statements serves the SEAT WG&#39;s best interest=
s unless concrete evidence for those claims can be brought forward and exam=
ined independently.<br>
&gt; &gt;<br>
&gt; &gt; I respectfully request that the authors update their ProVerif art=
ifacts to accurately reflect the actual binder derivations (such as the `HK=
DF-Expand-Label` derivation in Section 5.1.1) and the standard `Certificate=
Verify` boundaries established by the WG&#39;s drafts if they have not alre=
ady done so, and present that work here.<br>
&gt; &gt;<br>
&gt; &gt; With all of that said, I strongly believe this effort unequivocal=
ly demonstrates and makes clear that no further consideration of the long-e=
xpired `draft-fossati-tls-attestation` I-D is necessary effort in this WG. =
I would strongly recommend that any vendors still deploying systems based o=
n 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.<br>
&gt; &gt;<br>
&gt; &gt; Finally and to that end, I suggest this working group focus its f=
uture energy on carefully considering the merits of active indivual I-Ds su=
ch 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).<b=
r>
&gt; &gt;<br>
&gt; &gt; Authors (all): Please feel free to correct me if I&#39;ve missed =
a substantive detail, though nits are also okay!<br>
&gt; &gt;<br>
&gt; &gt; Cheers,<br>
&gt; &gt; Nathanael<br>
&gt; &gt;<br>
&gt; &gt; ---<br>
&gt; &gt;<br>
&gt; &gt; [9] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KBS=
" rel=3D"noreferrer" target=3D"_blank">https://github.com/CCC-Attestation/f=
ormal-spec-KBS</a><br>
&gt; &gt;<br>
&gt; &gt; [10] <a href=3D"https://mailarchive.ietf.org/arch/msg/tls/amNYPs3=
eV3a-l5bFQtUDGx4fU24/" rel=3D"noreferrer" target=3D"_blank">https://mailarc=
hive.ietf.org/arch/msg/tls/amNYPs3eV3a-l5bFQtUDGx4fU24/</a><br>
&gt; &gt;<br>
&gt; &gt; [11] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S/tree/f96761deeee3b7574959eec9f44fe940b33dcbde" rel=3D"noreferrer" target=
=3D"_blank">https://github.com/CCC-Attestation/formal-spec-KBS/tree/f96761d=
eeee3b7574959eec9f44fe940b33dcbde</a><br>
&gt; &gt;<br>
&gt; &gt; [12] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KB=
S/blob/f96761deeee3b7574959eec9f44fe940b33dcbde/README.md?plain=3D1#L58" re=
l=3D"noreferrer" target=3D"_blank">https://github.com/CCC-Attestation/forma=
l-spec-KBS/blob/f96761deeee3b7574959eec9f44fe940b33dcbde/README.md?plain=3D=
1#L58</a><br>
&gt; &gt;<br>
&gt; &gt; -----------------------------------------------<br>
&gt; &gt;<br>
&gt; &gt; From: Muhammad Usama Sardar &lt;<a href=3D"mailto:muhammad_usama.=
sardar@tu-dresden.de" target=3D"_blank">muhammad_usama.sardar@tu-dresden.de=
</a>&gt;<br>
&gt; &gt; Date: Thu, 25 Jun 2026 at 16:19<br>
&gt; &gt; Subject: [Seat] Re: Relay Attacks in Intra-handshake Attestation =
for Confidential Agentic AI Systems<br>
&gt; &gt; To: <a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.=
org</a> &lt;<a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.or=
g</a>&gt;, UFMRG IRTF &lt;<a href=3D"mailto:ufmrg@irtf.org" target=3D"_blan=
k">ufmrg@irtf.org</a>&gt;<br>
&gt; &gt;<br>
&gt; &gt; Hi SEAT and UFMRG,<br>
&gt; &gt;<br>
&gt; &gt; In line with the SEAT charter (emphasis our own):<br>
&gt; &gt;<br>
&gt; &gt; The working group will engage with the research community on the<=
br>
&gt; &gt; evaluation and formal analysis of the protocol artifacts in paral=
lel<br>
&gt; &gt; with the specification work.<br>
&gt; &gt;<br>
&gt; &gt; and the required property in the SEAT charter (emphasis our own):=
<br>
&gt; &gt;<br>
&gt; &gt; The attested D(TLS) protocol extension will also describe a minim=
um<br>
&gt; &gt; subset of properties that the attested state must convey in order=
<br>
&gt; &gt; to bind the Evidence and Attestation Results to the TLS connectio=
n.<br>
&gt; &gt;<br>
&gt; &gt; we (I, Slava, and Jean-Marie) would like to share the concrete te=
chnical results for binding mechanisms of the intra-handshake attestation f=
rom our formal analysis in ProVerif [9]:<br>
&gt; &gt;<br>
&gt; &gt; - All analyzed binding mechanisms and the corresponding implement=
ations of intra-handshake attestation are vulnerable to relay attacks.<br>
&gt; &gt;<br>
&gt; &gt; - Early exporter helps achieve level 1 binding.<br>
&gt; &gt;<br>
&gt; &gt; - Our proposed mechanism helps achieve level 2 binding.<br>
&gt; &gt;<br>
&gt; &gt; - It may not be possible to achieve level 3 binding in intra-hand=
shake attestation alone.<br>
&gt; &gt;<br>
&gt; &gt; - The research suggests that more recent proposals draft-fossati-=
seat-early-attestation and draft-ritz-seat-facts add complexity of intra-ha=
ndshake attestation relative to draft-fossati-seat-expat without offering a=
dditional security benefits.<br>
&gt; &gt;<br>
&gt; &gt; To support independent review, further research and development b=
y the RG/WG, we have released the ProVerif artifacts [9] under Apache-2.0 L=
icense. We hope these artifacts provide useful input for SEAT.<br>
&gt; &gt;<br>
&gt; &gt; There is also a paper-and-pen proof in the corresponding paper su=
pporting the above results, which we will share soon with the WG/RG.<br>
&gt; &gt;<br>
&gt; &gt; We welcome any constructive and technical feedback from the WG/RG=
 and will be happy to address it.<br>
&gt; &gt;<br>
&gt; &gt; Best regards,<br>
&gt; &gt;<br>
&gt; &gt; Usama, Slava, and Jean-Marie<br>
&gt; &gt;<br>
&gt; &gt; -----------------------------------------------<br>
&gt; &gt;<br>
&gt; &gt; From: Nathanael Ritz &lt;<a href=3D"mailto:nathanritz@gmail.com" =
target=3D"_blank">nathanritz@gmail.com</a>&gt;<br>
&gt; &gt; Date: Mon, 22 Jun 2026 at 11:12<br>
&gt; &gt; Subject: Re: [Seat] Re: Relay Attacks in Intra-handshake Attestat=
ion for Confidential Agentic AI Systems<br>
&gt; &gt; To: <a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.=
org</a> &lt;<a href=3D"mailto:seat@ietf.org" target=3D"_blank">seat@ietf.or=
g</a>&gt;<br>
&gt; &gt;<br>
&gt; &gt; Hi SEAT,<br>
&gt; &gt;<br>
&gt; &gt; I have some additional comments to offer in this thread.<br>
&gt; &gt;<br>
&gt; &gt; Comments are offered below with [NR]:<br>
&gt; &gt;<br>
&gt; &gt; On Thu, 18 Jun 2026 at 15:58, Muhammad Usama Sardar &lt;<a href=
=3D"mailto:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_=
usama.sardar@tu-dresden.de</a>&gt; wrote:<br>
&gt; &gt;<br>
&gt; &gt; Hi Paul,<br>
&gt; &gt;<br>
&gt; &gt; [...] Formal (Symbolic and paper-and-pen) analyses is the most se=
rious thing we could do. Let us know if you had/have something else in mind=
.<br>
&gt; &gt;<br>
&gt; &gt; [NR] I generally agree with Usama&#39;s sentiment regarding the m=
erits of additional formal analysis work, which he shared with me at [2]. O=
f course, understanding the context helps interpret any formal analysis to =
evaluate how and why certain query results relate to the present work.<br>
&gt; &gt;<br>
&gt; &gt; Technically, we do not believe we have missed any binding mechani=
sm for intra-handshake attestation that might lead to different results.<br=
>
&gt; &gt;<br>
&gt; &gt; [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 &quot;two [3,4] out of three current proposals under discussion in the =
WG.&quot; While formal analysis of real-world implementations may be useful=
 for some vendors still deploying old, unstable specs (resulting in high-se=
verity 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.<br>
&gt; &gt;<br>
&gt; &gt; 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 implementatio=
n for intra-handshake attestation you would like us to check. Formal analys=
is artifacts are easily extensible.<br>
&gt; &gt;<br>
&gt; &gt; [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 d=
efined by section 5.1.1.<br>
&gt; &gt;<br>
&gt; &gt; One can check additional binding mechanisms by just changing the =
value of a single variable: rdata. Everything else is automated.<br>
&gt; &gt;<br>
&gt; &gt; [NR] Depending on the model&#39;s construction, merely changing t=
he input to `rdata` may not yield new results, as that modification alone w=
ould be insufficient without also incorporating a CA-backed certificate int=
o the same model. I don&#39;t think anyone in this WG will argue that any c=
oncrete protocol proposals submitted to the list should not produce a usabl=
e second trust anchor. Usama also noted this sentiment in his IETF-125 foll=
ow-up to the CFRG mailing list regarding his presentation about composing r=
emote attestation with TLS [5]. I agree that providing two independent trus=
t anchors seems to be the general point of the exercise.<br>
&gt; &gt;<br>
&gt; &gt; [NR] Furthermore, both `draft-fossati-seat-expat-02` and `draft-f=
ossati-seat-early-attestation-04` acknowledge the risks of so-called &quot;=
split deployments,&quot; 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.<br>
&gt; &gt;<br>
&gt; &gt; [NR] Therefore, beyond merely updating the single `rdata` value -=
- the formal model needs to evaluate the security properties when a CA-back=
ed signing key (LTK) is composed with Evidence signed over by the attestati=
on signing key (AK) present inside the attesting environment. In a follow-u=
p to Usama&#39;s request [2] for my own formal analysis work on `draft-foss=
ati-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 i=
t&#39;s own (pending critical feedback on my model), I still found that bot=
h the AK and LTK independently provided resilience against single key compr=
omise.<br>
&gt; &gt;<br>
&gt; &gt; [NR] My models for `draft-fossati-seat-early-attestation-03` (ext=
ended from Sardar et al.&#39;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 st=
olen or otherwise compromised itself.<br>
&gt; &gt;<br>
&gt; &gt; [NR] In short, while it&#39;s hard to be sure about the full scop=
e of the forthcoming work for now, I would like to see Usama and collaborat=
ors share a model that explicitly evaluates the binder mechanism from `draf=
t-fossati-seat-early-attestation-04`, where the assumptions align with that=
 draft&#39;s security model: modeling a TEE-resident TIK that is provisione=
d with a CA-backed certificate alongside the novel binder mechanism. I woul=
d be very interested to see the results of such a direct analysis, regardle=
ss of opinions regarding the status of the draft&#39;s apparent scope withi=
n the SEAT charter.<br>
&gt; &gt;<br>
&gt; &gt; Sincerely,<br>
&gt; &gt;<br>
&gt; &gt; Nathanael<br>
&gt; &gt;<br>
&gt; &gt; [0] <a href=3D"https://github.com/CCC-Attestation/formal-spec-KBS=
#upcoming-and-recent-talks-and-research-visits" rel=3D"noreferrer" target=
=3D"_blank">https://github.com/CCC-Attestation/formal-spec-KBS#upcoming-and=
-recent-talks-and-research-visits</a><br>
&gt; &gt;<br>
&gt; &gt; [1] <a href=3D"https://datatracker.ietf.org/doc/draft-usama-seat-=
intra-vs-post/" rel=3D"noreferrer" target=3D"_blank">https://datatracker.ie=
tf.org/doc/draft-usama-seat-intra-vs-post/</a><br>
&gt; &gt;<br>
&gt; &gt; [2] <a href=3D"https://mailarchive.ietf.org/arch/msg/seat/VEgdWuR=
dOq0YwGV6OUTWUp5ShWM/" rel=3D"noreferrer" target=3D"_blank">https://mailarc=
hive.ietf.org/arch/msg/seat/VEgdWuRdOq0YwGV6OUTWUp5ShWM/</a><br>
&gt; &gt;<br>
&gt; &gt; [3] <a href=3D"https://datatracker.ietf.org/doc/draft-fossati-sea=
t-early-attestation/" rel=3D"noreferrer" target=3D"_blank">https://datatrac=
ker.ietf.org/doc/draft-fossati-seat-early-attestation/</a><br>
&gt; &gt;<br>
&gt; &gt; [4] <a href=3D"https://datatracker.ietf.org/doc/draft-ritz-seat-f=
acts/" rel=3D"noreferrer" target=3D"_blank">https://datatracker.ietf.org/do=
c/draft-ritz-seat-facts/</a><br>
&gt; &gt;<br>
&gt; &gt; [5] <a href=3D"https://mailarchive.ietf.org/arch/msg/cfrg/sUQnF1K=
OL5XsvCwY0VRASICk3T4/" rel=3D"noreferrer" target=3D"_blank">https://mailarc=
hive.ietf.org/arch/msg/cfrg/sUQnF1KOL5XsvCwY0VRASICk3T4/</a><br>
&gt; &gt;<br>
&gt; &gt; [6] <a href=3D"https://www.ietf.org/archive/id/draft-fossati-seat=
-expat-02.html#section-5.2-2" rel=3D"noreferrer" target=3D"_blank">https://=
www.ietf.org/archive/id/draft-fossati-seat-expat-02.html#section-5.2-2</a><=
br>
&gt; &gt;<br>
&gt; &gt; [7] <a href=3D"https://www.ietf.org/archive/id/draft-fossati-seat=
-early-attestation-04.html#section-5.2-2" rel=3D"noreferrer" target=3D"_bla=
nk">https://www.ietf.org/archive/id/draft-fossati-seat-early-attestation-04=
.html#section-5.2-2</a><br>
&gt; &gt;<br>
&gt; &gt; [8] <a href=3D"https://mailarchive.ietf.org/arch/msg/seat/zD1NTnU=
EdRM5SayHxXfuO9robTA/" rel=3D"noreferrer" target=3D"_blank">https://mailarc=
hive.ietf.org/arch/msg/seat/zD1NTnUEdRM5SayHxXfuO9robTA/</a><br>
&gt; &gt;<br>
&gt; &gt; On Thu, 18 Jun 2026 at 15:58, Muhammad Usama Sardar &lt;<a href=
=3D"mailto:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_=
usama.sardar@tu-dresden.de</a>&gt; wrote:<br>
&gt; &gt;<br>
&gt; &gt; Hi Paul,<br>
&gt; &gt;<br>
&gt; &gt; On 18.06.26 22:45, Paul Wouters wrote:<br>
&gt; &gt;<br>
&gt; &gt; On Jun 16, 2026, at 17:02, Muhammad Usama Sardar [&lt;<a href=3D"=
mailto:muhammad_usama.sardar@tu-dresden.de" target=3D"_blank">muhammad_usam=
a.sardar@tu-dresden.de</a>&gt;](mailto:<a href=3D"mailto:muhammad_usama.sar=
dar@tu-dresden.de" target=3D"_blank">muhammad_usama.sardar@tu-dresden.de</a=
>) wrote:<br>
&gt; &gt;<br>
&gt; &gt; Respectfully, just to clarify: as the email mentions, the work wa=
s requested by Paul, the AD at that time.<br>
&gt; &gt;<br>
&gt; &gt; i have not requested any formal verification papers.<br>
&gt; &gt;<br>
&gt; &gt; I meant to refer to the protocol design and analysis work, not th=
e paper. This is what we (Slava, Jean-Marie, and I) understood you to be re=
questing.<br>
&gt; &gt;<br>
&gt; &gt; 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 writ=
ing paper and getting it reviewed at conferences helps in independent evalu=
ation of the design approach and artifacts, in addition to WG participants&=
#39; review.<br>
&gt; &gt;<br>
&gt; &gt; I have asked the WG in the past to seriously look at intra handsh=
ake options with offering a straw man idea,<br>
&gt; &gt; 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.<br>
&gt; &gt;<br>
&gt; &gt; but you seem mostly interested in disproving your own versions of=
 intra-handshake in favour of your preferred solution.<br>
&gt; &gt;<br>
&gt; &gt; I don&#39;t think they are my versions. We have collected the bin=
ding mechanisms from existing real-world implementations of intra-handshake=
 attestation, including:<br>
&gt; &gt;<br>
&gt; &gt; - Meta&#39;s AI<br>
&gt; &gt;<br>
&gt; &gt; - Cocos AI<br>
&gt; &gt;<br>
&gt; &gt; - Edgeless Systems<br>
&gt; &gt;<br>
&gt; &gt; - CCC proof-of-concept<br>
&gt;<br>
&gt; &gt;<br>
&gt; &gt; and discussions with the community, i.e., several research and in=
dustry consortia [0], including the Confidential Computing Consortium.<br>
&gt; &gt;<br>
&gt; &gt; Technically, we do not believe we have missed any binding mechani=
sm 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 bindin=
g 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 automat=
ed.<br>
&gt; &gt;<br>
&gt; &gt; I also do not believe post-handshake is my preferred solution. It=
 was recommended by TLS WG back then, and several developers have shown the=
ir preference because of security, privacy and unnecessary complexity issue=
s with intra-handshake attestation [1].<br>
&gt; &gt;<br>
&gt; &gt; I still haven&#39;t seen, or missed in the many emails, of why bi=
nding TEE PKI evidence and web server tls WebPKI cannot be done with some D=
NS/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) a=
nd avoiding rebinding attacks by using a different compromised TEE<br>
&gt; &gt;<br>
&gt; &gt; via the SAN reference of the TEE.<br>
&gt; &gt;<br>
&gt; &gt; We did not understand how to formalize that. If you could write a=
 draft clarifying the protocol spec, we&#39;ll happily do the analysis for =
you and help you move the idea forward.<br>
&gt; &gt;<br>
&gt; &gt; Best regards,<br>
&gt; &gt;<br>
&gt; &gt; -Usama<br>
</blockquote></div></div>
</div>
</div>
</div>

--000000000000cbc0e50655a8fab7--