MIME-Version: 1.0
References: <4b968f77-631e-4d26-a86d-280dd9aee66e@tu-dresden.de>
 <1790524983056529169.1790524983@vision4d.ai>
 <CAK08nYazr3T2D4K1FgmSepxrECH2RaLNWiFpQX5VXNA-Xz-yNQ@mail.gmail.com>
 <1790604283057408440.1790604283@vision4d.ai>
In-Reply-To: <1790604283057408440.1790604283@vision4d.ai>
From: Songbo Bu <bluedognull@gmail.com>
Date: Tue, 29 Sep 2026 00:16:14 +0800
Message-ID: 
 <CAK08nYYLYWV6sJb4aCj0o9HCgtN4yENZ1JQVB7TcjbPGvadF6w@mail.gmail.com>
To: waqas.nawaz@vision4d.ai
Content-Type: multipart/alternative; boundary="0000000000003d0929065c8d637d"
Message-ID-Hash: FU5YXWNMTIQXYZFXLSKHURQO3LQQC5WS
CC: ufmrg@irtf.org
Precedence: list
Subject: [Ufmrg] =?utf-8?q?Re=3A_EarlyAttestationBleed=3A_Three_Critical-severity_Vul?=
	=?utf-8?q?nerabilities_of_CVSS_=E2=89=A5_9=2E0_in_Confidential_Computing?=
Archived-At: 
 <https://mailarchive.ietf.org/arch/msg/ufmrg/_Jyk7JiwKmJUgIYfL4vAZhboXDs>

--0000000000003d0929065c8d637d
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Hi Waqas,

Thank you for clarifying. You are right: I should have said =E2=80=9Cmake i=
t
explicit,=E2=80=9D not =E2=80=9Cmore visible.=E2=80=9D We will explicitly i=
dentify 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.

--0000000000003d0929065c8d637d
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><p>Hi Waqas,<br><br>Thank you for clarifying. You are righ=
t: I should have said =E2=80=9Cmake it explicit,=E2=80=9D not =E2=80=9Cmore=
 visible.=E2=80=9D We will explicitly identify the contribution of Section =
7 in Section 1.1 and add a dedicated subsection on implementation complexit=
y, as you suggest.<br><br>Your implementation experience gives that discuss=
ion a concrete focus: avoiding the attestation-specific changes to the TLS =
handshake that you previously needed. We will distinguish the integration a=
nd maintenance costs avoided from the attestation responsibilities that rem=
ain, including evidence validation, channel binding, and re-attestation. Th=
ank you also for highlighting the MITRE framework, which we cite in our pap=
er. Your example helps connect it to this discussion.<br><br>On ProVerif, c=
hanging 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.<br><br>A use=
ful starting point is to state the intended authentication claim in plain l=
anguage: who is authenticating whom, and on which values must they agree? T=
he event arguments should capture those identities and values. Injectivity =
additionally requires a distinct matching peer-event occurrence for each ac=
ceptance.<br><br>Section 6.2 of [1], particularly Section 6.2.2 on event ar=
guments, addresses this question directly. It discusses how parameter choic=
es affect correspondence queries, while Section 6.2.3 discusses event place=
ment. I would use the intended claim to guide those choices, rather than ad=
just the arguments simply to obtain a successful proof.<br><br>Best regards=
,<br>Songbo Bu<br><br>[1] Muhammad Usama Sardar, Mariam Moustafa, and Tuoma=
s Aura. *Identity Crisis in Confidential Computing: Formal Analysis of Atte=
sted TLS*. ASIA CCS 2026. DOI: 10.1145/3779208.3785387.</p>
</div>

--0000000000003d0929065c8d637d--