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

[Muhammad Usama Sardar <[e-mail]>]

Hi all,

It seems literally close to impossible that the whole community which 
has reviewed our papers and CVEs will miss anything. AFAIR, I am not 
aware of any single person who has some concern on our papers. Until we 
know any concern against exact statement(s) in the paper in clear terms, 
I don't see any way to do anything, as I have already discussed it in 
detail with many of the relevant participants of this RG (acknowledged 
in [27]: too many to mention here), in addition to the CFRG presentation 
[7,8].

I do believe some folks in CFRG might know but just to get everyone on 
the same page, here was our process for the creation of 16 (at the time 
of writing) issued CVEs:

 1. We submitted confidential vulnerability report together with formal
    analysis (and in some cases regression tests) to repo owner and
    maintainers following their disclosure processes. The maintainers
    reviewed, accepted, and published GitHub Security Advisories
    (GHSAs). Except for one CVE, they themselves requested the CVEs from
    GitHub. What do folks think: is it easy for developers to accept a
    vulnerability of CVSS 9.1 or 9.6? No! Everyone was uncomfortable
    because such a CVE goes straight in news. Who wants to ruin their
    business with such 9.1 CVSS CVEs? Who wants to do additional effort
    of moving from a deployed early (intra-handshake) attestation
    implementation to standard (post-handshake) attestation
    implementation? No one. With more evidence, they eventually accepted.

 2. GitHub (acting as CNA in most cases) and VulnCheck (acting as CNA in
    some cases) reviewed, accepted, and published as CVE record.

 3. NIST reviewed, accepted, and published as CVE records in NVD.

 4. ENISA reviewed, accepted, and published as EUVD records.

 5. China Information Technology Security Evaluation Center (CNITSEC)
    reviewed, accepted, and published as CNNVD records.

 6. Many other reputable international vulnerability database managers
    similarly reviewed, accepted, and published corresponding records in
    their vulnerability databases. I need not name each and every one here.

 7. Papers on these vulnerabilities have been reviewed and accepted at
    ASIA CCS [3] and ESORICS [2].

 8. Large amount of discussions have happened already in IETF/IRTF [11]
    with a wider acknowledgment of the community. I don't find any email
    refuting any claims in the papers or the CVEs. I explicitly asked
    Nathanael multiple times in the past to raise his concerns by
    mentioning the exact statements in paper and his rationale on those.
    Unless I have missed something (feel free to point me to those), I
    never heard any concerns refuting any statement in any paper.

 9. The vulnerabilities and corresponding papers have been shared with
    the related communities: Global Alliance for Genomics and Health
    (GA4GH) [12,13,14], UFMRG [15], Confidential Computing Consortium
    (CCC) [16], Agentic AI Foundation (AAIF) [17,18,19], Open Compute
    Project (OCP) security [20], Civil Infrastructure Platform (CIP)
    [21], ProVerif [22] and RIPE [23] communities. I'm surely missing a
    few, but I hope that gives sufficient idea to the RG. None of the
    CVEs has been refuted by any single person in the wider community to
    the best of my and my co-authors' knowledge at this point in time.

On the threat model, each paper [2,3,4] has a section on threat model 
and we have formalized it in ProVerif artifacts [5,6]. The community is 
welcome to review those papers and clarify exactly where someone sees 
the ambiguity in the threat model by mentioning the exact statement from 
the paper, or the artifacts. We will be happy to clarify/explain.

Apart from the threat model, the community is also welcome to review the 
draft [25], papers [2,3,4] and raise concerns in the corresponding repos 
[5,6,26] within the scope of these repos or in this thread if it is 
related to this discussion.

An upcoming (hopefully tomorrow) paper addresses the community feedback 
on ESORICS paper [2], and explicitly performs formal analysis of 
draft-fossati-seat-early-attestation.

A constructive way to raise concerns is inline:


[11] 
https://www.ietf.org/archive/id/draft-intra-handshake-fail-61.html#section-18.2

[12] 
https://groups.google.com/a/ga4gh.org/g/gif-open-tre-info/c/QBR8O4-jgNg/m/bKTM7WMnCAAJ

[13] 
https://groups.google.com/a/ga4gh.org/g/gif-open-tre-members/c/Tx-7KcXxiFI/m/RNS3STc_BAAJ

[14] 
https://www.researchgate.net/publication/415074362_Presentation_Safeguarding_GA4GH_Ecosystem_from_High-and_Critical-Severity_Vulnerabilities_in_Former_GIF_Design_for_Attested_TLS_draft-fossati-seat-early-attestation

[15] 
https://mailarchive.ietf.org/arch/msg/ufmrg/ZQKdp07P4UeTushAC1q9eBBtp0s/

[16] https://lists.confidentialcomputing.io/g/attestation/topic/121496347

[17] 
https://lists.aaif.io/g/wg-security-privacy/topic/contribution/121504323

[18] https://lists.aaif.io/g/wg-identity-trust/message/9

[19] https://lists.aaif.io/g/wg-governance-risk-regulatory/message/5

[20] https://ocp-all.groups.io/g/OCP-Security/message/1263

[21] https://lists.cip-project.org/g/cip-dev/message/24442

[22] https://sympa.inria.fr/sympa/arc/proverif/2026-09/msg00000.html

[23] https://ripe93.ripe.net/programme/meeting-plan/sessions/137/GJXMGP/

[24] https://github.com/CCC-Attestation/formal-spec-id-crisis/pull/4

[25] https://datatracker.ietf.org/doc/draft-intra-handshake-fail/

[26] https://github.com/muhammad-usama-sardar/intra-handshake-fail

[27] 
https://www.ietf.org/archive/id/draft-intra-handshake-fail-61.html#name-acknowledgments

On 04.11.26 13:33, Nathanael Ritz wrote:
> On Wed, 4 Nov 2026 at 05:37, Muhammad Usama Sardar 
> <[e-mail]> wrote:
>
>     If you have concern on any of our analysis, our proposed
>     mitigations in the papers, or any of our CVE, please say so
>     explicitly by quoting the section numbers, exact statements and
>     the concerns you have. We will address those.
>
> [NR]: Where would you like me to share this feedback? I would be happy 
> to engage if you have a specific repository or a mailing list thread 
> you prefer.

I don't know what's the best place but I believe you are very well aware 
of the repos [5,6] as you have previously provided your feedback there, 
which has been applied. For instance, PR [24] has been waiting your 
confirmation for over one month. Please keep it precise and concise.

Best regards,

-Usama


>
> [9] https://github.com/nathanaelritz/post-handshake.fail
>
> [10] 
> https://mailarchive.ietf.org/arch/msg/seat/QK8_j67VeIqmRLAwncuvfPf4F8g/
>
>     [0]
>     https://www.ietf.org/archive/id/draft-intra-handshake-fail-61.html#section-1.4.1
>
>
>     [5] https://github.com/CCC-Attestation/formal-spec-id-crisis
>
>     [6] https://github.com/muhammad-usama-sardar/intra-handshake.fail
>
>     [7]
>     https://datatracker.ietf.org/meeting/125/materials/slides-125-cfrg-relay-attacks-00
>
>     [8] https://youtu.be/IfKgbO74Lt4?t=6054
>
>         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
>