Session Date/Time: 16 Oct 2024 18:00

TLS

Summary

This meeting focused on reviewing and refining the TLS Working Group's Formal Analysis Team (FAT) process. The discussion centered on the intent of the FAT, its integration with the working group's document lifecycle, and practical challenges, particularly around securing formal security analysis. Key aspects included the role of a FAT liaison, the timing of reviews, and the scope of documents subject to FAT review. The working group agreed to move forward with the proposed process, acknowledging the need to address the open question of how to resource formal analysis.

Key Discussion Points

Note Well: The Chairs (Sean Turner, Goran Selmeci, Joe Salowey) reminded participants of the IETF Note Well and IPR disclosure requirements.
Agenda Overview: The primary goal was to review the general intent and process of the FAT, including its integration with the working group process, and to solicit feedback on potential improvements and documentation.
Intent of the FAT Process:
- To preserve existing security properties of TLS protocols, as proven by security researchers.
- To integrate security researchers into the protocol development process, allowing time for review and publication of analysis.
- The goal is to maintain the "pact" made with security researchers during TLS 1.3 development. There was no dissent on the fundamental idea of having a FAT process.
FAT Process Details:
- Working Group Adoption: The FAT process should not gate working group adoption. Initial review can be requested by chairs after adoption to identify potential issues early.
- FAT Liaison: A dedicated liaison person will act as the interface between the FAT experts and the working group. This person will collate responses, note consensus/dissension among FAT experts, and facilitate interaction between the working group (chairs, authors) and the FAT. This role is intended to manage potentially diverging expert opinions privately, presenting a consolidated view to the WG.
- Review Stages:
  - Initial ID Review: A "sniff test" after working group adoption to catch major issues early. Output: "needs analysis" or "good to go."
  - Stable ID Review: Right before Working Group Last Call (WGLC), when the document is relatively stable. This allows time for in-depth review, potentially months.
  - Formal Security Analysis (if requested): If the FAT recommends formal analysis and the working group agrees, this analysis can be commissioned and then reviewed by the FAT.
- FAT Input into WGLC: FAT input (including analysis recommendations and reviews) is submitted to the WGLC process. The working group ultimately decides how to act on this input.
- Shepherd Write-up: The shepherd write-up to the IESG will include an analysis of the FAT's input, detailing what was covered, what wasn't, and any instances where FAT recommendations were not followed, along with the reasons why.
Process Flowchart Review: Sean Turner presented a flowchart illustrating the FAT process, highlighting interaction points:
- After WG call for adoption, the WG begins work, and chairs request initial FAT review.
- Draft iterates, potentially with formal analysis happening organically.
- Once stable, the draft is sent for FAT review, which feeds into WGLC.
- If formal analysis is needed and not yet done, the WG decides whether to proceed with it.
- The FAT reviews the formal analysis. Successful analysis and addressed WGLC comments lead to IESG review.
Challenge: How to get formal analysis done? This was identified as the biggest open question. If the FAT recommends formal analysis and authors lack the expertise or resources, the mechanism for commissioning or performing this analysis is unclear.
- Ideas included leveraging UFM RG (IRTF Formal Methods Research Group) and its tools, "beg, borrow, and steal" from friends in the community, or potential future funding mechanisms if timelines stretch.
- There is hope that incentives (research results, good for humanity) might encourage participation.
Anonymity of Reviews: All FAT participants are known, and their contributions to the consolidated feedback via the liaison are known. The intent of the liaison is to allow FAT experts to discuss and disagree internally without public scrutiny, arriving at a team consensus.
Review Timelines:
- Initial "sniff test" feedback: Weeks (2-3 weeks, potentially up to a month if internal FAT consensus takes time).
- Actual formal analysis: Months, depending on the complexity and resource availability. The goal is to avoid delays of "years."
Case Study: draft-ietf-tls-wkd-8773bis (Russ's draft):
- This draft is currently at the "formal analysis needed, who does it?" stage, after already being published as an experimental RFC and being referenced as a down-ref.
- The lack of a dedicated FAT liaison for this draft was identified as a contributing factor to its current deadlock, as conflicting expert opinions ("big change" vs. "trivial") have not been internally reconciled by the FAT.
- The chairs acknowledge the need to unblock this draft promptly, ideally before the Dublin meeting.
FAT Composition: The FAT currently has 6-7 members, with plans to grow. Liaisons will rotate per document to prevent burnout.
Dennis Jackson's Feedback: Generally positive, emphasizing that the FAT should focus on formal verification questions, not IETF process, and that the WG makes the final decisions.
Scope of FAT Application: Not all TLS working group documents require FAT review. Only documents that significantly change the key schedule or other primary cryptographic components, thereby potentially affecting the proven security properties of TLS 1.3, will be subject to this process. Examples include new cipher suites affecting RSA, but not necessarily key log extensions.
Continuous Interaction: The formal analysis process, if initiated, should involve continuous back-and-forth between document authors, analysts, and the FAT (via liaison) between adoption and WGLC, allowing the document and analysis to evolve together.
Escalation: If timelines for formal analysis extend to "double-digit months," the chairs will revisit the process and consider how to obtain resources (e.g., funding) to maintain the "pact" with researchers.
AD Feedback: Paul Wouters (AD) indicated no red flags from his perspective.

Decisions and Action Items

Decision: The proposed FAT process, including the introduction of a FAT liaison for each document, is accepted and will be implemented.
Action Item: The Chairs will send a summary of this discussion to the TLS mailing list, noting the process's adoption and the outstanding challenge of resourcing formal security analysis.
Action Item: The Chairs will work to assign a FAT liaison to draft-ietf-tls-wkd-8773bis to facilitate internal FAT discussion and move the analysis process forward.
Action Item: Working Group participants who wish to propose topics for the upcoming Dublin meeting should submit their requests quickly due to limited slots.

Next Steps

The TLS WG will begin applying the updated FAT process to new and ongoing drafts that fall within its scope.
The chairs will continue to explore potential solutions for obtaining formal security analysis when required and not provided by authors.
Preparation for the Dublin IETF meeting will continue.