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

[Songbo Bu <[e-mail]>]

Hi all,

I agree with the clarifications in Usama's message. The question is
not whether a modified construction can satisfy selected correlation
properties under its own assumptions. My question was whether a hybrid
intra- and post-handshake design establishes a specific security
property that post-handshake attestation alone cannot establish.

The public artifact separates three correlation goals: Evidence with
the DH shared secret (G1), the client handshake traffic key (G2), and
the client application traffic key (G3). It shows that its proposed
intra-handshake construction establishes G1 and G2 but not G3. The
artifact does not model a hybrid design against a post-handshake-only
baseline, so it does not demonstrate a hybrid-over-post separation.

For that reason, I think a claimed counter-example should state:

1. the exact property satisfied by hybrid but not post-only;
2. the identical adversary, trust, and deployment assumptions under
which both are compared;
3. the exact statement in Section 9 that the result contradicts; and
4. the endpoint events and correspondence query used to establish the
separation.

Without that separation, changing the construction may still produce a
useful design, but it does not answer the question I posed. It also
leaves the additional intra-handshake machinery—Evidence availability
during the handshake, interaction with transcript and key state, new
failure paths, and implementation burden—without a demonstrated
security benefit over post-handshake attestation alone.

I also agree that two questions should be evaluated separately from
symbolic equality. Placing an infrastructure public key or identity in
signed report data does not by itself prove possession of the
corresponding private key. Reusing TLS-derived traffic keys for
another purpose also needs an explicit key-separation and
computational-security justification. These questions are not settled
merely because a symbolic model can express an equality.

This does not rule out operational reasons for a hybrid design. It
asks that operational motivation be separated from the claimed
security property, and that the latter be stated in a form that can be
formally verified. ProVerif code is never wired up in real
implementations.

On Tue, 28 Jul 2026 15:37:02 -0600, Nathanael Ritz <[e-mail]> wrote:
> Top posting. It appears I have been asked to set aside falsifiable formal analysis effort or to suggest that such work is itself unfalsifiable. While that may or may not be true, I believe this thread has truly run its course.
>
> Sincerely,
>
> Nathanael
>
> On Tue, 28 Jul 2026 at 14:37, Muhammad Usama Sardar <[e-mail]> wrote:
>
> Hi Nathanael,
>
> Markus kindly clarified what he would like to see in more detail.
> Could you please do the same to help keep this discussion more
> focused? Here is my understanding of the points where you
> disagree:
>
> - While the paper [6] claims it 'may not be possible' to achieve
> level 3 binding in intra-handshake attestation, you believe it
> is possible. Setting aside what you model and prove is correct
> or not, I don't see how this contradicts the claim 'may not be
> possible' in the paper.
>
> - We haven't yet seen a property that the hybrid construction

> (intra- + post-handshake attestation) can satisfy, but
> post-handshake attestation alone cannot satisfy, unless
> you are implicitly implying that level-3 binding cannot be
> achieved by post-handshake attestation. Please clarify
> explicitly.
>
> Is there something I have missed? As mentioned before to Markus,
> I believe it is much more organized to have them answered in
> detailed technical report. So more important than the discussion
> below is the correction/addition/edits in above statements.
>
> Also, I believe it will be more constructive to respond point by
> point to [5] where you disagree, so we can do further working to
> share with the WG/RG.
>
> We will then work on it and share with the WG/RG.
>
> On 28.07.26 20:51, Nathanael Ritz
> wrote:
>
> On Tue, 28 Jul 2026 at
> 10:00, Muhammad Usama Sardar <[e-mail]>
> wrote:
>
> This does not address any of the questions in [5]
> where your working was shown to be not correct, and
> these inaccuracies still remain here too.
>
> [NR}: I disagree, but the authors are welcome to cite
> my work and my words directly in relationship to any
> questions that are, in their opinion, left unanswered so
> that I can address them directly rather than guessing.
>
> For example, our responses to your #2 in [5].
>
> For clarity, nothing has changed in the key schedule
> of TLS 1.3 for quite long time (I think draft-20 which
> became RFC8446). Saying that RFC9846 is "new work" for
> key schedule is almost surely wrong. Maybe Ekr can
> confirm.
>
> [NR]: If it is being stated that I am suggesting
> RFC9846 includes 'new work for key schedule', please quote
> me directly, as I am currently unclear to what context and
> statements are being referenced to right now.
>
> Thanks for clarifying. 'non-conformant Key Schedule' and then
> mention of RFC 9846 §7.5 was unclear for #2 in [5]; it has stayed
> the same for pretty much a decade. We believe that both points in
> your #2 about key schedule are not valid and we justified it
> technically in [5], to which we have seen no response.
>
> Best regards,
>
> Usama, Slava, and Jean-Marie
>
> [5] https://mailarchive.ietf.org/arch/msg/seat/dKVqaL8RJSQLonIEmtzrDYEXEAU/
>
> [6] https://www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS