Skip to main content

Challenges, Opportunities, and Directions for Formal Analysis in the IETF and IRTF

Document Type Active Internet-Draft (individual)
Author Christopher A. Wood
Last updated 2023-03-13
RFC stream (None)
Intended RFC status (None)
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)
Network Working Group                                         C. A. Wood
Internet-Draft                                                Cloudflare
Intended status: Informational                             13 March 2023
Expires: 14 September 2023

  Challenges, Opportunities, and Directions for Formal Analysis in the
                             IETF and IRTF


   This document discusses challenges, opportunities, and directions for
   formal analysis of protocols developed in the IETF.

About This Document

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

   Status information for this document may be found at

   Source for this draft and an issue tracker can be found at

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

   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 14 September 2023.

Copyright Notice

   Copyright (c) 2023 IETF Trust and the persons identified as the
   document authors.  All rights reserved.

Wood                    Expires 14 September 2023               [Page 1]
Internet-Draft         Formal Analysis Challenges             March 2023

   This document is subject to BCP 78 and the IETF Trust's Legal
   Provisions Relating to IETF Documents (
   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.

Table of Contents

   1.  Introduction  . . . . . . . . . . . . . . . . . . . . . . . .   2
   2.  Conventions and Definitions . . . . . . . . . . . . . . . . .   4
   3.  Analysis Overview . . . . . . . . . . . . . . . . . . . . . .   4
   4.  Analysis Challenges and Open Problems . . . . . . . . . . . .   5
     4.1.  Timelines . . . . . . . . . . . . . . . . . . . . . . . .   5
     4.2.  Tooling . . . . . . . . . . . . . . . . . . . . . . . . .   6
     4.3.  Incentives  . . . . . . . . . . . . . . . . . . . . . . .   7
     4.4.  Complexity and Precision  . . . . . . . . . . . . . . . .   7
     4.5.  Resource Limits . . . . . . . . . . . . . . . . . . . . .   8
   5.  Security Considerations . . . . . . . . . . . . . . . . . . .   9
   6.  IANA Considerations . . . . . . . . . . . . . . . . . . . . .   9
   7.  References  . . . . . . . . . . . . . . . . . . . . . . . . .   9
     7.1.  Normative References  . . . . . . . . . . . . . . . . . .   9
     7.2.  Informative References  . . . . . . . . . . . . . . . . .  10
   Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . .  11
   Author's Address  . . . . . . . . . . . . . . . . . . . . . . . .  11

1.  Introduction

   The IETF and IRTF produce technical specifications for protocols used
   on the Internet.  Applications use these technical specifications in
   shipping software.  Often times, use of these technical
   specifications has a direct impact on end users of the Internet.  As
   an obvious example, TLS 1.3 [TLS13] is the de-facto transport
   security protocol used on the Internet, protecting data in transit
   between different different parties on the Internet.

   The process by which TLS 1.3 was developed was unique for its time.
   In the wake of one too many security problems with prior versions of
   the protocol, TLS 1.3 was developed in close collaboration with
   security researchers to ensure that the resulting design and
   specification provided provably secure properties that one would
   expect from such a protocol.  The process took years and resulted in
   dozens of academic publications and interoperable implementations,
   further improving the community's confidence in the result.  And in
   the end, the work paid off: TLS 1.3 has be safely deployed at scale
   for years without any significant issues.

Wood                    Expires 14 September 2023               [Page 2]
Internet-Draft         Formal Analysis Challenges             March 2023

   Several IETF protocols since TLS 1.3 have built on the process by
   which it was developed, including QUIC [RFC9000], MLS [MLS],
   Oblivious HTTP [OHTTP], and Privacy Pass [PRIVACYPASS].  Each of
   these published and developing specifications have incorporated
   security analysis into the process by which the specifications are

   Formal analysis gives us confidence in the protocols we specify and
   deploy.  It advocates for a rigorous approach to defining protocols
   and describing their security properties.  Failure to apply formal
   analysis does not definitively yield protocols with known flaws, but
   it can lead to security failures in practice.  Infamous examples as
   of late include Matrix, Telegram, PGP, and various configurations of
   TLS 1.2 and earlier versions.  In contrast, applying formal analysis
   helps demonstrate that certain classes of attacks are not applicable.
   While this does not necessarily rule out attacks entirely, since
   modeling and analysis is always imprecise and requires simplifying
   compromise, it has the potential to more consistently yield better

   However, there are still plenty of examples of technical
   specifications that lack any sort of formal analysis.  Lack of formal
   analysis is problematic for a number of reasons, including, though
   not limited to, the following:

   1.  Real world vulnerabilities.  Protocol specifiations may be
       developed with security or privacy vulnerabilities.  Such
       vulnerabilities can lead to real problems for end users.  In this
       sense, publishing specifications without formal analysis is akin
       to testing software in production, yet is uniquely worse since
       updating specifications requires IETF processes to enact and
       takes time.

   2.  Specification misuse.  Formal analysis requires a certain degree
       of precision and rigor in which specifications for algorithms,
       protocols, and systems are described.  This precision helps
       refine the interface for these types of objects.  Lack of
       analysis can therefore lead to misuse of the object.  This can in
       turn lead to undesired outcomes, including even security

   3.  Audience confusion.  Protocol specifications without analysis may
       lack precision or specificity that often comes from formal
       analysis, yielding complex documents that are difficult to
       understand, use, and deploy in practice.

Wood                    Expires 14 September 2023               [Page 3]
Internet-Draft         Formal Analysis Challenges             March 2023

   Lack of formal analysis comes from a variety of reasons.  This
   document summarizes some of those problems and discusses
   opportunities for potential solutions and new directions the
   community can explore to improve the situation.  It is meant to
   encourage discussion, not be published as an RFC.

2.  Conventions and Definitions

   The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT",
   "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.

3.  Analysis Overview

   As the IETF is primarily tasked with producing technical
   specifications for protocols, analysis of these protocols can benefit
   greatly from computer-aided tools.  For example, [ProVerif] and
   [Tamarin] are both tools that protocol designers can use to model
   their protocol, attacker, and prove (or disprove) certain properties
   of the protocol.  As with any modeling tool, these are limited both
   by the specificity of the model as well as the questions that are
   asked of the model.  For example, security protocol models often make
   simplifying assumptions about the underlying cryptographic objects
   used in the protocol, whereas in practice these objects may break
   over time.  Hand-written proofs complement computer-aided, machine-
   checked proofs.  These proofs are often more complicated since they
   more accurately model all aspects of the protocol.  As a result,
   these proofs yield mathematically precise statements of security.

   Regardless of the mechanism, analysis generally follows the following

   1.  Specify the threat model, including the attacker and its

   2.  Specify the security goals with respect to this threat model.

   3.  Describe whether the security goals are met and, if and when they
       are not met, a description of how they are not met through an
       exemplary attack that violates the goal.  Applicable attacks are
       often accompanied with explanations of why they are out of scope
       or how applications and deployments can deal with the attack in

Wood                    Expires 14 September 2023               [Page 4]
Internet-Draft         Formal Analysis Challenges             March 2023

   The order of these tasks is not always the same, but the content is
   generally consistently applied.  What differs across technical
   specifications is the rigor through which these tasks are achieved.
   As an example, TLS 1.3 (Appendix E of [TLS13]) includes a list of
   security properties and, for each property, describes the attacker
   model in which these properties are satisfied.  It additionally
   points to relevant, peer reviewed formal analysis work that
   demonstrates validity of these claims.  QUIC [QUIC] lists various
   types of attacker models and, within each attacker model, the types
   of attacks that are possible.  However, unlike [TLS13], does not have
   backing formal analysis for all of claims about attack resistance.
   As another example, Oblivious HTTP [OHTTP] takes an even different
   approach by informally describing the threat model and security goals
   of the protocol, with a reference to backing analysis (that did not
   receive peer review) with Tamarin.

4.  Analysis Challenges and Open Problems

   This section describes some high level problems that impact the scale
   at which the IETF and IRTF applies formal analysis to technical

4.1.  Timelines

   Sometimes formal analysis does not occur due to mismatched timelines.
   Formal analysis takes time, and that time may not align with the
   desired pace at which a technical specification moves towards
   publication.  The general requirement for advancing technical
   specifications in IETF and IRTF groups is rough consensus and running
   code, and those are often easier to achieve than formal analysis.  In
   many cases, the pressure to ship or otherwise advance specifications
   often trumps the desire for formal analysis.

   Analysis is time consuming, perhaps even more so than the development
   of the specification itself.  While the iterative process TLS 1.3
   established between specification, analysis, and experimentation is
   ideal, often times many protocols are fully specified prior to
   analysis.  Applying analysis after specification in sequence, rather
   than in applying analysis in parallel with protocol specification,
   means that the result on publishing time is worsened.

   Overcoming this challenge may require a change in the way in which we
   establish consensus for technical specifications.  Some possibilities
   are below.

   1.  Establish a set of common questions and formal process for formal
       analysis.  This may include, for example, a template by which
       analysis findings may be documented, as well as key questions to

Wood                    Expires 14 September 2023               [Page 5]
Internet-Draft         Formal Analysis Challenges             March 2023

       ask.  It may also include standardized notation that document
       editors can use for noting analysis-relevant questions and issues
       in their protocol documents.

   2.  Seek out formal analysis for working group documents as soon as
       possible after adoption.  This helps ensure that analysis occurs
       in line with protocol specification to the maximum extent

   3.  Encourage protocol editors and expert reviewers to share analysis
       results with the relevant working group(s) as early as possible.
       If possible, these findings can be shared during in-person
       meetings, but may also be shared on the mailing list.

4.2.  Tooling

   Another barrier to scaling formal analysis is the state of tooling.
   While there exists a wide variety of tools by which protocol
   designers can model and analyze their protocol, including [ProVerif]
   and [Tamarin], not all tools are easy-to-use for protocol designers
   or provide the necessary set of features required for analysis.  For
   example, modeling privacy -- for some definition of privacy -- is
   often a difficult task with tools like Tamarin and ProVerif.

   There may be multiple ways by which these obstacles are overcome.
   For example, the community might invest or otherwise contribute to
   the ongoing development and maintenance of these tools.  In general,
   they are often maintained by academic researchers, including graduate
   students, who leave the project or move on to other things over time.
   Like an critical open source project, these tools require consistent
   and reliable support to encourage continued maintenance and
   development to better fit the needs of the community.

   Beyond explicit tooling support, the amount of educational resources
   available for consumption, including examples, demos, running code,
   etc., could be improved and made more approachable for newcomers.
   While there exists plenty of learning material for these tools, they
   are often oriented towards those with a background or familiarity
   with formal methods.  Educational material oriented towards engineers
   is needed.

Wood                    Expires 14 September 2023               [Page 6]
Internet-Draft         Formal Analysis Challenges             March 2023

4.3.  Incentives

   Lack of incentives is a large barrier to adopting formal analysis in
   practice.  From a research perspective, there is often little
   incentive to work on formal analysis for "uninteresting" or "overly
   simple" protocols, including those that seem to be "obviously
   correct."  Publishing formal analysis with negative results, i.e.,
   which demonstrate that there are no problems with a technical
   specification, is often challenging.  And without proper publishing
   incentives, there is little incentive for academic researchers to
   spend time on this type of work.  Addressing this problem may require
   establishing a venue for more easily publishing formal analysis
   without compromising on the quality of peer review.  Such venue
   should make clear that publishing analysis of any type is
   appropriate, including formal models, pen and paper proofs, and so

   From the specification editor's perspective, sometimes analysis can
   seem unnecessary, perhaps because the object being specified is
   indeed "obviously correct" or that security considerations with
   proven interoperability seem sufficient.  However, as has been
   demonstrated, security considerations are not a suitable replacement
   for security analysis.  In general, the problem here seems to be that
   the type of analysis that would be sufficient to provide confidence
   in the specification is not clear.  The IETF and IRTF community needs
   guidance on what type of analysis is appropriate.  As obvious
   examples, cryptographic algorithms require analysis.  Network
   protocols such as TLS also require analysis, but of a different type.
   The community could work on collecting examples of formal analyses to
   use as guidance in determining the suitable amount of analysis.

4.4.  Complexity and Precision

   Specification complexity is a barrier to analysis.  Complexity makes
   it challenging to develop an accurate mental model for the problem
   being solved, which is necessary for defining and refining the threat
   model and desired security properties of a protocol.  Complexity
   makes the learning curve steep, deterring otherwise willing
   contributors from working on the analysis.  Complexity can be dealt
   with by breaking down specifications into smaller, purpose-specific
   pieces, where possible.  Beyond helping tame complexity, this might
   also help enable better reuse of existing analysis results.
   Complexity might also be dealt with by improving the presentation
   quality of specifications, e.g., by using consistent vocabulary
   across related specifications, including more discusson about
   intuition, and so on.

Wood                    Expires 14 September 2023               [Page 7]
Internet-Draft         Formal Analysis Challenges             March 2023

   Specifications also sometimes suffer from lack of precision.
   Naturally, as specifications are written in English, they are prone
   to misinterpretations by different people, especially those for whom
   English is not a native language.  While prose is useful for
   describing intution, it is often insufficient for rigorous technical
   details.  Lack of precision therefore makes analysis difficult since
   there lacks clarity on what is the exact object or syntax being
   specified.  Use of more rigorous specification language, e.g.,
   consistently presented and readable pseudocode, formal grammars,
   state machine descriptions, etc can all help improve the precision by
   which specifications are represented.  However, it's worth noting
   that sometimes precision can increase specification complexity.
   Balancing these two is not always easy in practice.

4.5.  Resource Limits

   Analysis is also impeded by a limitation of resources.  Formal
   analysis is not an easy task.  The tools, techniques, and
   methodologies for applying formal analysis vary in maturity, and the
   people generally capable of contributing such analyses are far fewer
   than the number required to analyze all known protocols.  Moreover,
   the domain expertise required to formulate and represent and describe
   a suitable threat model is often difficult to acquire for those that
   do have the skills to perform formal analysis.  For better or worse,
   specification editors are often not equipped to formulate problem
   statements, threat models, and security definitions.

   Specification editors can take steps to help bridge the gap between
   themselves and those capable of performing protocol design and
   analysis.  Some possible actions are below.

   1.  Identify and collaborate with domain experts who might offer
       expertise for their protocol.  If domain experts are unknown,
       consult the WG chairs or security area contributors for

   2.  Include the protocol's desired security properties and threat
       model in the protocol document.  This can be done in the security
       considerations or elsewhere, but including it somewhere helps
       give domain experts and reviewers a target for analysis.

   3.  Include known implementations of protocols somewhere alongside
       the protocol being developed.  Some analysis efforts focus on the
       gap between specifications and implementations, and reviewing
       implementations is an important part of assessing that gap.

Wood                    Expires 14 September 2023               [Page 8]
Internet-Draft         Formal Analysis Challenges             March 2023

   4.  Document all known gaps between the protocol specification and
       known formal analysis.  This helps ensure that the results of the
       analysis are properly represented to consumers of protocol
       specification documents.

   5.  Identify open issues or aspects of the protocol that require
       formal analysis during development of the protocol specification.
       One way to do this is to note that the entire draft is still a
       work in progress, whereas another way is to highlight specific
       properties of the protocol that require more analysis.

   Conversely, protocol designers and researchers can also take steps to
   bridge the gap between their skill set and the actual technical
   specifications.  Some possible actions are below.

   1.  Collaborate with protocol document editors to determine what are
       ongoing analysis tasks.  The end goal here is to minimize
       conflicts and competition that might emerge with different
       experts performing reviews.

   2.  Ensure that analysis work that requires running code, such as
       formal analyses using modeling tools such as ProVerif and
       Tamarin, are understandable and reproducible.  It should be
       possible for any contributor in the IETF to re-run the analysis
       and understand its results.

5.  Security Considerations

   This document discusses challenges for applying formal analysis to
   technical specifications produced by the IETF and IRTF.  It does not
   raise new security considerations.

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, March 1997,

   [RFC8174]  Leiba, B., "Ambiguity of Uppercase vs Lowercase in RFC
              2119 Key Words", BCP 14, RFC 8174, DOI 10.17487/RFC8174,
              May 2017, <>.

Wood                    Expires 14 September 2023               [Page 9]
Internet-Draft         Formal Analysis Challenges             March 2023

7.2.  Informative References

   [MLS]      Barnes, R., Beurdouche, B., Robert, R., Millican, J.,
              Omara, E., and K. Cohn-Gordon, "The Messaging Layer
              Security (MLS) Protocol", Work in Progress, Internet-
              Draft, draft-ietf-mls-protocol-18, 13 March 2023,

   [OHTTP]    Thomson, M. and C. A. Wood, "Oblivious HTTP", Work in
              Progress, Internet-Draft, draft-ietf-ohai-ohttp-07, 9
              March 2023, <

              Davidson, A., Iyengar, J., and C. A. Wood, "The Privacy
              Pass Architecture", Work in Progress, Internet-Draft,
              draft-ietf-privacypass-architecture-11, 6 March 2023,

   [ProVerif] Blanchet, B., "Modeling and Verifying Security Protocols
              with the Applied Pi Calculus and ProVerif", Foundations
              and TrendsĀ® in Privacy and Security vol. 1, no. 1-2, pp.
              1-135, DOI 10.1561/3300000004, 2016,

   [QUIC]     Iyengar, J., Ed. and M. Thomson, Ed., "QUIC: A UDP-Based
              Multiplexed and Secure Transport", RFC 9000,
              DOI 10.17487/RFC9000, May 2021,

   [RFC9000]  Iyengar, J., Ed. and M. Thomson, Ed., "QUIC: A UDP-Based
              Multiplexed and Secure Transport", RFC 9000,
              DOI 10.17487/RFC9000, May 2021,

   [Tamarin]  Cortier, V., Delaune, S., Dreier, J., and E. Klein,
              "Automatic generation of sources lemmas in Tamarin:
              Towards automatic proofs of security protocols1", Journal
              of Computer Security vol. 30, no. 4, pp. 573-598, DOI 
              10.3233/jcs-210053, August 2022,

   [TLS13]    Rescorla, E., "The Transport Layer Security (TLS) Protocol
              Version 1.3", RFC 8446, DOI 10.17487/RFC8446, August 2018,

Wood                    Expires 14 September 2023              [Page 10]
Internet-Draft         Formal Analysis Challenges             March 2023


   This document was influenced by conversations with many people that
   led to the UFMRG formation.

Author's Address

   Christopher A. Wood

Wood                    Expires 14 September 2023              [Page 11]