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

[Iman Schrock <[e-mail]>]

SEAT colleagues,

I hope all is well.

I and my team EMILIA have now finished review of the paper and
independently executed the disclosed
`intra-handshake.fail` artifacts from Muhammad Usama Sardar,
Viacheslav Dubeyko and
Jean-Marie Jacquet. I appreciate the level of depth of key schedule in
it and agree with their
results and the clarifications they have provided on list.
The acknowledgement of vulnerabilities by the implementers is
sufficient on its own.
I believe their work deserves focused SEAT and implementation
community attention because it addresses a practical gap between proving that
a workload is attested and proving that the attestation is bound to the exact
application traffic a relying party is about to trust.

In plain language, remote attestation can establish that approved software is
running in an expected environment, while TLS can establish an encrypted
connection. Sardar and his co-authors ask the additional question: is the
attestation cryptographically correlated to the correct stage of that same
connection, strongly enough to prevent an attacker from relaying or
substituting traffic? Their analysis distinguishes correlation to shared DH
secret (G1), handshake traffic secret (G2), and application traffic
secret (G3), then
tests seven intra-handshake binding mechanisms and a proposed mitigation under
a well-defined and explicit system and threat model.

This matters beyond one TLS draft, two SEAT drafts and the
implementations considered in the paper. Confidential-computing
systems, enclave
services, cloud control planes, and AI agents increasingly use attestation as a
basis to trust sensitive requests. A valid attestation result is not enough if
the relying party cannot tell whether it is bound to the application traffic
secret that will actually protect the consequential secrets and
actions. In healthcare, financial,
government, and enterprise automation, that distinction can determine whether
an apparently verified workload is permitted to influence a real system.

The authors also deserve recognition for the patience with which they
handled the work. Their
public timeline documents sustained responsible disclosure and engagement with
affected implementers and standards participants before broad publication.
They published formal models, code, logs, and a detailed record after a
prolonged and uneven community response over ten months. That
transparency and professionalism of authors made external
scrutiny possible and reduced the risk of turning a serious security finding
into an unsupported public claim.

For my review, I pinned the upstream repository at commit
`8275cc613d7724d21c5353374020e275d3edd7ef` and executed it outside the
authors' environment using ProVerif 2.05. All eight upstream executions
completed, produced all 16 query results, and reproduced the authors' published
G1/G2/G3 table: mechanisms 1, 2, 4, and 6 returned
`false/false/false`; mechanisms 3, 5, and 7 returned
`true/false/false`; and the proposed mitigation returned
`true/true/false`. This is an independent reproduction of the disclosed model
outputs.

The extensibility of the models allows the community to develop and check the
the assurance level achieved.
That is the narrow connection to EMILIA. EMILIA takes security seriously and
requires level-3 binding for secure operation.

EMILIA team agrees with all of the authors' clarifications on the
list. For example, there is a very crucial distinction between
handshake secret and handshake traffic secret and that
proof-of-possesion of both `EK` and `LTK`
are required to avoid diversion attacks. Cryptographic separation is
well-known and reuse
of keys for multiple purposes creates cryptographic problems and such problems
do not show up in abstract ProVerif analysis. ProVerif code is never wired up in
real implementations. Authors are correct that using standard
exporters of RFC9846 in
intra-handshake makes no sense and that early_exporter_secret `ems0`
is unrelated to the standard exporter.
Regardless of whether the handshake is PSK or not, PSK input in the
key schedule remains.
Nothing has changed in the key schedule of TLS 1.3 for about a decade.

All affected implementers have acknowleged the attacks.
I therefore support the claims in the disclosed paper, models, and
attack traces.

The authors' contribution is important because it asks the question
industry too often
skips: not only "was something attested?" but "what exact traffic and later
consequence may that attestation truthfully support?"

Moving forward, I would like to see an answer to Songbo's question:
which specific security property in ProVerif hybrid construction can
satisfy that post-handshake alone cannot satisfy? Drastically changing
the model to satisfy the same properties does not settle this
question. It seems trivial in post-handshake to achieve level-3
binding.

Best,
Iman Schrock
Founder, EMILIA Protocol
emiliaprotocol.ai