[Seat] Re: Threat model and properties for attested TLS

[Songbo Bu <[e-mail]>]

Nathanael, Chengxin, Tiru, Jakub, Yaron, Ionut, Usama, Haowen, Steve, all,

Thank you.

We have narrowly discussed this many times that "correlation goals" do not
need any assumptions and this debate was settled. Very simple way to think
of this is that: why does proposed binder achieve level 2 without any
assumption? This is a concrete counter-example to your position and has
been narrowly discussed before. I do not understand why we are restarting
this settled debate again.

Paper-and-pen proof in section 6.4 is not the same as ProVerif proof.
Paper-and-pen proof is cryptographic proof. ProVerif is not cryptographic
proof. Conflating the two is a category error. Again, we have discussed
this. Please clarify why you are repeating this again, or present your new
argument more narrowly.

Chengxin narrowly answered your question 10 minutes before your email [1].
So can you please clarify if you had a chance to read his message before
sending this one or if not, does that answer your question?

I could not find GC-2 in Intra-handshake.fail paper [2]. This is again
conflating two very different things.

My broader point is people keep repeating the same question over and over
again and then complain that we are doing "marketing campaign". Please read
the papers carefully and do not repeat the settled matters for SEAT to
proceed forward.

Usama previously told me that in 2029, confidential computing consortium
predicts more than 75% of the connections to be based on confidential
computing. The community needs a standard. Let's move forward rather than
backward.

Best,
Songbo

[1] https://mailarchive.ietf.org/arch/msg/seat/tg4y4s_gixVH80ThHVVl0LRzEww/
[2]
https://www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS

Nathanael Ritz <[e-mail]> 于2026年8月20日周四 09:33写道：

> Hi Usama,
>
> On Tue, 11 Aug 2026 at 18:51, Muhammad Usama Sardar <
> [e-mail]> wrote:
>
>> [...]
>>
>> Effectively, there is zero entropy in the binder [0] of
>> draft-fossati-seat-early-attestation-06 since all values are public. [...]
>>
>
> On Wed, 12 Aug 2026 at 19:01, Muhammad Usama Sardar <
> [e-mail]> wrote:
>
>> [SNIP] ===
>>
>> Hi Nathanael,
>>
>> Thanks for the correction. I meant secrecy (confidentiality) rather than
>> entropy in my last email.
>>
>
> Thanks for sharing your intent. However, substituting "secrecy" for
> "entropy" structurally invalidates your critique of the early-attestation
> binder. This conflation is the exact mechanism that invalidates the formal
> model provided in the "Intra-handshake.fail" paper as a suitable tool for
> analysis against draft-fossati-seat-early-attestation-06. Since you appear
> curious about how Evidence can possibly be bound to the secure channel
> without involving any shared secret, it turns out that it is through the
> application of entropy. In fact, the models you are extending from are
> designed to demonstrate just that (and the consequence of what happens when
> entropy is insufficient) [0]. Unfortunately, as I have explained on-list
> before, a close examination of the associated symbolic models reveals a
> structural discrepancy between the threat model stated in the mathematical
> proof and the execution of the ProVerif correlation queries.
>
> In Section 6.4 of the paper (that is, Proposition 1), the security
> hierarchy (G3 => G2 => G1) is established strictly under Assumption 1. This
> assumption *explicitly* requires the absence of weak hashes (WH) and weak
> Diffie-Hellman groups (WDH). However, the provided ProVerif models
> associated with the paper define `WeakHash` through algebraic rewrite rules
> as returning a static `collision` [1], consistent with [0].
>
> Because the TLS 1.3 key schedule relies entirely on these hash functions,
> the introduction of `WeakHash` collapses the protocol. This is why its
> exclusion is required when evaluating injective-agreement or key secrecy
> properties in your other-props.pvl library file. This is because, following
> the snapshot of CH...SH and the derivation of the handshake traffic keys,
> it forces all other transcript hashes and derived keys to resolve with
> "collision", instead of the 512+ bits of public entropy that TLS 1.3 would
> otherwise provide under an idealized "StrongHash".
>
> By lacking the necessary exclusions, the automated solver evaluates the
> goals in an environment where `WeakHash` and `WeakDH` are trivially
> exploitable. This directly violates the specific premises established by
> Assumption 1 in your paper. Real-world TLS 1.3 does not allow an adversary
> to unilaterally downgrade algorithms without consequence [2]; the handshake
> thoroughly utilizes transcript hashes in all of its `Derived-Secret`
> outputs [3]. Therefore, as demonstrated by the paper's own pen-and-paper
> proofs in Section 6.4, authentication of G3 mathematically guarantees a
> legitimate, untampered initial exchange because it successfully
> authenticates the entire deterministic transcript log (including the Log_SH
> snapshot of CH...SH).
>
> This is why when the formal model is corrected to properly enforce
> Assumption 1 by excluding the negotiation of a `WeakHash` within the
> correlation queries, the evaluation of (kc1 = kc2) will return true when
> utilizing the proposed binder (or by simply replacing the non-standard
> derivation of `cb` simply with the CH...SH `log_SH` checkpoint).
>
> I understand that you may have only been able to briefly skim the mailing
> list recently. However, I recently shared a method to evaluate the GC-2
> relay attack query from your other-props.pvl file, complete with the
> assumption that the ephemeral signing key is somehow compromised (in line
> with the summary text from CVE-2026-33697) [4]. Have you run the query [5]
> for yourself yet? If you have not yet had the opportunity, I encourage you
> or your colleagues to evaluate the query and share your findings with the
> working group.
>
> Sincerely,
> Nathanael Ritz
>
> [0] https://ieeexplore.ieee.org/document/7958594
>
> [1]
> https://github.com/muhammad-usama-sardar/intra-handshake.fail/blob/main/proposal/tls-lib-simple.pvl#L89
>
> [2] https://mailarchive.ietf.org/arch/msg/tls/evs5vqvK7kTEFHCPdnqM7Xf3Yyk/
>
> [3] https://mailarchive.ietf.org/arch/msg/tls/LaZwmoGaUxxGQXKvfa58mPg77y0/
>
> [4]
> https://mailarchive.ietf.org/arch/msg/seat/G0QyNW2SM1uPpOFeGeJgtbKziYg/
>
> [5] https://github.com/nathanaelritz/gists/blob/main/Property_G-C2.pvl
> _______________________________________________
> Seat mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]
>