[Ufmrg] Re: [Seat] Comments on formal analysis of relay attacks in intra-handshake attestation (CVE-2026-33697)

[Songbo Bu <[e-mail]>]

Hi Usama, Slava, Jean-Marie, all,

Based on my participation in the related research discussions, I appreciate
sharing Intra-handshake.fail paper and code with the WG/RG and strongly
support using them as important technical input for the ongoing SEAT
discussion.

The paper and code is valuable because it makes the discussion more
property-driven. In particular, I think the WG should explicitly examine
what security property a hybrid intra-handshake plus post-handshake
attestation design can satisfy that post-handshake attestation alone cannot
satisfy. This question is independent of any particular specification
proposal, and it is important for evaluating whether additional
intra-handshake complexity is technically justified.

I also support the paper’s narrower focus on intra-handshake attestation.
Keeping the analysis scoped in this way avoids conflating different
attestation models and allows the WG/RG to reason more precisely about
binding mechanisms, relay attacks, and the relationship between Evidence
and the TLS connection.

>From WG charter perspective, the paper is useful because it gives the
community a concrete object to review, challenge, reproduce, and improve.
This is especially important where formal models, protocol state-machine
changes, and production implementations intersect.

It helps bring the standards community and formal methods researchers
closer to share experience and ideas and provides UFMRG a concrete
methodology for protocol analysis of AI agents.

For these reasons, I strongly support sharing this paper and code with the
WG/RG and encourage review from SEAT WG participants and UFMRG
formal-methods experts.

Best regards,
Songbo Bu

>