[Ufmrg] Observations on Formal Analysis Methodology for Relay Attacks in Intra-handshake Attestation for Confidential Agentic AI Systems

[Nathanael Ritz <[e-mail]>]

Dear UFMRG,

I understand that participation in this RG is minimal, and I often feel
that contributions here are directed toward a rather limited audience.
Nevertheless, while I've shared plenty directly with SEAT WG (cross-posted
to this RG list already), I am directing these comments directly to this RG
because they focus on my reading of the UFMRG charter. Specifically, this
recent output feels in tension with what reads to me as the original
ambition of this group.

The UFMRG charter emphasizes exploring the strengths and limitations of
formal methods and understanding how they intersect with the
consensus-building process. I believe this recent paper offers a practical
illustration of how the alignment between a formal model’s automated
output, its textual explanation, and its summarized presentation can, in my
opinion, visibly conflict with the stated goals of the community.

### 1. Alignment Between Witness Traces and Textual Rationale

Section 7.1 of the paper attributes the failure of the early exporter
(Mechanism #3) to a structural protocol gap, stating that because there is
no contribution from the server, an adversary can relay exp0, the Early
Exporter.

However, the corresponding ProVerif logs indicate that the counterexample
generated for the reported G2 failure is not a structural relay attack. The
specific witness trace relies on a cryptographic downgrade, requiring the
adversary to force a weak Diffie-Hellman group and a bad element
(`event(ServerChoosesKEX(cr',sr',DHE_13(WeakDH,badEl)))`). My concern is
not that the model permits this attack, but that there appears to be a
divergence between the structural explanation presented in the natural
language prose and the specific execution path produced by the verification
tool.

### 2. Behavior Under Standard Cryptographic Assumptions

In Sections 6.1 and 6.4, the authors define "Assumption 1", which
explicitly conditions the equivalence of connection keys on the absence of
weak cryptographic primitives and leakages.

When the native ProVerif queries are constrained to exclude these downgrade
paths, aligning with the Standard Cryptographic Assumptions described
earlier in the paper, the analytical output changes. In every evaluated
binding mechanism I have re-examined so far that achieves G1 (Mechanisms
#3, #5, and #7), G2 and G3 also evaluate to true.

I have generated and compiled the logs demonstrating this exact behavior
for Mechanism #3 here:

https://raw.githubusercontent.com/nathanaelritz/gists/refs/heads/main/log-binder3-cve.txt

If the authors have found a specific instance where a G1 binder fails at G2
or G3 without relying on weak cryptographic primitives or leakages, that
would be a highly interesting scientific result. However, that is not what
the current analysis demonstrates, as I understand it from the published
model and my reproductions. There is a reason why Gx and Gy can travel
unauthenticated safely before the TLS 1.3 CertificateVerify message and
Finished MAC binder are compared.

### 3. Concerns Regarding Consensus Building

Table 4 of the paper records the verification results as a binary pass/fail
grid, reporting failures for G2 and G3. This presentation does not
distinguish between inherent protocol-level binding flaws and failures that
depend upon the downgrade and weakness assumptions introduced into the
threat model.

When the paper's own authors admit that very few people are capable of
understanding the formal analysis source [*], I believe this presentation
introduces a significant risk of undue ambiguity into the consensus
process. It obscures the boundary conditions of the tool's findings and
requires standards engineers to manually audit the formal codebase to
identify the root cause of the reported vulnerability.

Respectfully sent,
Nathanael

[*] https://mailarchive.ietf.org/arch/msg/seat/-dG-IJtKTNQ5pds2ZDTWvprQ1kQ/

On Mon, 29 Jun 2026 at 17:12, Muhammad Usama Sardar <
[e-mail]> wrote:

> Hi SEAT and UFMRG,
>
> In line with the SEAT charter (cf. emphasis in the email below), we would
> like to share our contribution, namely detailed technical report [11] of
> shared ProVerif artifacts [10] for intra-handshake attestation. In
> particular, the new contribution is a paper-and-pen proof in [11].
>
> The vulnerability in intra-handshake attestation was responsibly disclosed
> -- as noted in [12] -- to the vendors, which resulted in CVE
> (CVE-2026-33697) of CVSS 7.5 [13]. We highly recommend that developers and
> maintainers in the WG/RG pay special attention and move from
> intra-handshake attestation to post-handshake attestation [15]; since to
> our knowledge, it is one of the highest scored vulnerabilities in
> confidential computing literature [14].
>
> Also, please see one small update and one reference inline below.
>
> Hope this contribution answers some of the questions posed.
>
> We welcome any constructive and technical feedback, suggestions or
> questions from the WG/RG and will be happy to answer those or address those
> in our ongoing work. We also warmly welcome future collaborators moving
> forward.
>
> Best regards,
>
> Usama, Slava, and Jean-Marie
>
>
>
> On 26.06.26 00:18, Muhammad Usama Sardar wrote:
>
> Hi SEAT and UFMRG,
>
> In line with the SEAT charter (*emphasis* our own):
>
> The working group will engage with the research community on the
> evaluation and formal analysis of the protocol artifacts *in parallel*
> with the specification work.
>
> and the required property in the SEAT charter (*emphasis* our own):
>
> The attested D(TLS) protocol extension will also describe a minimum
> subset of properties that the attested state must convey in order
> to *bind the Evidence* and Attestation Results *to the TLS connection*.
>
> we (I, Slava, and Jean-Marie) would like to share the concrete technical
> results for binding mechanisms of the intra-handshake attestation from our
> formal analysis in ProVerif [10]:
>
>
>    1. All analyzed binding mechanisms and the corresponding
>    implementations of intra-handshake attestation are vulnerable to relay
>    attacks.
>    2. Early exporter helps achieve level 1 binding.
>    3. Our proposed mechanism helps achieve level 2 binding.
>    4. It may not be possible to achieve level 3 binding in
>    intra-handshake attestation alone.
>    5. The research suggests that more recent proposals
>    draft-fossati-seat-early-attestation and draft-ritz-seat-facts add
>    complexity of intra-handshake attestation relative to
>    draft-fossati-seat-expat without offering additional security benefits.
>
> s/add/may add unnecessary
>
>
>
> To support independent review, further research and development by the
> RG/WG, we have released the ProVerif artifacts [10] under Apache-2.0
> License. We hope these artifacts provide useful input for SEAT.
>
> There is also a paper-and-pen proof in the corresponding paper supporting
> the above results, which we will share soon with the WG/RG.
>
> Please see Sec. 6.4 of [11].
>
> We welcome any constructive and technical feedback from the WG/RG and will
> be happy to address it.
>
> Best regards,
>
> Usama, Slava, and Jean-Marie
>
>
> On 03.03.26 18:47, Muhammad Usama Sardar wrote:
>
> Hi all,
>
> Following up with supporting public evidence: *Cocos AI has publicly
> acknowledged [9]* the relay attacks last Friday.
>
> # *Context*
>
> As helpful context, Cocos AI [4] claimed their attested TLS to be the
> "best in the world" in the Confidential Computing Consortium and despite we
> having informed them repeatedly about the attacks after our formal
> analysis, they were continuing to misguide the community on social media.
> Anyway, we now respect their honesty and transparency, and we remain fully
> committed to helping them towards secure solutions.
>
> # *Cocos AI acknowledgment of attacks*
>
> Cocos AI (one of the implementers of the protocol) has publicly
> acknowledged [9] our email and the relay attacks we highlighted on their
> design and implementation in our email. Particularly, see the sections
> "Limitations and the Relay Attack" and "The Relay Attack Scenario" in [9].
> Note that their description is almost a paraphrase of our email. There are
> some nits that we disagree with them but that doesn't matter much. They
> have essentially acknowledged the attacks and shared a short-term,
> medium-term and long-term roadmap for mitigations of the attacks. We
> believe this alone is sufficient supporting evidence.
> Best regards,
> Usama, Slava (Viacheslav), and Jean-Marie
>
> On 11.01.26 02:17, Muhammad Usama Sardar wrote:
>
> Hi SEAT and UFMRG,
>
> # *Context*
>
> We (i.e., I, Dr. Viacheslav Dubeyko [IBM], and Prof. Jean-Marie Jacquet
> [University of Namur]) did an extensive exploration of binding mechanisms
> in intra-handshake attestation for confidential agentic AI systems, that
> was presented on mic at SEAT meeting 124 and later submitted as a draft [0]
> with focus on AI agent. In line with the scope of SEAT charter, we also did
> formal analysis in state-of-the-art tool ProVerif and we would like to
> share a summary of our findings from our formal analysis with the hope that
> the analysis provides important data points to WG for making informed
> decisions.
>
> # *Key Finding*
>
> *All* analyzed binding mechanisms and implementations are ad-hoc and *all*
> of them result in relay attacks.
>
> Please note that this includes Meta's AI [1] for which a thorough security
> assessment [2] was carried out by *Trail of Bits* and they were unable to
> capture the relay attacks but as kindly clarified by Tjaden Hess, no formal
> methods were used in their review process. Our analysis shows the value of
> formal methods in the review process.
>
> # *Fundamental Issue*
> Basically, there is no binding of Evidence to the TLS connection in all of
> these implementations.
>
> # *TEE-agnostic System Model*
>
>    - Layered Attester (e.g., Intel TDX)
>    - Composite Attester (e.g., Arm CCA)
>
> # *Scope of Attested TLS*
>
>    - Intra-handshake attestation
>
> # *Formalization Approach*
>
>    - Symbolic security analysis
>
> # *Formalization Tool*
>
>    - ProVerif
>
>
> # *Binding Mechanisms*
>
> *A*. We considered the following values for user-defined field "rdata" in
> TEEs
>
>    1. Client's TLS nonce
>    2. Client's Attestation nonce
>    3. Early exporter
>    4. (Hash of) Server's public key
>
> *Question for WG/RG*: Is someone aware of any other value that folks use
> in "rdata"? If possible, please share a link to specification and/or
> implementation together.
> *B*. Combinations:
> We considered the following combinations of binding mechanisms from *A*:
>
>    1. Hash (Client's TLS nonce || Server's public key)
>    2. Hash (Client's Attestation nonce || Server's public key)
>
> *Question** for WG/RG*: Is someone aware of any other combination that
> folks use in "rdata"? If possible, please share a link to specification
> and/or implementation together.
>
>
> # *Prominent Industrial Implementations*
>
>    1. Edgeless Systems Contrast [3]: uses binding mechanism *B*.2
>    2. Cocos AI [4]
>    3. CCC proof-of-concept [5]: Implementation of
>    draft-fossati-tls-attestation
>    4. Meta’s AI [1]: uses binding mechanism *A*.1
>
> *Question** for WG/RG*: Is someone aware of any other intra-handshake
> attestation implementation? If possible, please share a link to
> specification and/or implementation together.
>
>
> # *Binding Levels*
>
>    1. Shared DH secret (g^xy)
>    2. Client's handshake traffic key (htsc)
>    3. Client's application traffic key (atsc)
>
>
> # *Correlation Properties*
>
>    - G1: Correlation of Evidence to Shared DH Secret
>    - G2: Correlation of Evidence to Client’s Handshake Traffic Key
>    - G3: Correlation of Evidence to Client’s Application Traffic Key
>
>
> # *Results*
>
> We proved the proposition: G3 => G2 => G1
>
> We discovered relay attacks in all above proposals for binding mechanisms
> as well as all implementations analyzed. We provide a formal proof of
> insecurity that all above binding mechanisms and implementations fail to
> even achieve G1 property (Level 1 binding).
>
> Any binding that involves server's public key needs additional assumption
> that server's private key does not leak.
>
> In general, all solutions fail when server's private key is leaked. In
> other words, extension of TLS with attestation in these implementations is
> not really bringing much benefit from a security perspective and rather
> giving a false sense of security.
>
> We believe that it is not possible to achieve level 3 binding for
> intra-handshake attestation within the scope of SEAT charter.
>
>
> # *Implementation Issues*
>
>    - Meta's AI uses client's TLS nonce (instead of attestation nonce),
>    and hence does not provide Evidence freshness.
>    - Cocos AI abuses the SNI extension to convey attestation nonce.
>    - Edgeless Systems Contrast was abusing the SNI extension to convey
>    attestation nonce, and currently abusing the ALPN extension to convey
>    attestation nonce.
>
>
> # *Proposed Mitigation*
>
>    - We propose a cryptographic binder and modify CertificateVerify
>    message, which achieves level 2 binding.
>
>
> # *Paper and Artifacts*
> A paper draft has been prepared and artifacts are well-documented. If you
> are interested in reviewing one/both of them and can provide some feedback
> until 19th Jan, please reach out to me off-list. If someone can
> substantially improve the paper and/or artifacts, we are very welcoming to
> adding you as co-author. We will make the paper and artifacts public later
> on.
>
>
> # *Contributors*
> We thank Juho Forsén, Mariam Moustafa, Markus Rudy, Tjaden Hess, Yuning
> Jiang, and Pavel Nikonorov for sharing their insights and providing
> valuable feedback.
>
>
> # *Other known related implementations*
>
>    - Attested EDHOC: Our intuition (no formal proof yet) is that the
>    attacks should apply to attested EDHOC protocol in intra-handshake
>    attestation [6] as well -- at least for the case of Responder as Attester.
>    We will reach out to LAKE WG to inform them about these attacks.
>    - Attested Noise: Confer's private inference [7] uses binding
>    mechanism *A*.4 [8] for Noise protocol. This implementation started
>    just 3 weeks ago (with holidays in between) and is not mature yet. Anyway,
>    we will reach out to the implementer (Moxie Marlinspike) to inform him
>    about these attacks.
>
>
> # *Feedback/Ideas*
> We believe that we have explored all options in intra-handshake
> attestation within the scope of SEAT charter. We look forward to your
> thoughts and ideas on how we can mutually progress this work forward.
>
> -Usama
>
> [0] https://datatracker.ietf.org/doc/draft-jiang-seat-dynamic-attestation/
>
> [1]
> https://ai.meta.com/static-resource/private-processing-technical-whitepaper
>
> [2]
> https://github.com/trailofbits/publications/blob/master/reviews/2025-08-meta-whatsapp-privateprocessing-securityreview.pdf
> [3]
> https://github.com/CCC-Attestation/meetings/blob/main/materials/MarkusRudy.contrast-atls-ccc-attestation.pdf
>
> [4] https://docs.cocos.ultraviolet.rs/atls
>
> [5] https://github.com/ccc-attestation/attested-tls-poc
>
> [6] https://datatracker.ietf.org/doc/draft-ietf-lake-ra/
>
> [7] https://confer.to/blog/2026/01/private-inference/
>
> [8]
> https://github.com/ConferLabs/confer-proxy/blob/0f69f522f7597c6587741055e86ae802c10891ab/src/main/java/org/moxie/confer/proxy/attestation/AttestationService.java#L145
>
> [9]
> https://web.archive.org/web/20260227160554/https://www.ultraviolet.rs/blog/tee-tls-privacy/
>
> [10] https://github.com/CCC-Attestation/formal-spec-KBS
>
> [11]
> https://www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS
> [12]
> https://github.com/ultravioletrs/cocos/security/advisories/GHSA-vfgg-mvxx-mgg7
>
> [13] https://www.cve.org/CVERecord?id=CVE-2026-33697
>
> [14]
> https://github.com/CCC-Attestation/formal-spec-KBS#comparison-with-other-vulnerabilities-in-confidential-computing-literature
>
> [15] https://datatracker.ietf.org/doc/draft-fossati-seat-expat/
> _______________________________________________
> Seat mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]
>