[Seat] Re: Regarding symbolic analysis of draft-fossati-seat-early-attestation-06

[Nathanael Ritz <[e-mail]>]

Hi, comments inline with [NR]:

On Sun, 9 Aug 2026 at 08:02, Songbo Bu <[e-mail]> wrote:

> Nathanael,
>
> Since you invited questions, I have some technical questions.
>
> Are you confusing draft-fossati-tls-attestation-06 that Usama have in
> intra-handshake.fail paper and repo with
> draft-fossati-seat-early-attestation-06?
>
> If not, can you share your rationale of how you conclude
> "draft-fossati-seat-early-attestation-06 was applied to binder 7" and
> "README was updated to suggest that draft-fossati-seat-early-attestation-06
> is represented by what the page labels as "binder 7""?
>

[NR]: It is right that within the paper-ready README for the paper, binder7
appears to be applied for draft-fossati-tls-attestation-06; thanks for the
correction. To wit, the academic paper-ready language simply states with
careful language that I-Ds such as "draft-fossati-seat-early-attestation
and draft-ritz-seat-facts may add unnecessary complexity of intra-handshake
attestation without adding any security benefit compared to post-handshake
attestation alone [...]" [0]

[NR]: However, in contrast, in an a seperate Internet-Draft that Usama
shares from the same README [1], we find this statement: "At least the
following protocol specifications with intra-handshake attestation path are
vulnerable to CVE-2026-33697 and EUVD-2026-16488: [...]
draft-fossati-seat-early-attestation:
symbolic and computational proof of insecurity (orginially done for -04 and
applies also to -06)"

[NR]: So, the question remains where and how is proof supplied? I don't
believe the proof is available for public review.


>
> Are you refusing the vulnerability CVE-2026-33697 that all vendors and
> draft authors have acknowledged (
> https://www.ietf.org/archive/id/draft-intra-handshake-fail-03.html#section-4)?
> If so, I haven't seen any technical substance at all in your refusal.
>

[NR]: This appears to be putting words in my mouth and I would ask that
participants please refrain from doing so in the future.


> For "the entire working group would appreciate", I don't think you can
> speak on behalf of the entire WG. Everyone can say his own opinion and you
> can say your own opinion but not pretend it for the entire WG. From
> context, it is clear that "other claims" meant other claims in your email
> that he was responding to.
>

[NR]: It would be helpful to know what specific claims represent what kind
of overstatement, so I can address them directly.


>
> Can you narrowly share the exact value of `rdata` that you believe is the
> correct value for this draft version that I can put in Usama's model to
> check all binding properties without changing anything else in the model?
>

[NR]: Absolutely: `log_SH` represents the checkpoint for
ClientHello...ServerHello that draft-fossati-seat-early-attestation -06
calls for in section 5.1.1. However, as I clearly identified before,
Usama's model includes a `selfsign` parameter that is generated on the
server-side and is then passed through the `CRT` message over the adversary
controlled channel unchecked. Not only is `selfsign` unchecked by the
client-side, but is entirely unused. It represents artificial noise in the
system and therefore causes the G3 query to fail unilaterally, regardless
of how the query is written (without applying the industry standard
cryptographic assumptions applied to TLS 1.3).

[NR]: With that bug present, there are still other ways to properly
evaluate the properties of the CH...SH checkpoint inside the `rdata` field.
I invite participants to cross reference the results between any of the
numbered binder folders against other-props.pvl and evaluate "Property
G-C2: Composition Property for Relay attack" [3]. Of course, that property
already returns true as-is because it has both pubAK and pubEK present in
the RHS disjunctions. Take that very same query and remove LeakedEK(pubEK)
from it, leaving the query to evaluate the resilience against relay attacks
by presence of AK alone (example query shown here: [4]).

[NR]: Note that taking a query designed to test against relay attacks and
reducing the number of disjunctions on the RHS makes the query and
demonstrated property stronger, and does not represent a modeling change of
any kind. Testing AK alone with the existing binders based on the expired
and withdrawn draft returns false; this demonstrates the insecurity.
However, that very same query with `Log_SH` placed inside `rdata` will flip
that result to true, demonstrating that the non-secret two-sided connection
uniquness of the CH...SH checkpoint effectively mitigates the relay attacks
found for the niaeve binders.


>
> Usama said he is close to finding a computational proof of *insecurity*
> for draft-fossati-seat-early-attestation. Are you refusing his claim? Do
> you have a computational proof of *security* for this draft?
>

[NR]: I will not engage with non-sequitors. Since it appears this kind of
language appears a second time in the same email I will ask a second time
that participants refrain from putting words in my mouth, thank you.


>
> I am really surprised how in a few hours your claim has changed from your
> own "Early take-away" to closing the matter. Closing the matter of widely
> acknowledged critical vulnerabilities seems huge disservice to the
> community.
>

[NR]: I quite clearly stated that I was open to specific questions if they
were raised, and if not, then I would be happy to consider the matter
closed. Since some questions were raised, here we are.

Cheers,
Nathanael


>
> Best,
> Songbo
>

[0]
https://github.com/muhammad-usama-sardar/intra-handshake.fail/blob/819bb7f20ac458b27c9be2c91cce1e72b8b5f4f7/README.md?plain=1#L140

[1]
https://github.com/muhammad-usama-sardar/intra-handshake.fail/blob/819bb7f20ac458b27c9be2c91cce1e72b8b5f4f7/README.md?plain=1#L11

[2]
https://www.ietf.org/archive/id/draft-intra-handshake-fail-04.html#section-8-2.2.1

[3]
https://github.com/muhammad-usama-sardar/intra-handshake.fail/blob/819bb7f20ac458b27c9be2c91cce1e72b8b5f4f7/binder7/other-props.pvl#L669

[4] https://github.com/nathanaelritz/gists/blob/main/Property_G-C2.pvl