Re: [Edm] Tracking (and distinguishing) formal analysis

[Martin Thomson <[e-mail]>]

I tend to think that the draft should be citing work like what you reference.

Still, having references to implementations, analyses, or other relevant material, can still be valuable to collect the way you describe.  I think that this could help.  Given that this is a bag of tagged URLs, the bar for adding new types should be pretty low.

On that thought, I'd be OK with "explanatory blog posting" meeting the bar, as well, if you like.  We've had a ton of really good ones published over time for IETF work.  Sometimes they are the best way to get introductory-level background on the work.  Add those too.

(Tracking clicks might only offer the most vague approximation of "value".  Discussion might be a better indicator. Though in this case, the number of people qualified to read and contribute to that work is very much limited.)

On Wed, Mar 15, 2023, at 22:04, Christopher Wood wrote:
> 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?
> -- 
> Edm mailing list
> [e-mail]
> https://www.iab.org/mailman/listinfo/edm