Internet-Draft UFM Sample June 2023
Farrell Expires 21 December 2023 [Page]
Network Working Group
Intended Status:
S. Farrell
Trinity College, Dublin

Usable Formal Methods Research Group Sample Problems


This draft provides reasoning as to why the Usable Formal Methods research group might benefit from having an IETF-relevant sample problem and describes one such (IMAP search). This is just an initial draft aiming to help move discussion forward so may be dropped or replaced by other drafts or the research group may prefer some non I-D format, or the research group may decide that sample problems aren't sufficiently useful. Early days, basically!

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 21 December 2023.

Table of Contents

1. Introduction

The Usable Formal Methods research group [ufmrg] has discussed the idea that having one or more "sample" problems might be useful for a number of reasons:

The hope is that this should help both sets of people better understand how formal methods may be useful for IETF work.

We posit that the following characteristics will help us identify one or more "good" sample problems:

We provide an initial description of one such problem in the section 2. If additional sample problems are proposed, those could be documented in other sections of this draft or in other documents. (To be clear: the author would welcome such text - the more the merrier for now.)

1.1. Success Criteria

If this approach succeeds we would expect:

  • to see formal methods proponents publish analyses of the sample problem(s)
  • to see IETF participants use/reference those analyses
  • to eventually see teams of IETF participants (with implementation/deployment experience) work together with proponents of formal method schemes to extend those analyses

If this approach doesn't get traction, we will most likely hear crickets.

1.2. Discussion Venues

The github repo for this draft is at:

PRs, issues etc are welcome. Substantive discussion however should for now at least be directed to the UFMRG mailing list:

3. Acknowledgments


4. Security Considerations

The security properties of the sample problem(s) are of course of interest but this draft itself will hopefully introduce no new security considerations unless we omit something from the description of the sample problem(s) that leads to erroneous conclusions about those security properties.

5. IANA Considerations

No changes to IANA processes are made by this memo.

6. Informative References

Melnikov, A., Ed. and B. Leiba, Ed., "Internet Message Access Protocol (IMAP) - Version 4rev2", RFC 9051, DOI 10.17487/RFC9051, , <>.
IRTF, "Usable Formal Methods Research Group", , <>.
IRTF, "May 2023 UFMRG online Interim meeting", , <>.

Appendix A. Changes from Earlier Versions

RFC editor: please remove this section.

Draft -00:

Author's Address

Stephen Farrell
Trinity College, Dublin