Formal analysis says early attestation is broken; its spec author says prove it

A formal takedown, with CVEs attached

Muhammad Usama Sardar of TU Dresden spent the autumn arguing that a core idea in confidential computing does not hold up, and this week he brought the argument to the IETF's Crypto Forum Research Group. The idea is early attestation, sometimes called intra-handshake attestation: proving that a TLS server is running inside a genuine, un-tampered trusted execution environment as part of the TLS handshake itself, rather than afterward. Sardar and his co-author modeled it in the formal-analysis tool ProVerif, checked three properties they call binding strength, server authentication, and compound authentication, and reported that each one fails in ways that permit cross-connection relay attacks and server impersonation.

The claim does not rest on theory alone. Over October, GitHub accepted seven security advisories the group filed against early-attestation code from Privasys and Edgeless Systems, issuing seven CVEs each rated 9.1 out of 10, and the CNA VulnCheck accepted an eighth against the Confidential Computing Consortium's Attestation SIG, also at 9.1. All of them now sit in the US National Vulnerability Database and the European EUVD. Sardar points to the fallout as corroboration: Privasys has moved to a post-handshake attestation proposal, the CCC Attestation SIG archived its early-attestation repository, and an earlier individual draft, draft-fossati-tls-attestation, was withdrawn. This outlet reported in October on the first wave of that work, which produced three CVSS-9-plus flaws against award-touted attested-TLS stacks. The new paper, which Sardar titled EarlyAttestationTschuss, a goodbye to early attestation, is the escalation.

The rebuttal: implementation bugs are not a broken design

The reception from the people who write the specification was not agreement. Thomas Fossati, the author of the draft at the center of the argument, and Nathanael Ritz, who has worked on the surrounding architecture, made the same core objection: a protocol specification cannot be disproved by implementations that ignore its mandatory requirements. In Ritz's framing, "a protocol specification cannot be invalidated by systems that fail to satisfy its normative requirements," and the CVEs, read one by one, are exactly such systems. The five Privasys relay CVEs, he noted, "affected code that bound only the TLS public key and an external challenge nonce into the attestation evidence, with zero session binding to the TLS connection." The CCC vulnerability hit "a historical proof-of-concept repository that had already been marked defunct." The diversion CVEs against Edgeless, Cocos AI, and Privasys were, in his account, authorization and allowlisting failures where a relying party accepted evidence from any unrevoked TEE without checking that it came from the right one.

Fossati's objection was more specific, and it went to the heart of what the formal model actually captured. The current draft, draft-fossati-seat-early-attestation-09, derives its attestation binder from the full TLS transcript running from ClientHello through ServerHello, and mixes in a hash of the server's public key. "So -09 binds to the transcript and to the public key," he wrote. "Binding to the transcript, in addition to the key, is what locks the Evidence to this connection." His conclusion was blunt: "if the model drops the key binding then it is not analysing -09."

The crux nobody can settle yet

This is where the dispute becomes genuinely unresolved rather than merely heated, and where both sides have a real point. Sardar answered that the model does not drop the key binding at all. The appearance that it did, he said, was a typo in his email, not in the paper: the modeled binder is the transcript hash concatenated with the ephemeral public key, documented as binder number eight in the paper's Tables 5 and 7, with the circular-dependency reasoning spelled out in its Section 6.1. If that is accurate, Fossati's central objection does not land, and the formal result stands against the current draft rather than only against legacy code.

The problem is that no one outside the authors can check it. The ProVerif model has not been released. Fossati, notably, did not declare the paper wrong; he reserved judgment. "I'll wait for the artefacts to be published, then, so that the assertions made in the paper can be checked. It's impossible to say anything more at this stage, as we don't have the full picture yet." Ritz made the same complaint from the other direction, that it is hard to evaluate "a pre-print" that "makes the assertions it does without a reproducible artifact to examine." So the decisive question, whether the formal model faithfully encodes the -09 binder or a weaker version of it, is answerable, just not today. Until the model is public, the defensible reading is narrow: the eight CVEs are real, third-party-validated, and sit against deployed implementations, while the larger claim that the design itself is broken is asserted by its authors and doubted by the draft's author, with the evidence to decide between them still unpublished.

Then it became an argument about AI

What might have stayed a technical standoff curdled into something else. Sardar announced that he would not engage with Ritz's messages because detector tools, he said, flagged them as almost entirely machine-written: "I refuse to engage with the RG participant below apparently using close to 100% AI-based responses according to GPTzero.me and Humalingo." His tell, he said, was a reply arriving within 47 minutes of a 44-page paper dense with mathematics, plus a reference to CVEs that neither the paper nor his email had mentioned.

Ritz did not deny using a model. He drew a line through the middle of it: "I used an LLM to scribe the email. The premise of the paper itself is already deeply contested in the SEAT WG... It's those topics and message which I used an LLM to sort and organize for me. However, the analysis is my own and I stand by it." A third participant, Islam Aboubakarov, pressed the same point from Sardar's side, calling several of the AI-assisted replies hallucinated. The exchange was by then running across at least two lists, CFRG and the Usable Formal Methods group, and it drew in Stephen Farrell, a former IETF security area director, who asked the parties to stop: "Can I ask that you take interpersonal disagreements off the list? This disagreement seems to be happening on multiple mailing lists and that isn't a good plan."

That subplot is not a sideshow to this publication's readers so much as a recurring motif. Recent coverage here has tracked the arrival of models as contributors to open-source projects, as the machine in the middle of review, and most recently as the thing dismantling a national cryptography competition's first round in an afternoon. The attestation fight adds a new variant: not a model finding a bug or writing a patch, but a model standing in for a human reviewer, and a researcher refusing to treat that as engagement at all. Whether a terse, possibly AI-organized review counts as a real objection is now part of the technical argument, not separate from it.

Why it matters

Confidential computing sells itself on a single promise, that a remote party can verify what is running inside a sealed enclave before trusting it with data, and attested TLS is how that promise reaches the wire. If early attestation is salvageable, the current draft is worth finishing. If it is structurally unable to bind an enclave's identity to a specific connection, then a line of products and open-source stacks is building on sand, and the move several projects have already made toward post-handshake attestation is the safer bet. The honest status at this moment is unsatisfying but real: the implementation-level failures are documented and severe, the design-level verdict is contested by the people best placed to render it, and the artifact that would settle the question is still, as of this writing, unpublished.