Relay Attacks Formal

This folder contains the artifacts for formal specification and analysis of the attested TLS proof-of-concept in this repo.

We identified seven candidate binding mechanisms for binding in intra-handshake attestation for standardization of attested TLS protocols:

Client’s attestation nonce

Combination of #2 and #3

Combination of #2 and #4

Combination of #2, #3, and #4

Attested TLS proof-of-concept in this repo uses mechanism #6.

We provide a proof of insecurity of attested TLS proof-of-concept implementation in this repo using the state-of-the-art tool ProVerif .

Handshake traffic key

Application traffic key

We consider TLS Server as RATS Attester, which is typical in confidential computing.

Correlation of Evidence to a DH Shared Secret (G1)

Correlation of Evidence to Client’s Handshake Traffic Key (G2)

Correlation of Evidence to Client’s Application Traffic Key (G3)

The implementation of attested TLS proof-of-concept does not satisfy any of the correlation properties and is thus vulnerable to relay attacks.

Because of high-severity vulnerabilities, we very strongly recommend the developers and maintainers NOT to use this proof-of-concept.

Muhammad Usama Sardar ( : muhammad_usama.sardar at tu-dresden.de)

Muhammad Usama Sardar, Viacheslav Dubeyko, and Jean-Marie Jacquet

Preprint is available here .

Scientific Publication

The formal analysis in this repo is part of the work accepted for publication at ESORICS and should be cited as follows:

Muhammad Usama Sardar, Viacheslav Dubeyko, and Jean-Marie Jacquet. 2026. Intra-handshake.fail (CVE-2026-33697): High-severity CVE in Attested TLS. In 31st European Symposium on Research in Computer Security (ESORICS) 2026, September 14-18, 2026, Rome, Italy. LNCS, 20 pages.

Muhammad Usama Sardar, Viacheslav Dubeyko, and Jean-Marie Jacquet. 2026. Intra-handshake.fail (CVE-2026-33697): High-severity CVE in Attested TLS. In 31st European Symposium on Research in Computer Security (ESORICS) 2026, September 14-18, 2026, Rome, Italy. LNCS, 20 pages.

and then use as {{Intra-handshake.fail}}

For citing the corresponding repo with complete artifacts:

and then use as {{Intra-handshake.fail-repo}}

We gratefully acknowledge the following for insightful discussions on this work:

We also gratefully acknowledge the following who gave feedback on state-of-the-art that we utilize as the basis:

Several others at the IETF, IRTF, CCC, and GA4GH have contributed by providing feedback.

We sincerely thank Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi for the foundational formal model of draft 20 of TLS 1.3 in their work .

We use state-of-the-art symbolic security analysis tool ProVerif for the specification of the protocols.

Install the latest version (2.05 at the moment) of ProVerif: see for details. See Section 1.4 of manual for installation options:

via OPAM: Section 1.4.1

from sources: Section 1.4.2 or simply try the script by replacing 2.04 by 2.05

from binaries: Section 1.4.3

The formal model uses the fixed version of diversion attacks in intra-handshake attestation from our work as the starting point to focus on relay attacks in intra-handshake attestation in this work. The rationale is that we consider it more useful to show the added value of this contribution to the community by using the fixed version of diversion attacks in intra-handshake attestation as the baseline, rather than showing the same diversion attacks from ID-Crisis paper , and the discovered CVE (CVE-2026-33697) -- which the analysis could not find -- practically demonstrates the added value.

Artifacts organization

Folder binder6 contains code for binding mechanism #6.

Running automatic proofs

For completeness, optional commands for running other properties are also provided for each.

With other properties

Generation of traces for failing properties

In order to additionally generate a trace for each property which results in "false", create a subfolder (e.g., traces in the following command) for results before executing.

Then to execute: run as follows:

Subfolder traces will contain the traces in .dot as well as .PDF.

With other properties

To additionally save in log file together with display:

With other properties

To additionally see the Horn clauses generated in ProVerif:

a. use command-line option -test as follows:

b. add one of the following two settings inside the input (*.pv) file:

set verboseClauses = short. to display the Horn clauses

set verboseClauses = short. to display the Horn clauses

set verboseClauses = explained. to additionally display a sentence after each clause it generates to explain where this clause comes from.

set verboseClauses = explained. to additionally display a sentence after each clause it generates to explain where this clause comes from.

With other properties

a. use command-line option -test as follows:

To run in interactive mode:

With other properties

Upcoming and Recent Talks and Research Visits

If you are around on any of the following venues of upcoming talks (in reverse chronological order) on topics related to the project, you are very welcome to join/meet.

Feedback/ /Critique/Contributions

We would love to have your contributions and feedback (especially critique! yes, this is how the science progresses, but please be genuine!). Muhammad Usama Sardar on CCC Slack Workspace, by email , submit a minimal PR, or open an issue.