[Edm] Tracking (and distinguishing) formal analysis

[Christopher Wood <[e-mail]>]

Hi folks,

One of the helpful contributions of this group was changes to the datatracker that help track implementations of specifications (under "additional resources"). I've used this for a couple of specifications [0], and I hope others find them useful [1].

Implementations are not the only artifact that help with the development of specifications, though. Artifacts produced through formal analysis, such as executable models using tools like ProVerif or Tamarin and even pen-and-paper analyses, both change as the specification changes. As we develop specifications, new analyses appear over time, including after the final RFC is published.

Given that these artifacts have similar churn as implementations, and complement specifications in a similar way as well, I'm wondering if we ought to extend the available tags in the datatracker to keep track of these things. As a strawman proposal, what do folks think about adding a "related_analyses" tag (similar to the "related_implementations" tag) to the set of available tags in the datatracker? We might use it like so:

    related_analyses https://github.com/cloudflare/ohttp-analysis (Tamarin model of Oblivious HTTP)
    
Additionally, I'm wondering if we could also add a way to "flag" different resources so that they are easier to identify. Not everyone might know what a "Tamarin model" is. So for example, perhaps we could have colored label that says "analysis" (or something) next to the rendered item in the datatracker.

Good idea? Bad idea? I'm curious to hear your thoughts. If interested, maybe we could discuss this in 116?

Best,
Chris

[0] https://datatracker.ietf.org/doc/draft-ietf-ohai-ohttp/ as one example
[1] I don't know how useful these are to others. Do we have a way to determine how many times these links are clicked?