Extensions to TLS FATT Process
draft-usama-tls-fatt-extension-07
This document is an Internet-Draft (I-D).
Anyone may submit an I-D to the IETF.
This I-D is not endorsed by the IETF and has no formal standing in the
IETF standards process.
| Document | Type | Active Internet-Draft (individual) | |
|---|---|---|---|
| Author | Muhammad Usama Sardar | ||
| Last updated | 2026-05-02 | ||
| RFC stream | (None) | ||
| Intended RFC status | (None) | ||
| Formats | |||
| Additional resources |
GitHub Repository
|
||
| Stream | Stream state | (No stream defined) | |
| Consensus boilerplate | Unknown | ||
| RFC Editor Note | (None) | ||
| IESG | IESG state | I-D Exists | |
| Telechat date | (None) | ||
| Responsible AD | (None) | ||
| Send notices to | (None) |
draft-usama-tls-fatt-extension-07
Transport Layer Security M. U. Sardar
Internet-Draft TU Dresden
Intended status: Informational 2 May 2026
Expires: 3 November 2026
Extensions to TLS FATT Process
draft-usama-tls-fatt-extension-07
Abstract
This document applies only to non-trivial extensions of TLS, which
require formal analysis. It proposes the authors specify a threat
model and informal security goals in the Security Considerations
section, as well as motivation and a protocol diagram in the draft.
We also briefly present a few pain points of the team doing the
formal analysis which -- we believe -- require refining the process:
* Provide protection against FATT-bypass by other TLS-related WGs
* Contacting FATT
* ML-KEM
* Understanding the opposing goals
* Response within reasonable time frame
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.
Sardar Expires 3 November 2026 [Page 1]
Internet-Draft Extensions to TLS FATT Process May 2026
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 November 2026.
Copyright Notice
Copyright (c) 2026 IETF Trust and the persons identified as the
document authors. All rights reserved.
This document is subject to BCP 78 and the IETF Trust's Legal
Provisions Relating to IETF Documents (https://trustee.ietf.org/
license-info) in effect on the date of publication of this document.
Please review these documents carefully, as they describe your rights
and restrictions with respect to this document. Code Components
extracted from this document must include Revised BSD License text as
described in Section 4.e of the Trust Legal Provisions and are
provided without warranty as described in the Revised BSD License.
Table of Contents
1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . 3
1.1. Motivation . . . . . . . . . . . . . . . . . . . . . . . 4
1.2. Scope . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2. Conventions and Definitions . . . . . . . . . . . . . . . . . 5
2.1. Protocol Diagram . . . . . . . . . . . . . . . . . . . . 5
2.2. Verifier . . . . . . . . . . . . . . . . . . . . . . . . 5
2.3. Definition of Attack . . . . . . . . . . . . . . . . . . 5
3. Pain Points of Verifier . . . . . . . . . . . . . . . . . . . 5
3.1. Provide Protection Against FATT-bypass by Other TLS-related
WGs . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
3.2. Contacting FATT . . . . . . . . . . . . . . . . . . . . . 6
3.2.1. Failure of Current Process . . . . . . . . . . . . . 7
3.3. ML-KEM . . . . . . . . . . . . . . . . . . . . . . . . . 7
3.3.1. Formal Analysis (Work-in-progress) . . . . . . . . . 8
3.3.2. "Cost" . . . . . . . . . . . . . . . . . . . . . . . 9
Sardar Expires 3 November 2026 [Page 2]
Internet-Draft Extensions to TLS FATT Process May 2026
3.4. Understanding the Opposing Goals . . . . . . . . . . . . 9
3.5. Response Within Reasonable Time Frame . . . . . . . . . . 9
4. Proposed Solutions . . . . . . . . . . . . . . . . . . . . . 9
4.1. Contacting FATT . . . . . . . . . . . . . . . . . . . . . 9
4.1.1. Separate List for FATT and WG Members . . . . . . . . 9
4.1.2. Lead FATT Person for Contact . . . . . . . . . . . . 11
4.1.3. Students/Researchers of FATT . . . . . . . . . . . . 11
4.2. ML-KEM: FATT Review . . . . . . . . . . . . . . . . . . . 11
4.2.1. Expected Learning . . . . . . . . . . . . . . . . . . 12
4.3. Scope of FATT . . . . . . . . . . . . . . . . . . . . . . 12
4.4. Discussion at Meeting . . . . . . . . . . . . . . . . . . 12
5. Contribution of Authors . . . . . . . . . . . . . . . . . . . 13
5.1. Real Motivation . . . . . . . . . . . . . . . . . . . . . 13
5.2. Threat Model . . . . . . . . . . . . . . . . . . . . . . 13
5.2.1. Typical Dolev-Yao adversary . . . . . . . . . . . . . 13
5.2.2. Potential Weaknesses of Cryptographic Primitives . . 14
5.2.3. Keys . . . . . . . . . . . . . . . . . . . . . . . . 14
5.3. Informal Security Goals . . . . . . . . . . . . . . . . . 14
5.4. Protocol Diagram . . . . . . . . . . . . . . . . . . . . 15
6. Document Structure . . . . . . . . . . . . . . . . . . . . . 15
6.1. Introduction . . . . . . . . . . . . . . . . . . . . . . 15
6.2. Terminology . . . . . . . . . . . . . . . . . . . . . . . 15
6.3. Motivation and design rationale . . . . . . . . . . . . . 16
6.4. Proposed solution (one or more sections) . . . . . . . . 16
6.5. Security considerations . . . . . . . . . . . . . . . . . 16
6.5.1. Threat model . . . . . . . . . . . . . . . . . . . . 16
6.5.2. Desired security goals . . . . . . . . . . . . . . . 16
6.5.3. Other security implications/considerations . . . . . 16
7. Contribution of Verifier . . . . . . . . . . . . . . . . . . 16
8. Security Considerations . . . . . . . . . . . . . . . . . . . 16
9. IANA Considerations . . . . . . . . . . . . . . . . . . . . . 17
10. References . . . . . . . . . . . . . . . . . . . . . . . . . 17
10.1. Normative References . . . . . . . . . . . . . . . . . . 17
10.2. Informative References . . . . . . . . . . . . . . . . . 17
Appendix . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
Document History . . . . . . . . . . . . . . . . . . . . . . . 19
Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . 20
Author's Address . . . . . . . . . . . . . . . . . . . . . . . . 20
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, the current FATT process
has some practical limitations. Given a relatively smaller formal
methods community, and a steep learning curve as well as very low
consideration of usability in the existing formal analysis tools,
this document proposes some solutions to make the FATT process
Sardar Expires 3 November 2026 [Page 3]
Internet-Draft Extensions to TLS FATT Process May 2026
sustainable.
Specifically, the TLS FATT process does not outline the division of
formal analysis work between the authors and the WG members doing the
formal analysis; the latter is hereafter referred to as the
"Verifier" for convenience. This document aims to propose some
solutions without putting an extensive burden on either party.
An argument is often presented by the authors that an Internet-Draft
is written for the implementers. We make several counter-arguments
here:
* Researchers and protocol designers are also stakeholders of such
specifications [I-D.irtf-cfrg-cryptography-specification].
* Even implementers may like to understand the security implications
before blindly starting to implement it.
* With the FATT process, this argument is clearly invalid. The
Verifier may not be an implementer.
This document outlines the corresponding changes in the way Internet-
Drafts are typically written. For the Internet-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 5. Future versions of
this draft will include concrete examples.
Expected contributions of the Verifier are summarized in Section 7.
1.1. Motivation
A clear separation of expected contributions would help IRTF UFMRG to
train the authors and Verifiers separately to make their own
contributions to the formal analysis.
Sardar Expires 3 November 2026 [Page 4]
Internet-Draft Extensions to TLS FATT Process May 2026
Moreover, we believe that the experiences can help improve the FATT
process. The goal is to document the identified gaps with concrete
examples, discuss those and mutually find the best way forward.
1.2. 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.
2.2. Verifier
In this document, the Verifier refers to the *WG members* doing the
formal analysis. Note that it is *NOT* a new formal role in the WG
process.
2.3. Definition of Attack
Any ambiguity originating from the threat model, informal security
goals, and a Protocol Diagram is to be considered as an attack. The
authors are, therefore, encouraged to be as precise as possible. The
Verifier may propose text for consideration by authors/WG to
disambiguate or propose a fix to the attack.
3. Pain Points of Verifier
From the two extremes -- [I-D.ietf-tls-8773bis] where Russ kindly
provided all requested inputs and we were able to get it through
(with a small change (https://mailarchive.ietf.org/arch/msg/
tls/6Wk82oBGd61rTK23DgfYb7BmRKM/)) without any formal analysis to
[I-D.fossati-tls-attestation-08] where formal analysis revealed
vulnerabilities [ID-Crisis] and resulted in a separate WG to tackle
this problem -- we summarize the pain points of the Verifier with the
Sardar Expires 3 November 2026 [Page 5]
Internet-Draft Extensions to TLS FATT Process May 2026
hope that we can refine the process.
Note that we are not at all asserting that the authors have no pain
points. They very likely have their own -- that is another
indication that the process needs a refinement.
3.1. Provide Protection Against FATT-bypass by Other TLS-related WGs
TLS-related WGs in particular those where the representation of TLS
WG is a minority -- including the one (SEAT WG) that the author has
defended himself as one of the six proponents -- MUST NOT be allowed
to make changes to the TLS protocol beyond what is explicitly allowed
in their charter.
If rechartering of such WGs is _absolutely unavoidable_ and includes
non-trivial changes to the TLS protocol, it MUST only be done after
agreement with the TLS WG. This will prevent the short-circuit path
for FATT. If the WG does not have proper FATT-like process, TLS WG
may request FATT review before WGLC.
In short, our concern is:
What's the point of such a TLS FATT process when other WGs
can simply bypass this process to make key schedule level changes?
For example, [I-D.fossati-seat-early-attestation-00] makes key
schedule level changes, breaks the SEAT WG charter and SEAT WG has no
formal FATT-like process.
3.2. Contacting FATT
According to FATT process [TLS-FATT], FATT is a 'design team' as per
[RFC2418] (also see this (https://datatracker.ietf.org/doc/statement-
iesg-on-design-teams-20011221/)).
The FATT process restricts the WG members -- except for *authors*
(see for example this (https://mailarchive.ietf.org/arch/msg/tls/
pYmjTTlYd11FnjdYoOL6RdGk0sk/))-- from contacting the FATT directly.
This creates an unjustified situation where the authors have an
*exclusive* access to FATT. We argue that WG members -- including
the Verifier -- should also be allowed to contact the FATT because of
the following reasons:
* Formal methods community is small and within this small community,
those with deep knowledge of TLS are quite limited.
Sardar Expires 3 November 2026 [Page 6]
Internet-Draft Extensions to TLS FATT Process May 2026
Such a restriction would not have been there if the Verifier
were not a member of the TLS WG and analyzing the same draft
and free to contact the same FATT for advice. Being a member
of the TLS WG actually puts the Verifier at unnecessary disadvantage.
* The feedback we receive on the list is really limited.
* Communication via chairs is a source of misunderstandings, as it
has already happened with the chairs summarizing the intent of
"Tamarin-like" to just "Tamarin".
* The process has to be *inclusive* of WG members who are willing to
help but don't work in formal methods research groups.
Our proposed solution for this point is in Section 4.1.
3.2.1. Failure of Current Process
The FATT process assigns a "FATT point person" [TLS-FATT] after
adoption. However, until FATT point person is assigned for a draft,
Verifier is essentially not allowed to talk to any one in FATT. Note
that it could mean (almost) the whole lifetime of the draft. A
practical example is the PAKE draft [I-D.ietf-tls-pake]. While the
PAKE authors seemed ready for WGLC in meeting 125, no FATT person has
been announced at the time of publishing this draft.
3.3. ML-KEM
While ML-KEM [I-D.ietf-tls-mlkem] looks like just a "trivial"
addition, it had an opposition of several (ca. 25 in our
understanding) WG members in the last WGLC. We see 2 possible
options:
* Continue tabletop discussions on subjective calculation of risks,
costs, tradeoffs, etc., and keep burning WG energy.
* Do some technical analysis using formal methods (such as symbolic
and computational) to get a confirmation and offer a statement for
security considerations, and move on to more critical works like
hybrid authentication.
We believe the former cannot resolve the dispute. We believe the
latter _may_ help.
Sardar Expires 3 November 2026 [Page 7]
Internet-Draft Extensions to TLS FATT Process May 2026
We believe the security considerations of {{I-D.ietf-tls-mlkem}} are
insufficient. We also believe FATT review could have significantly
improved it, including but not limited to the preference of hybrids,
and potential issues regarding KEM binding in TLS.
We have provided significant feedback during the two WGLCs. However,
almost none of that is actually reflected in the updated editor's
version.
Our proposed solution for this point is in Section 4.2.
3.3.1. Formal Analysis (Work-in-progress)
We have presented observation from our ongoing symbolic security
analysis (cf. limitations in Section 8) using ProVerif on the mailing
list.
We argue that in general:
1. Migration from ECDHE to hybrid is security improvement.
2. Migration from hybrid to standalone ML-KEM is security
regression.
3.3.1.1. Hybrid PQ/T
More formally, the property hybrid PQ/T should provide is:
Hybrid PQ/T is secure unless both ECDHE and ML-KEM are broken.
Hybrid preserves ECDHE, and adds ML-KEM as an additional factor. So
as long as one of them is not broken, the system is secure. In
particular, even if ML-KEM is completely broken, the system retains
the security level of ECDHE.
3.3.1.2. Non-hybrid PQ
On the other hand, the formal property non-hybrid PQ provides is:
Non-hybrid PQ is secure unless ML-KEM is broken.
If ML-KEM is broken, the whole system is broken.
Sardar Expires 3 November 2026 [Page 8]
Internet-Draft Extensions to TLS FATT Process May 2026
3.3.1.3. Comparison
Leak out the ECDHE key from hybrid PQ/T and you get a standalone ML-
KEM. Clearly, hybrid is in general more secure, unless ECDHE is
fully broken, in which case it still falls equivalent to standalone
ML-KEM, or in the hypothetical scenario that there is an
implementation bug in the ECDHE part which is triggered only in
composition.
3.3.2. "Cost"
"Cost" has been presented on the list as the motivation for ML-KEM
but no reference has yet been presented. We believe costs will
depend on several factors and it is quite subjective. There seems to
be a need for a thorough study to understand the "cost."
3.4. Understanding the Opposing Goals
The authors need to understand that the task of the Verifier is to
find the subtle corner cases where the protocol may fail. This is
naturally opposed to the goal of the authors -- that is, to convince
the WG that the protocol is good enough to be adopted/published.
Unless the Verifier remains really focused on checking subtleties,
there is little value of formal analysis.
In particular, some topics like remote attestation need more precise
specifications because small changes or ambiguites may make a big
difference.
3.5. Response Within Reasonable Time Frame
If authors do not respond to the Verifier's questions within a
reasonable time frame (say a few weeks but not months), the Verifier
may not pursue formal analysis of their draft.
4. Proposed Solutions
In addition to those mentioned inline in the previous section, we
propose the following:
4.1. Contacting FATT
4.1.1. Separate List for FATT and WG Members
We propose creating a public mailing list (something like tls-fatt)
for discussions between interested WG members and FATT.
Sardar Expires 3 November 2026 [Page 9]
Internet-Draft Extensions to TLS FATT Process May 2026
In our understanding, the idea -- in a nutshell -- is something like
*hybrid* design team, i.e.,:
* FATT continues to use whatever they currently use for their
internal communication ("closed")
* The proposed list additionally allows public FATT-WG engagement
("open") for questions and discussion of WG members or FATT
4.1.1.1. Potential Need of FATT-WG Engagement
In addition to the questions from the WG for the FATT, FATT also
needs to engage with the WG:
* At *initial* FATT review (just after adoption), FATT may have
questions from authors as well as Verifiers. For the former, to
understand better the threat model and desired security goals,
etc. to be able to suggest which approach is best-suited. For the
latter, to better understand what formal analysis approach and
tool is being planned/currently used (if any).
* During *final* FATT review (just before WGLC), FATT may have
questions on what the Verifier has done, especially in cases where
a peer-reviewed publication is not yet available. We believe
evaluating someone else's code is not easy, or at least if FATT
has the opportunity to talk to the Verifier, it will decrease the
brain cycles that they will have to spend on it.
4.1.1.2. Design Goals
* *minimal process change*: some private discussions typically
happen between authors and FATT; move them to public list for
transparency. Keep intra-FATT communication private as it is.
* *balanced workload*: not to increase anyone's workload on average
over a finite period of time (say lifetime of one document):
joining list is voluntary; responding to list questions is
voluntary
* *all stakeholders benefit*: ensure all stakeholders (FATT,
authors, WG members, chairs) benefit compared to current process
4.1.1.3. Benefits
In addition to transparency where this removes the current situation
where only the authors have an exclusive access to FATT, we think the
proposal has merits where all stakeholders benefit:
Sardar Expires 3 November 2026 [Page 10]
Internet-Draft Extensions to TLS FATT Process May 2026
* *Chairs* get relief from carrying messages back and forth between
WG and FATT.
* *FATT* gets involved early in the process and has to do lesser
work later on (e.g., checking artifacts before WGLC).
* *Interested WG members* get a direct contact with experts.
* *Uninterested WG members* get lesser noise on the TLS list. They
can check the public archives by searching for a specific draft if
they would like to.
4.1.1.4. Risks
* We acknowledge the risk of '*no response from FATT*' identified on
list. In such cases, WG can continue with its best judgement
based on its understanding of the available literature.
4.1.1.5. Open Questions
Opinion of FATT is critical in this proposal whether the middle
ground of hybrid is acceptable to (some of) them.
4.1.2. Lead FATT Person for Contact
This proposal assigns a single FATT person -- referred to as Lead
FATT Person -- who the WG group members and authors can contact for
general queries. It can keep rotating after certain time, such as
one month.
4.1.3. Students/Researchers of FATT
Most of FATT persons are from academia. WG can request FATT to use
their own students/researchers to do the formal analysis.
4.2. ML-KEM: FATT Review
We have formally requested the chairs to initiate the FATT process
for [I-D.ietf-tls-mlkem]. See this
(https://mailarchive.ietf.org/arch/msg/tls/
rClgrWm2hnhESXHx56U8InbwQQs/) and this
(https://mailarchive.ietf.org/arch/msg/
tls/7lj6fYAweMBwNMxFerNl7xhY0pk/).
Sardar Expires 3 November 2026 [Page 11]
Internet-Draft Extensions to TLS FATT Process May 2026
4.2.1. Expected Learning
We believe formal methods can provide additional value for security
considerations of this draft in order to maintain the high
cryptographic assurance of TLS. Since we have no guarantee on
whether ECDHE will break before ML-KEM, it seems appropriate to do
thorough cryptographic analysis. The Harvest Now, Decrypt Later
(HNDL) attack applies equally well to non-hybrid ML-KEM. Adversary
can record all traffic and decrypt it when ML-KEM is broken (or
probably it is already broken; who knows?)
* As an example, it can help justify design choices, such as the
preference for hybrids. It can help identify ways in which ML-KEM
can break. It can also help identify all the assumptions under
which the properties hold.
* As a relevant data point in the context of standardization, LAKE
WG has done formal analysis for EDHOC-PSK with KEM (ref
(https://mailarchive.ietf.org/arch/msg/
lake/2XGOI9OCwylJUfSCasvvwM2FXmw/)).
* _Computational_ analysis (cf. SoK
(https://eprint.iacr.org/2019/1393.pdf))-- using tools such as
CryptoVerif -- seems like a reasonable approach to ensure security
of ML-KEM in TLS, such as binding.
4.3. Scope of FATT
* Be more explicit on:
- what is the scope of FATT?
- what kind of drafts need FATT review and why? Discussion on
this is happening in issue 19 (https://github.com/tlswg/tls-
fatt/issues/19).
4.4. Discussion at Meeting
Formal analysis -- just like any other code development -- is an
iterative process and needs to be **progressively** discussed with
the WG (and not just authors!) to be able to propose secure
solutions.
So at least some time should be allocated in the meetings for
discussion of ongoing formal analysis, rather than just the results.
Sardar Expires 3 November 2026 [Page 12]
Internet-Draft Extensions to TLS FATT Process May 2026
If the authors are doing the formal analysis themselves, it would be
helpful to also present the current state of formal analysis in
meetings for discussion. This may be a single slide describing:
* Approach used: symbolic or computational
* Tool used: ProVerif, CryptoVerif etc.
* Properties established
This will help the WG give any feedback and avoid other Verifiers
doing redundant effort using potentially same tools.
5. Contribution of Authors
The following contributions are expected from the authors:
5.1. Real Motivation
Authors are expected to provide the real motivation of the work
(i.e., the proposed extension of TLS). The Verifier can then ask
questions to improve it.
5.2. Threat Model
A threat model identifies which threats are in scope for the protocol
design. So it should 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?
5.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 should be
explicitly stated.
Sardar Expires 3 November 2026 [Page 13]
Internet-Draft Extensions to TLS FATT Process May 2026
5.2.2. Potential Weaknesses of Cryptographic Primitives
In general, it also outlines the potential weaknesses of the
cryptographic primitives used in the proposed protocol extension.
Examples include:
* weak hash functions
* weak Diffie-Hellman (DH) groups
* weak elements within strong DH groups
5.2.3. Keys
This section should 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 should be distinguished in an unambiguous way.
5.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. should be outlined in the Internet-Draft. If the informal
security goals are not spelled out in the Internet-Draft, it is safe
to assume that the goals are still unclear to the authors.
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.
Sardar Expires 3 November 2026 [Page 14]
Internet-Draft Extensions to TLS FATT Process May 2026
* 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.
5.4. Protocol Diagram
A Protocol Diagram should 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].
6. Document Structure
While the needs may differ for some drafts, we propose the following
baseline template, with an example of
[I-D.wang-tls-service-affinity]:
The template is:
* Easy for readers
* Easy for reviewers
* Easy for formal analysis
TODO: Currently it is almost a copy of the guidance email
(https://mailarchive.ietf.org/arch/msg/tls/LfIHs1OVwDKWmDuCEx0p8wP-
KPs/) to the authors. We will add details in next versions.
6.1. Introduction
* Problem statement: Say in general what the problem is.
* For [I-D.wang-tls-service-affinity], we believe this should _not_
include CATS. Anyone unfamiliar with CATS should be able to
understand your problem.
6.2. Terminology
* Define any terms not defined in RFC8446bis or point to other
drafts from where the definition is used.
Sardar Expires 3 November 2026 [Page 15]
Internet-Draft Extensions to TLS FATT Process May 2026
6.3. Motivation and design rationale
* We really like how Russ motivates the problem statement in
[I-D.ietf-tls-8773bis]. Use it as a sample.
* Here authors should address all the concerns from WG, including
justification with compelling arguments and authentic references
why authors think it should 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.
6.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.
6.5. Security considerations
6.5.1. Threat model
6.5.2. Desired security goals
As draft proceeds these desired security goals will become what the
draft actually achieves.
6.5.3. Other security implications/considerations
7. Contribution of Verifier
When the authors declare the version as ready for formal analysis,
the Verifier takes the above inputs, performs the formal analysis,
and brings the results back to the authors and the WG. Based on the
analysis, the verifier may propose updates to the Security
Considerations section or other sections of the Internet-Draft.
8. Security Considerations
The whole document is about improving security considerations.
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.
Sardar Expires 3 November 2026 [Page 16]
Internet-Draft Extensions to TLS FATT Process May 2026
9. IANA Considerations
This document has no IANA actions.
10. References
10.1. Normative References
[RFC2119] Bradner, S., "Key words for use in RFCs to Indicate
Requirement Levels", BCP 14, RFC 2119,
DOI 10.17487/RFC2119, March 1997,
<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,
May 2017, <https://www.rfc-editor.org/rfc/rfc8174>.
[TLS-FATT] IETF TLS WG, "TLS FATT Process", June 2025,
<https://github.com/tlswg/tls-fatt>.
10.2. Informative References
[I-D.fossati-seat-early-attestation-00]
Sheffer, Y., Mihalcea, I., Deshpande, Y., Fossati, T., and
T. Reddy.K, "Using Attestation in Transport Layer Security
(TLS) and Datagram Transport Layer Security (DTLS)", Work
in Progress, Internet-Draft, draft-fossati-seat-early-
attestation-00, 9 January 2026,
<https://datatracker.ietf.org/doc/html/draft-fossati-seat-
early-attestation-00>.
[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, 21
October 2024, <https://datatracker.ietf.org/doc/html/
draft-fossati-tls-attestation-08>.
[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, 5 September
2025, <https://datatracker.ietf.org/doc/html/draft-ietf-
tls-8773bis-13>.
Sardar Expires 3 November 2026 [Page 17]
Internet-Draft Extensions to TLS FATT Process May 2026
[I-D.ietf-tls-mlkem]
Connolly, D., "ML-KEM Post-Quantum Key Agreement for TLS
1.3", Work in Progress, Internet-Draft, draft-ietf-tls-
mlkem-07, 12 February 2026,
<https://datatracker.ietf.org/doc/html/draft-ietf-tls-
mlkem-07>.
[I-D.ietf-tls-pake]
Bauman, L., Benjamin, D., Menon, S., and C. A. Wood, "A
Password Authenticated Key Exchange Extension for TLS
1.3", Work in Progress, Internet-Draft, draft-ietf-tls-
pake-01, 2 March 2026,
<https://datatracker.ietf.org/doc/html/draft-ietf-tls-
pake-01>.
[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, 13 September 2025,
<https://datatracker.ietf.org/doc/html/draft-ietf-tls-
rfc8446bis-14>.
[I-D.irtf-cfrg-cryptography-specification]
Sullivan, N. and C. A. Wood, "Guidelines for Writing
Cryptography Specifications", Work in Progress, Internet-
Draft, draft-irtf-cfrg-cryptography-specification-02, 7
July 2025, <https://datatracker.ietf.org/doc/html/draft-
irtf-cfrg-cryptography-specification-02>.
[I-D.wang-tls-service-affinity]
Wang, W., Wang, A., Sahni, M., and K. Sheth, "Service
Affinity Solution based on Transport Layer Security
(TLS)", Work in Progress, Internet-Draft, draft-wang-tls-
service-affinity-01, 8 April 2026,
<https://datatracker.ietf.org/doc/html/draft-wang-tls-
service-affinity-01>.
[ID-Crisis]
Sardar, M. U., Moustafa, M., and T. Aura, "Identity Crisis
in Confidential Computing: Formal Analysis of Attested
TLS", November 2025, <https://www.researchgate.net/
publication/398839141_Identity_Crisis_in_Confidential_Computing_Formal_Analysis_of_Attested_TLS>.
[RFC2418] Bradner, S., "IETF Working Group Guidelines and
Procedures", BCP 25, RFC 2418, DOI 10.17487/RFC2418,
September 1998, <https://www.rfc-editor.org/rfc/rfc2418>.
Sardar Expires 3 November 2026 [Page 18]
Internet-Draft Extensions to TLS FATT Process May 2026
[RFC4101] Rescorla, E. and IAB, "Writing Protocol Models", RFC 4101,
DOI 10.17487/RFC4101, June 2005,
<https://www.rfc-editor.org/rfc/rfc4101>.
Appendix
Document History
-07
* Failure of current process in Section 3.2.1
* Students of FATT in Section 4.1.3
* Lead FATT Person for Contact in Section 4.1.2
* 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 5.2
* Helpful discussions on formal analysis in meetings in Section 4.4
* Pointer to formal analysis and costs in Section 3.3
-03
Sardar Expires 3 November 2026 [Page 19]
Internet-Draft Extensions to TLS FATT Process May 2026
* 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
* Pain points of Verifier Section 2.1
* Small adjustment of phrasing
Acknowledgments
We thankfully acknowledge the following for their valuable input:
* Eric Rescorla for review of -02, -05, and -06.
* John Mattsson for proposing text for security considerations.
* S. Moonesamy for identifying the 'no response' risk in the
proposal for new list.
* David Benjamin for review of -06.
The research work is funded by German Research Foundation ("Deutsche
Forschungsgemeinschaft.")
Author's Address
Muhammad Usama Sardar
TU Dresden
Email: muhammad_usama.sardar@tu-dresden.de
Sardar Expires 3 November 2026 [Page 20]