[CFRG] Re: Stop Calling Them Provers: The Case for Calling ProVerif and Tamarin Symbolic Protocol Analyzers

[Nathanael Ritz <[e-mail]>]

Hi Songbo,

Changing the timing of remote attestation (i.e., from intra- to post-) does
not provide the required mitigations. The required mitigations are
available through strict fail-closed semantics, ensuring per-connection
freshness and binding the RATS Evidence to the TLS connection. This can be
done entirely without overhauling an existing implementation.

On Wed, 4 Nov 2026 at 03:19, Songbo Bu <[e-mail]> wrote:

> Keys earlier than application traffic keys do not establish the
> cryptographic properties required for security
>

You seem to be conflating "keys" with RATS Evidence here. Setting formal
verification aside entirely, your claim appears to misunderstand standard
TLS 1.3 protocol architecture. Any difference in threat models does not
change this diagnostic, as the claim concerns the underlying protocol
mathematics. TLS 1.3 always authenticates earlier handshake states
retroactively.

To elaborate: ephemeral key-exchange parameters (such as DH shares g^x and
g^y, or KEM public keys and ciphertexts) are transmitted entirely
unauthenticated in ClientHello and ServerHello—long before application keys
exist. Yet the resulting shared secret (kem_ss / g^xy) and ephemeral keys
are understood to be secure because CertificateVerify retroactively signs
the cumulative transcript, and the Finished MACs authenticate it.

This is how it works with the intra-handshake (early) attestation protocol
under discussion:

1. Binder Derivation: The server computes the binder over the
`ClientHello...ServerHello` transcript checkpoint, binding it directly to
the hash of the server's public key.

2. Evidence Transmission: The Evidence containing this binder is conveyed
within the `remoteAttestation` extension of the Certificate message.

3. Cumulative Transcript Incorporation: The Certificate message (and the
Evidence payload within it) is an immutable input into the running
handshake transcript.

4. Transcript Sealing and Key Derivation: That cumulative transcript is
signed by CertificateVerify and authenticated by the Finished MAC. Because
the transcript is cumulative, that same Evidence commitment carries
directly into the transcript hash used to derive the application traffic
keys (`c_ap_traffic` / `s_ap_traffic`).

So while the Evidence is conveyed inside the Certificate message,
verification is anchored downstream, as always. Because the handshake
transcript is cumulative and collision-resistant, tampering with the
Evidence, key shares, or binder produces a divergent transcript hash. That
divergence causes CertificateVerify and the Finished MAC to fail,
immediately aborting the connection before application data can be
decrypted or sent. This assumes the absence of baseline TLS 1.3
implementation failures, of course.

That means Evidence generated on demand for the current TLS handshake will
be cryptographically sealed and bound to the application traffic keys by
the time those keys are instantiated, since the transcript containing the
Evidence serves as the context input in the key schedule. This is exactly
how application traffic keys and remote attestation Evidence are immutably
tied together to provide the required security you mentioned.

Cheers,
Nathanael

On Wed, 4 Nov 2026 at 03:19, Songbo Bu <[e-mail]> wrote:

> Keys earlier than application traffic keys do not establish the
> cryptographic properties required for security.
>
> Section 15.4.2 of draft [1] offers a mitigation. Each paper cited in draft
> offers some mitigation. For example, see:
>
> Section 7.2 of Intra-handshake.fail [2] offers level-2 mitigation. Section
> 9 of ID-crisis [3] offers 6 solutions. Section 4 and 5 of
> EarlyAttestationBleed [4] offer mitigations. Section 7 of our new paper
> EarlyAttestationTschuss offers mitigations.
>
> All vendors, except one, have applied the mitigations.
>
> Best,
> Songbo
>
> [1]
> https://www.ietf.org/archive/id/draft-intra-handshake-fail-61.html#section-15.4.2
>
> [2]
> https://www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS
>
> [3] https://dl.acm.org/doi/10.1145/3779208.3785387
> [4]
> https://www.researchgate.net/publication/414529199_EarlyAttestationBleed_Three_Critical-severity_Vulnerabilities_of_CVSS_90_in_Confidential_Computing
>
> Nathanael Ritz <[e-mail]> 于2026年11月3日周二 15:21写道：
>
>> Hi,
>>
>> On Mon, 2 Nov 2026 at 06:01, Nadim Kobeissi <[e-mail]>
>> wrote:
>>
>>> <snip>
>>>
>>> [...] Calling these tools provers makes it such that "we ran
>>> Tamarin/ProVerif" starts standing in for "we proved it secure" in papers,
>>> audit reports and pitch decks. The authors of these tools have been
>>> curiously comfortable with this misleading practice, but it's time to put
>>> an end to it.
>>>
>>>
>> I can only imagine the framing behind "[...] starts standing in for 'we
>> proved it secure' [...]" is focused at intentional bad-faith marketing
>> attempts or naive interpretations of the tooling (aka in service to pitch
>> decks and the like). In which case, the premise sounds more than
>> plausible.
>>
>> And what about using the tooling to identify real gaps and then using the
>> same tooling to close those gaps? This is a rhetorical question, as the
>> answer seems self-evident to me. Using these tools to identify gaps and
>> then helping protocol designers produce future revisions that avoid the
>> identified pitfalls found through that analysis seems pretty much the
>> point, right?
>>
>> For example, I observed in your paper on formal analysis for
>> draft-ietf-acme-acme-03, from 2016, the paper begins by concluding: "As a
>> result of our disclosures to the ACME team, the latest ACME protocol
>> version (draft-4) has been designed to avoid the pitfalls that make these
>> attacks possible," before proceeding to later advocate to "the CA/Browser
>> forum to eventually mandate the use of ACME (or some other well-defined
>> domain validation protocol that can be formally analyzed)" [0].
>>
>> It makes me wonder how much constructive value could be unlocked for the
>> various relevant fora, if efforts like [1] approached the problem in a
>> similar way you and your collaborators took with ACME."
>>
>> Thanks for sharing your pre-print.
>>
>> Cheers,
>> Nathanael
>>
>> [0] "Formal Modeling and Verification for Domain Validation and ACME",
>> https://doi.org/10.1007/978-3-319-70972-7_32
>>
>> [1] https://datatracker.ietf.org/doc/draft-intra-handshake-fail/
>>
>> On Mon, 2 Nov 2026 at 12:16, Muhammad Usama Sardar <
>> [e-mail]> wrote:
>>
>>> <snip>
>>
>> Problem at our hands was early attestation within the TLS handshake.
>>>
>>> Nothing stopped us from creating a formal model from the implementation
>>> -- we did for several of those; see the 16 published CVEs against
>>> implementations of early attestation in TLS and 25+ more CVEs in process
>>> to come [1] -- most of those are in the critical- to high-severity zone.
>>>
>>> I am curious how cryptographers would have approached this problem.
>>> Maybe they would have started directly with something like CryptoVerif.
>>> Creating all these CVEs is a lot of fun but maybe I will wake up one day
>>> to find out that a cryptographer in this RG has proved the impossibility
>>> of security of early attestation in TLS.
>>>
>>> _______________________________________________
>> CFRG mailing list -- [e-mail]
>> To unsubscribe send an email to [e-mail]
>>
>