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

[Song Haowen <[e-mail]>]

Dear Usama, Slava and Jean-Marie,

One point in your paper that I find especially useful is the way it cleanly
separates trust in an attested TLS connection into different binding
levels. From a relying party’s perspective, there is a real difference
between Evidence that is only related to early handshake material, Evidence
that reaches the handshake traffic-key level, and Evidence that is
correlated with the application-traffic key that will protect the user’s
data. That distinction makes the paper’s result important.

I also think the result is strong because the analysis is not limited to
abstract protocol sketches. It considers real-world intra-handshake
attestation mechanisms and production implementations, and then evaluates
them through explicit correlation properties. That is the right way to
handle this problem scientifically. When TLS and remote attestation are
composed, intuitive protocol reasoning may be too weak; the security claim
has to be stated as a property and checked against a realistic
relay-adversary model.

I strongly support the results of the paper. Even if the community later
refines parts of the model or the mitigation, the current result is already
valuable because it identifies the kind of binding property that future
attested TLS work needs to satisfy.

Thanks
Haowen Song

On Tuesday, July 7, 2026, Chengxin Huang <[e-mail]> wrote:

> Hello everyone,
>
> After careful review, I would like to express strong support for the main
> results of the Intra-handshake.fail paper and for considering its
> accompanying code artifacts as substantive technical input for SEAT and
> UFMRG.
>
> The result I find most important is that the security of intra-handshake
> attestation cannot be judged only by whether Evidence is carried during the
> TLS handshake. The central question is that how strongly Evidence is bound
> to the same TLS connection whose keys will protect the later application
> traffic. This is a protocol-level issue, and it is directly relevant to how
> SEAT evaluates candidate mechanisms for attested TLS.
>
> The paper's analysis of binding levels is especially useful. It connects
> the Evidence to different stages of the TLS key schedule and explains why
> some seemingly natural binding materials are not sufficient against relay
> attacks. In my view, this gives the WG a concrete basis for discussing the
> paper's result instead of relying only on intuitive message-flow arguments.
>
> I also support the methodological direction of the paper. For work that
> adds attestation-related logic to or around the TLS handshake, explicit
> security properties and reproducible formal artifacts are the right way
> forward. Authors make it possible for the community to inspect assumptions,
> test claims, compare mitigations, and improve the design on a scientific
> basis.
>
> This work is also relevant to UFMRG. It is a practical example of applying
> formal analysis to an active IETF protocol-standardization problem. The
> paper and code can help both the standards community and the formal-methods
> community understand how formal models can be used in real protocol work,
> including where such models are strong and where further analysis may still
> be needed.
>
> For these reasons, I strongly support the analysis of the paper and
> support treating the paper and code as important technical input for
> further SEAT and UFMRG review and refinement, as we move forward.
>
> Best regards,
> Chengxin Huang
>
> On Mon, Jul 6, 2026 at 11:17 PM Steve <[e-mail]> wrote:
>
>> Dear all,
>>
>> I am Research Analyst at Cloud Security Alliance (CSA-GCR).
>>
>> Because of highly severe attacks, the intra-handshake.fail paper deserves
>> close attention from the SEAT WG, UFMRG and the related research community.
>> From a Cloud Security Alliance community and cloud-security industry
>> perspective, I strongly support bringing the paper and its supporting
>> open-source code into the WG/RG discussion.
>> Cloud and confidential-computing deployments rely on attestation
>> mechanisms that can be implemented, audited, and operated at scale. In this
>> setting, a protocol extension that adds intra-handshake attestation
>> behavior affects more than message syntax. It affects implementation
>> assurance, conformance testing, incident response, certification, and
>> enterprise risk acceptance.
>>
>> The paper is therefore important industry input because it connects a
>> concrete protocol-design question with formal analysis, relay-attack risk,
>> and production implementation impact. Its treatment of binding mechanisms
>> gives cloud providers, enterprise relying parties, security vendors, and
>> governance teams a sharper basis for judging whether a proposed attestation
>> transport path delivers security value proportionate to its operational
>> complexity.
>>
>> I strongly support using the Intra-handshake.fail paper and code as a
>> reference point for further SEAT and UFMRG discussion, and I encourage
>> review by WG participants, UFMRG experts, confidential-computing
>> implementers, and cloud-security stakeholders.
>>
>> Best regards,
>> Steve Luo
>> Research Analyst, Cloud Security Alliance (CSA-GCR)
>>
>> Songbo Bu <[e-mail]> 于2026年7月6日周一 22:18写道：
>>
>>> 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
>>>
>>>> _______________________________________________
>>> 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]
>>
>