[Ufmrg] Re: EarlyAttestationBleed: Three Critical-severity Vulnerabilities of CVSS ≥ 9.0 in Confidential Computing

[Songbo Bu <[e-mail]>]

Hi Waqas,

Thank you for clarifying. You are right: I should have said “make it
explicit,” not “more visible.” We will explicitly identify the contribution
of Section 7 in Section 1.1 and add a dedicated subsection on
implementation complexity, as you suggest.

Your implementation experience gives that discussion a concrete focus:
avoiding the attestation-specific changes to the TLS handshake that you
previously needed. We will distinguish the integration and maintenance
costs avoided from the attestation responsibilities that remain, including
evidence validation, channel binding, and re-attestation. Thank you also
for highlighting the MITRE framework, which we cite in our paper. Your
example helps connect it to this discussion.

On ProVerif, changing the event arguments can legitimately change the
result, because it can change the security property being checked. That
difference alone does not establish whether the generated ProVerif model is
correct.

A useful starting point is to state the intended authentication claim in
plain language: who is authenticating whom, and on which values must they
agree? The event arguments should capture those identities and values.
Injectivity additionally requires a distinct matching peer-event occurrence
for each acceptance.

Section 6.2 of [1], particularly Section 6.2.2 on event arguments,
addresses this question directly. It discusses how parameter choices affect
correspondence queries, while Section 6.2.3 discusses event placement. I
would use the intended claim to guide those choices, rather than adjust the
arguments simply to obtain a successful proof.

Best regards,
Songbo Bu

[1] Muhammad Usama Sardar, Mariam Moustafa, and Tuomas Aura. *Identity
Crisis in Confidential Computing: Formal Analysis of Attested TLS*. ASIA
CCS 2026. DOI: 10.1145/3779208.3785387.