Internet-Draft Proposed Document Template for TLS FATT July 2026
Sardar Expires 3 January 2027 [Page]
Workgroup:
Transport Layer Security
Internet-Draft:
draft-usama-tls-fatt-extension-08
Published:
Intended Status:
Informational
Expires:
Author:
M. U. Sardar
TU Dresden

Proposed Document Template for TLS FATT Process

Abstract

This document applies only to non-trivial extensions of TLS, which require formal analysis. FATT process has successfully discovered CVEs of CVSS 7.5 and most recently expected CVSS 9.1 in the production implementations of the drafts proposed for adoption in the TLS WG. To achieve high cryptographic assurances, this document proposes the drafts specify a clear threat model and informal security goals in the Security Considerations section, as well as motivation and a protocol diagram in the draft.

About This Document

This note is to be removed before publishing as an RFC.

The latest revision of this draft can be found at https://muhammad-usama-sardar.github.io/tls-fatt-extension/draft-usama-tls-fatt-extension.html. Status information for this document may be found at https://datatracker.ietf.org/doc/draft-usama-tls-fatt-extension/.

Discussion of this document takes place on the Transport Layer Security Working Group mailing list (mailto:tls@ietf.org), which is archived at https://mailarchive.ietf.org/arch/browse/tls/. Subscribe at https://www.ietf.org/mailman/listinfo/tls/.

Source for this draft and an issue tracker can be found at https://github.com/muhammad-usama-sardar/tls-fatt-extension.

Status of This Memo

This Internet-Draft is submitted in full conformance with the provisions of BCP 78 and BCP 79.

Internet-Drafts are working documents of the Internet Engineering Task Force (IETF). Note that other groups may also distribute working documents as Internet-Drafts. The list of current Internet-Drafts is at https://datatracker.ietf.org/drafts/current/.

Internet-Drafts are draft documents valid for a maximum of six months and may be updated, replaced, or obsoleted by other documents at any time. It is inappropriate to use Internet-Drafts as reference material or to cite them other than as "work in progress."

This Internet-Draft will expire on 3 January 2027.

▲

Table of Contents

1. Introduction

While the TLS FATT process [TLS-FATT] marks a historic change in achieving high cryptographic assurances by tightly integrating formal methods in the working group (WG) process, it would be helpful to adapt the way in which drafts are typically written to get the benefits.

1.1. Motivation

Unverified protocol designs, imprecisely stated threat model and security goals have led to high and critical severity vulnerabilities of the extensions proposed in the drafts.

1.1.1. Concrete Motivational Example: Practical Exploits in Production Systems

As an illustrative example, authors of [I-D.fossati-tls-attestation-08] asked for adoption in IETF 121, explicitly requesting us (by name) for formal analysis [Intra-handshake-attestation]. We carried out formal analysis of draft in support for FATT process. The formal analysis led to three orthogonal issues:

This shows the value of FATT process in the design of secure protocols to find subtle vulnerabilities, which could otherwise be missed.

1.2. Proposal

To produce high-quality specifications, this document outlines the corresponding changes in the way drafts are typically written. For the draft to be useful for the formal analysis, this document proposes that it would be helpful for the formal analysis if the draft contains four main items, namely:

  • motivation,

  • a threat model,

  • informal security goals, and

  • a protocol diagram (Section 2.1).

Each one of these is summarized in Section 3. Future versions of this draft will include further concrete examples.

1.3. Scope

The scope of this document is only non-trivial extensions of TLS, which require formal analysis.

2. Conventions and Definitions

The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in BCP 14 [RFC2119] [RFC8174] when, and only when, they appear in all capitals, as shown here.

2.1. Protocol Diagram

In the context of this document, a Protocol Diagram specifies the proposed cryptographically-relevant changes compared to the standard TLS protocol [I-D.ietf-tls-rfc8446bis]. This is conceptually similar to the Protocol Model in [RFC4101]. However, while [RFC4101] only recommends diagrams, we consider diagrams to be essential to reduce the gap between:

  • the specifications and formal analysis

  • the specifications and implementation

3. Contents of Drafts

The following contents are expected in drafts:

3.1. Motivation

Drafts are expected to provide the motivation of the work (i.e., the proposed extension of TLS).

3.2. Threat Model

A threat model identifies which threats are in scope for the protocol design. So it can answer questions like:

  • What are the capabilities of the adversary? What can the adversary do?

  • Whether post-quantum threats are in scope?

  • What can go wrong in the system? etc.

  • What are the computational and memory resources available to the adversary?

3.2.1. Typical Dolev-Yao adversary

A typical threat model assumes the classical Dolev-Yao adversary, who has full control over the communication channel.

Any additional adversary capabilities and assumptions ought to be explicitly stated.

3.2.2. Keys

This is particularly relevant for proposals of hybrid key establishment or hybrid authentication. This section ought to specify any keys in the system (e.g., long-term keys of the server) in addition to the standard TLS key schedule. Theoretically and arguably practically, any key may be compromised (i.e., become available to the adversary).

For readability, we propose defining each key clearly as in Section 4.1 of [ID-Crisis]. Alternatively, present as a table with the following entries for each key:

  • Name (or symbol) of the key

  • Purpose of the key

  • (optionally but preferably -- particularly when the endpoint is not fully trusted) Which software in the system has access to the key?

If more than one servers are involved (such as migration cases), the keys for servers ought to be distinguished in an unambiguous way.

3.3. Informal Security Goals

Knowing what you want is the first step toward achieving it. Hence, informal security goals such as integrity, authentication, freshness, etc. ought to be outlined in the draft.

Examples:

  • Integrity of message X holds unless some key Y is leaked.

  • (stated differently) Integrity of message X holds as long as some key Y is protected.

  • Freshness of message X holds unless some key Y or some key Z is leaked.

  • Server Authentication holds unless some key Y or some key Z is leaked.

See Section 5.1 of [ID-Crisis] for concrete examples.

3.4. Protocol Diagram

A Protocol Diagram ought to clearly mention the initial knowledge of the protocol participants, e.g., which authentic public keys are known to the protocol participants at the start of the protocol. An example of a Protocol Diagram for [I-D.fossati-tls-attestation-08] is provided in Figure 5 in [ID-Crisis].

4. Document Structure

While the needs may differ for some drafts, we propose the following baseline template, with examples of [I-D.wang-tls-service-affinity] and [I-D.sheffer-tls-pqc-continuity]:

The template is:

TODO: Currently it is almost a copy of the guidance email to the authors. We request feedback on what to add in next versions.

4.1. Introduction

  • Problem statement: Say in general what the problem is.

  • For [I-D.wang-tls-service-affinity], we believe this may preferably not include CATS. Anyone unfamiliar with CATS ought to be able to understand the problem statement.

4.2. Terminology

  • Define any terms not defined in RFC8446bis or point to other drafts from where the definition is used.

4.3. Motivation and design rationale

  • We really like how the author of [I-D.ietf-tls-8773bis] motivates the problem statement. Use it as a sample.

  • Here authors can address all the concerns from WG, including justification with compelling arguments and authentic references why authors think it ought to be done within TLS WG (and within handshake).

  • For [I-D.wang-tls-service-affinity], authors could put CATS here as a motivational use case.

  • For [I-D.sheffer-tls-pqc-continuity], it should clarify why the problem is specific to PQ-only and why did the WG do such a thing for the transition for other primitives, as requested by several WG participants.

4.4. Proposed solution (one or more sections)

  • Protocol design with Protocol Diagram: we work on the formal analysis of TLS 1.3 exclusively. Please contact someone else if your draft relates to older versions.

4.5. Security considerations

4.5.2. Desired security goals

As draft proceeds these desired security goals will become what the draft actually achieves.

5. Security Considerations

The whole document is about improving security considerations. As mentioned in Section 1.1.1, unverified specifications have led to high and critical severity exploits.

Like all security proofs, formal analysis is only as strong as its assumptions and model. The scope is typically limited, and the model does not necessarily capture real-world deployment complexity, implementation details, operational constraints, or misuse scenarios. Formal methods should be used as complementary and not as subtitute of other analysis methods.

6. IANA Considerations

This document has no IANA actions.

7. References

7.1. Normative References

[RFC2119]
Bradner, S., "Key words for use in RFCs to Indicate Requirement Levels", BCP 14, RFC 2119, DOI 10.17487/RFC2119, , <https://www.rfc-editor.org/rfc/rfc2119>.
[RFC8174]
Leiba, B., "Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words", BCP 14, RFC 8174, DOI 10.17487/RFC8174, , <https://www.rfc-editor.org/rfc/rfc8174>.
[TLS-FATT]
IETF TLS WG, "TLS FATT Process", , <https://github.com/tlswg/tls-fatt>.

7.2. Informative References

[CVE-2026-33697]
CVE, "CoCoS attested TLS is vulnerable to relay attacks via extracted ephemeral TLS keys", , <https://www.cve.org/CVERecord?id=CVE-2026-33697>.
[I-D.fossati-tls-attestation-08]
Tschofenig, H., Sheffer, Y., Howard, P., Mihalcea, I., Deshpande, Y., Niemi, A., and T. Fossati, "Using Attestation in Transport Layer Security (TLS) and Datagram Transport Layer Security (DTLS)", Work in Progress, Internet-Draft, draft-fossati-tls-attestation-08, , <https://datatracker.ietf.org/doc/html/draft-fossati-tls-attestation-08>.
[I-D.fossati-tls-attestation-09]
Tschofenig, H., Sheffer, Y., Howard, P., Mihalcea, I., Deshpande, Y., Niemi, A., and T. Fossati, "Using Attestation in Transport Layer Security (TLS) and Datagram Transport Layer Security (DTLS)", Work in Progress, Internet-Draft, draft-fossati-tls-attestation-09, , <https://datatracker.ietf.org/doc/html/draft-fossati-tls-attestation-09>.
[I-D.ietf-tls-8773bis]
Housley, R., "TLS 1.3 Extension for Using Certificates with an External Pre-Shared Key", Work in Progress, Internet-Draft, draft-ietf-tls-8773bis-13, , <https://datatracker.ietf.org/doc/html/draft-ietf-tls-8773bis-13>.
[I-D.ietf-tls-rfc8446bis]
Rescorla, E., "The Transport Layer Security (TLS) Protocol Version 1.3", Work in Progress, Internet-Draft, draft-ietf-tls-rfc8446bis-14, , <https://datatracker.ietf.org/doc/html/draft-ietf-tls-rfc8446bis-14>.
[I-D.sheffer-tls-pqc-continuity]
Sheffer, Y. and T. Reddy.K, "PQC Continuity: Downgrade Protection for TLS Servers Migrating to PQC", Work in Progress, Internet-Draft, draft-sheffer-tls-pqc-continuity-02, , <https://datatracker.ietf.org/doc/html/draft-sheffer-tls-pqc-continuity-02>.
[I-D.wang-tls-service-affinity]
Wang, W., Wang, A., 汪宗斌, P., Sahni, M., and K. Sheth, "Service Affinity Solution based on Transport Layer Security (TLS)", Work in Progress, Internet-Draft, draft-wang-tls-service-affinity-03, , <https://datatracker.ietf.org/doc/html/draft-wang-tls-service-affinity-03>.
[ID-Crisis]
Sardar, M., Moustafa, M., and T. Aura, "Identity Crisis in Confidential Computing: Formal Analysis of Attested TLS", ACM, Proceedings of the ACM Asia Conference on Computer and Communications Security pp. 547-560, DOI 10.1145/3779208.3785387, , <https://doi.org/10.1145/3779208.3785387>.
[ID-Crisis-repo]
Sardar, M. U., Moustafa, M., and T. Aura, "Identity Crisis in Confidential Computing: Formal Analysis of Attested TLS", , <https://github.com/CCC-Attestation/formal-spec-id-crisis>.
[Intra-handshake-attestation]
Hannes Tschofenig, "Attestation and TLS", , <https://datatracker.ietf.org/meeting/121/materials/slides-121-tls-tls-and-attestation-00.pdf>.
[Intra-handshake.fail]
Sardar, M. U., Dubeyko, V., and J.-M. Jacquet, "Intra-handshake.fail (CVE-2026-33697): High-severity CVE in Attested TLS", , <https://www.researchgate.net/publication/408219182_Intra-handshakefail_CVE-2026-33697_High-severity_CVE_in_Attested_TLS>.
[Intra-handshake.fail-repo]
Sardar, M. U., Dubeyko, V., and J.-M. Jacquet, "Intra-handshake.fail (CVE-2026-33697): High-severity CVE in Attested TLS", , <https://github.com/CCC-Attestation/formal-spec-KBS>.
[RFC4101]
Rescorla, E. and IAB, "Writing Protocol Models", RFC 4101, DOI 10.17487/RFC4101, , <https://www.rfc-editor.org/rfc/rfc4101>.

Appendix

Document History

-08

  • Focused on document structure only

  • Motivational examples

-07

  • Failure of current process

  • Students of FATT

  • Lead FATT Person for Contact

  • Feedback from the WG

-06

  • Solution for ML-KEM: FATT analysis

  • Solution for FATT contact: new mailing list

  • Replaced responsibilities by expected contributions

  • Clarified Verifier even further that it is just a WG member; no formal role

  • s/pure/non-hybrid

-05

  • Removed process-related stuff

  • Moved discussion at meeting to solutions

  • Added ML-KEM

-04

  • Extended threat model Section 3.2

  • Helpful discussions on formal analysis in meetings

  • Pointer to formal analysis and costs

-03

  • Limitations of formal analysis in security considerations

  • Proposed solutions section

  • More guidance for authors: Threat Model and Informal Security Goals

-02

  • Added document structure

  • FATT-bypass by Other TLS-related WGs

  • FATT process not being followed

-01

Acknowledgments

We thankfully acknowledge the following for their valuable input:

We gratefully acknowledge the valuable contributions of co-authors of papers for their instrumental contributions in formal analysis: Mariam Moustafa, Tuomas Aura, Viacheslav Dubeyko, and Jean-Marie Jacquet.

We sincerely thank the contributors of the formal analyses [ID-Crisis-repo] and [Intra-handshake.fail-repo] mentioned in the respective repositories.

We express our appreciation to Yaakov Stein and Ilari Liusvaara for their substantial technical guidance, valuable feedback, and contributions in early attempts to formally model ML-KEM.

The research work is funded by German Research Foundation ("Deutsche Forschungsgemeinschaft.")

Author's Address

Muhammad Usama Sardar
TU Dresden