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

[Lucas Pardue <[e-mail]>]

To echo some of what Martin said, in the QUIC sphere I tend to see research
in papers or proceedings. Some of that research has identified issues with
a specific implementation, confirmed that the protocol behaves in
deployments as intended, etc etc. While not strict formal verification,
there is perhaps merit in collecting links to artefacts to help track _use
and deployment_ of a protocol after the initial design work was done and
the RFC cut.

Tangent: more of a tools discuss item probably - but having the list
managed directly in the datatracker isn't the most user-friendly thing. As
the number of items grows, it makes change management a bit tedious. It's
also not clear to me who has write access (I assume just chairs and ADs?).
A model where folks could propose their additions for review and approval
would help crowd source that slightly. Currently as a non-logged in user,
its not even obvious that the "Additional resources" field is such a
free-form field and that we'd likely welcome people volunteering their own
links there.

Cheers,
Lucas

On Wed, Mar 15, 2023 at 11:24 AM Martin Thomson <[e-mail]> wrote:

> 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
>
> --
> Edm mailing list
> [e-mail]
> https://www.iab.org/mailman/listinfo/edm
>