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

[Chengxin Huang <[e-mail]>]

Dear Nathanael,

You have raised 2 concerns in [intra-handshake.fail]:

First, WeakDH. We have already settled it in [seat] and [ufmrg]. It is a
violation of seat procedures to keep repeating it without bringing any new
information.

Second, the statement:
"The core problem is that intra-handshake attestation binds Evidence to an
unauthenticated peer."

This is a new concern that you have raised for the first time. The
statement in the paper is correct and consistent with [cve]. See the "CWE"
section of [cve] explicitly stating
"CWE-322: Key Exchange without Entity Authentication"
"CWE-346: Origin Validation Error"

Please follow the [advice] of Dr. Schmeig to move on positively.

Best regards,

Chengxin Huang

[intra-handshake.fail]
https://www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS
[seat]
https://mailarchive.ietf.org/arch/msg/seat/x3eQxFjQFJLceae6l4_NgXnmsDY/
[ufmrg]
https://mailarchive.ietf.org/arch/msg/ufmrg/ZRhR7o1HrWxfGDfgRJMR65RBkDE/
[cve] https://www.cve.org/CVERecord?id=CVE-2026-33697
[advice]
https://mailarchive.ietf.org/arch/msg/seat/t8aobzB374lWiLzrVrORY7kGYyQ/

On Fri, Aug 21, 2026 at 12:01 PM Nathanael Ritz <[e-mail]>
wrote:

> Hi Songbo, Usama,
>
> On Thu, 20 Aug 2026 at 15:22, Muhammad Usama Sardar <
> [e-mail]> wrote:
> > [...] both Songbo (to whom you are replying) and Chengxin (whose email
> [1] he quoted) are co-authors with me in the draft [5] and have been
> contributing to the follow-up research built on the same artifacts, and so
> they are both more than capable of answering any technical question either
> on paper or on ProVerif artifacts -- maybe currently even more than me
> because I do not have full context of the discussion in the other thread
> [1] in which they seem to be actively participating.
> >
> > Hope that helps.
> >
> > Best regards,
> > -Usama
>
> On Thu, Aug 20, 2026 at 8:44 AM Songbo Bu wrote:
> > [SNIP] Why does proposed binder achieve level 2 without any assumption?
>
> [NR]: It's because every single input required to compute `kch` is
> deterministically fixed by `log_SH`, meaning there are no free variables in
> the state machine for an adversary to manipulate at that stage. The moment
> evaluation moves to derive `kc`, the key schedule ingests `log_SFIN`, which
> extends the transcript past `log_SH` to include Certificate (`CRT`,
> [including unchecked parameters like the selfsign example]),
> CertificateVerify (`CV_Ext`), and Finished (`FIN`). When weak primitives
> are left unconstrained by RHS disjuncts, the adversary exploits two
> critical reduction rules defined in the symbolic model that trivially
> collapse entropy in the protocol [*]. Because the integrity of the TLS 1.3
> transcript rests squarely on the assumption of CSPRNG-derived hash and
> key-exchange entropy, the `WeakHash` and `WeakDH` constants do not
> represent realistic threats for RFC9846, nor any specifications might
> expect from the SEAT WG.
>
> [NR]: In any case, the correlation queries cannot demonstrate privacy for
> Evidence, resistance to secret compromise, or injective correspondence
> between peers. Because machine identity and peer validation are explicitly
> omitted from the correlation goals, the queries simply demonstrate an
> artifact of the deterministic TLS key schedule. In fact, having (kc1 = kc2)
> evaluate to `true` is entirely possible even during an active MITM attack
> where secrecy and injective agreement are demonstrably compromised. Simply
> put, key correlation on its own is an insufficient metric for determining
> the security of an attested TLS protocol, let alone for capturing
> vulnerability to relay attacks in state-of-the-art proposals to SEAT. That
> does not mean the models themselves are flawed for evaluating the prior art
> for which they were carefully scoped, just that they are out of scope for
> SEAT, as I have indeed repeated before.
>
> Cheers,
> Nathanael
>
> [*] Examples of these trivial exploits manifesting in the models are
> clearly documented in `log.txt` for the proposed binder, spanning lines
> 9202 through 10128 :
> https://github.com/muhammad-usama-sardar/intra-handshake.fail/blob/main/proposal/log.txt
>
> On Thu, 20 Aug 2026 at 18:04, Nathanael Ritz <[e-mail]> wrote:
>
>> Hi Usama,
>>
>> Thanks for the response. Please see my comments inline with [NR], which I
>> hope are helpful:
>>
>> On Thu, 20 Aug 2026 at 15:22, Muhammad Usama Sardar <
>> [e-mail]> wrote:
>> >
>> > Hi folks,
>> >
>> > I was asked to provide some input in this thread, presumably as an
>> author of ESORICS paper [2] or AsiaCCS paper [4]. I'd like to clarify that
>> correlation goals are part of ESORICS paper but G-C2 property is part of
>> AsiaCCS paper. Both seem to be conflated in the two threads. I did not yet
>> have the time to closely follow the other thread [1], but the email cites
>> that thread. So I may be missing some context.
>>
>> [NR]: Not to worry, I don't think there is any conflation between the
>> papers or the threads. For example, the file other-props.pvl is present
>> directly in your own ESORICS artifact repository, where Property G-C2 is
>> explicitly defined and evaluated as the "Composition Property for Relay
>> attack" along with useful and meaningful annotations regarding the goals
>> and properties associated with properly authenticated attested TLS [*].
>>
>> [NR]: Aside from that, we understand that the core cryptographic issue
>> across both works is identical: how attestation Evidence is bound to
>> session parameters, and how that binding is evaluated within the formal
>> model's threat library. The G-C2 query effectively demonstrates that any
>> binder lacking channel context in rdata (Mechanisms 1, 2, 4, and 6 in Table
>> 2) fails against a relay attack (providing direct evidence towards
>> CVE-2026-33697).
>>
>> > [...] I haven't seen any concrete statement being disputed in the above
>> two papers. If there is a disputed statement in one of the papers, please
>> exactly quote the statement(s) first, then suggest the change, and explain
>> your rationale, so that I can understand the context of what exactly is
>> being disputed.
>>
>> [NR]: Sure: The conclusion of the ESORICS paper claims that "the core
>> problem" that presumably led to the discovery of CVE-2026-33697 is that
>> "intra-handshake attestation binds Evidence to an unauthenticated peer."
>> This assertion directly contradicts the published technical description of
>> CVE-2026-33697 itself, which identifies the root cause as a failure of
>> channel binding. I suggest you find a way to incorporate the core technical
>> finding from the CVE which states: "Because the attestation evidence is
>> bound to the ephemeral key but not to the TLS channel, possession of that
>> key is sufficient to relay or divert the attested TLS session" instead.
>>
>> [NR]: The rationale is straightforward: as demonstrated already by the
>> supplied model and queries, the CVE-2026-33697 vulnerability is possible
>> because that binder design contained zero channel context bound to signed
>> hardware Evidence. That is to say, if the TLS signing key is not
>> confidential, an adversary can relay the Evidence using that
>> non-confidential key because the Evidence was never tied to the TLS channel
>> in the first place.
>>
>> >
>> > Some quick notes for a couple of emails -- more later when I have time.
>> >
>> > On 20.08.26 16:44, Songbo Bu wrote:
>> >
>> > 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.
>> >
>> > I fully agree. We discussed it comprehensively and "settled" it in the
>> SEAT [0] plus UFMRG [3] threads. If there is still some disagreement, our
>> upcoming paper provides more evidence.
>> >
>> > 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.
>> >
>> > Correct.
>>
>> [NR]:  A proof from a symbolic verification tool like ProVerif is
>> distinct from a computational proof yes, but that statement seems to
>> displace the core mathematical properties shared between the two
>> complementary approaches. Regarding the noted gap in the symbolic models, I
>> imagine you would know well enough that when ProVerif verifies a
>> correspondence assertion, it verifies that the condition holds for every
>> reachable trace in the model. Because the threat library inherits the
>> algebraic rewrite rules for weak primitives from the original reftls
>> artifacts to simulate legacy downgrade attacks (SLOTH, Logjam), those
>> branches exist in ProVerif's state space.
>>
>> [NR]: So, the discrepancy is straightforward: In Section 6.4, Proposition
>> 1 establishes the security hierarchy strictly under Assumption 1 (Absence
>> of WeakHash and WeakDH). However, in the supplied ProVerif models, the
>> query for G3 is executed without disjuncts to enforce Assumption 1. The
>> automated solver explores paths where weak primitives are forcibly
>> negotiated, trivially stripping the protocol of its intrinsic entropy and
>> thus causing the query to evaluate to false.
>>
>> [NR]: The pen-and-paper proof from the ESORICS paper demonstrates through
>> logical implication from Proposition 1 (G3 => G2 => G1) that authentication
>> of the conveyed Evidence by the peer is only required to close at G3
>> (Finished); as long as the private Attestation Key for the peer is secure,
>> then the initial exchange is provably untampered.
>>
>> >
>> > [...] I need to understand the dispute to judge whether it was already
>> discussed among authors or otherwise which of my co-authors I should
>> consult.
>>
>> [NR]: I suggest consulting your co-author who helped prepare the
>> pen-and-paper proof for Section 6.4 of the ESORICS paper. That author ought
>> to be able to confirm the following argument: Under Assumption 1 (the
>> absence of weak hashes and weak DH), successful authentication at G3
>> mathematically guarantees a legitimate, untampered initial exchange because
>> it successfully authenticates the entire deterministic transcript log
>> (including the transcript checkpoint log covering CH...SH).
>>
>> Cheers,
>> Nathanael
>>
>> [*]
>> https://github.com/muhammad-usama-sardar/intra-handshake.fail/blob/main/proposal/other-props.pvl#L678
>>
>>
>>
>> On Thu, 20 Aug 2026 at 15:22, Muhammad Usama Sardar <
>> [e-mail]> wrote:
>> >
>> > Hi folks,
>> >
>> > I was asked to provide some input in this thread, presumably as an
>> author of ESORICS paper [2] or AsiaCCS paper [4]. I'd like to clarify that
>> correlation goals are part of ESORICS paper but G-C2 property is part of
>> AsiaCCS paper. Both seem to be conflated in the two threads. I did not yet
>> have the time to closely follow the other thread [1], but the email cites
>> that thread. So I may be missing some context.
>> >
>> > In the following I am speaking for myself and not for the authors. As
>> you can see, the set of authors is different for AsiaCCS paper and ESORICS
>> paper. So I need to understand the dispute to judge whether it was already
>> discussed among authors or otherwise which of my co-authors I should
>> consult.
>> >
>> > I may have missed something in the 100+ SEAT emails (and a dozen more
>> emails from RATS in a sub-thread of this thread) within 3 weeks, but in a
>> quick skim of archives, I haven't seen any concrete statement being
>> disputed in the above two papers. If there is a disputed statement in one
>> of the papers, please exactly quote the statement(s) first, then suggest
>> the change, and explain your rationale, so that I can understand the
>> context of what exactly is being disputed.
>> >
>> > Some quick notes for a couple of emails -- more later when I have time.
>> >
>> > On 20.08.26 16:44, Songbo Bu wrote:
>> >
>> > 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.
>> >
>> > I fully agree. We discussed it comprehensively and "settled" it in the
>> SEAT [0] plus UFMRG [3] threads. If there is still some disagreement, our
>> upcoming paper provides more evidence.
>> >
>> > 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.
>> >
>> > Correct.
>> >
>> > Chengxin narrowly answered your question 10 minutes before your email
>> [1].
>> >
>> > For that specific email [1], I can confirm that the "necessary but not
>> sufficient" interpretation of Chengxin is correct. I haven't explored
>> [Contrast-Policies] and have no answers to his questions. Maybe Markus can
>> answer those?
>> >
>> > I could not find GC-2 in Intra-handshake.fail paper [2]. This is again
>> conflating two very different things.
>> >
>> > Correct. GC-2 is in AsiaCCS paper [4] and orthogonal to the work in
>> ESORICS paper [2].
>> >
>> > ===
>> >
>> > On 20.08.26 17:11, Nathanael Ritz wrote:
>> >
>> > I ask that participants be patient while waiting for a direct
>> substantive response to the technical discussion at hand by the authors
>> themselves, please.
>> >
>> > I don't believe this is how participation in the IETF works. Writing a
>> research paper does not make the paper authors superior to any other WG
>> participant. The paper is just a contribution to the WG. Everyone has equal
>> right to speak. Unfortunately, the thread has gone very far from the
>> discussion points I was actually interested in [6,7]. But if I am the only
>> one interested in those questions, well I am fine with it but I do believe
>> we may keep talking past each other until we resolve those.
>> >
>> > Besides, both Songbo (to whom you are replying) and Chengxin (whose
>> email [1] he quoted) are co-authors with me in the draft [5] and have been
>> contributing to the follow-up research built on the same artifacts, and so
>> they are both more than capable of answering any technical question either
>> on paper or on ProVerif artifacts -- maybe currently even more than me
>> because I do not have full context of the discussion in the other thread
>> [1] in which they seem to be actively participating.
>> >
>> > Hope that helps.
>> >
>> > Best regards,
>> >
>> > -Usama
>> >
>> > [0]
>> https://mailarchive.ietf.org/arch/msg/seat/x3eQxFjQFJLceae6l4_NgXnmsDY/
>> >
>> > [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
>> >
>> > [3]
>> https://mailarchive.ietf.org/arch/msg/ufmrg/ZRhR7o1HrWxfGDfgRJMR65RBkDE/
>> >
>> > [4] https://doi.org/10.1145/3779208.3785387
>> >
>> > [5] https://datatracker.ietf.org/doc/draft-intra-handshake-fail/
>> >
>> > [6]
>> https://mailarchive.ietf.org/arch/msg/seat/6v_mzjg6dyv8QlHUFV13v-b8wFI/
>> >
>> > [7]
>> https://mailarchive.ietf.org/arch/msg/seat/tikYsd1RZbEhzFfute1GB5EJvGs/
>> >
>> > _______________________________________________
>> > Seat mailing list -- [e-mail]
>> > To unsubscribe send an email to [e-mail]
>>
> _______________________________________________
> Seat mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]
>