Skip to main content

Minutes IETF117: ufmrg: Tue 00:30

Meeting Minutes Usable Formal Methods Research Group (ufmrg) RG
Date and time 2023-07-25 00:30
Title Minutes IETF117: ufmrg: Tue 00:30
State Active
Other versions markdown
Last updated 2023-07-24



Agenda Bash (chairs, 10)

[Agenda survived unscathed.]

Sample problems for UFMRG (Farrell, 15)

Collin Perkins: Likes this idea, IMAP seems okay, but this could be too
Marc Petit-Huguenin: IMAP isn't that complex, especially the search
subset. Might want something more complex. This seems to be a reasonable
size. Issues only found in the ABNF.

Chair: how many sample problems? What complexity?

Collin P.: Not too many, likely to have a range of problems of different
complexity problems. Something from a tutorial problem, to a more
complex problem. Maybe ones at different diffculty levels.

Stephen: Something that might be interesting for a grad student to
explore with a tool

Phil H-B: What are you going to prove is a key part of the

Chris I.: Do you want to be able to test running generated code? What's

Barnes: Some part of OAUTH was mentioned, maybe tractable in size, and

Alessandro ghendi: as a non experienced person, knowing what's too hard
or too easy is hard to tell. But with QUIC, some sample debuging events,
where just a packet can jam up the system at the right time, it might be
interesting what the right part is.

Stephen: for a grad student; but less than 6-months.

Hoyland: scale of detail matters; to get down to security properties,
you need to get down to like the level of inputs to hash functions

Yaron: missed it

Pete Resnick: retransmit timers or slow start of tcp?

Mark P-H: TFTP (which was on the mail list); its simple enough, but its
a good scale of protocol to check. There is a known bug in there.

David Schinazy: Bug in TCP cubic. Google found the bug in cubic code by
building unit tests for cubic.

Wes H: IMAP (especially search) depends what's in the users box. SNMP v3
is also an IETF protocol with similar

Collin P: maybe write down not just the problem, but the properties that
we would like to explore.

Mark P-H: We should focus on the "useable" part; so that we get to the
point where IETF folks are asking for support to use tools to do formal
analysis. "Useable" is in the eye of the beholder, have to be able to
convince people this can be done.

Lucas P: I definitely don't want to do stuff. Would love to have
analysis of multipath QUIC thats happening, but thats likely too
complex. Compression issues, q-pack compression scheme, and the
complexities of adding compression to protocols.

Chair: Volunteer to write up a challenge problem.
Hannes: volunteer to write up DPOP.

Isabelle (Buday, 20)

Hoyland: Tamarin can takes days and many gigabytes to analyze a model;
adding 2x on that would be expensive/prohibitive. Is there reason to
pick Isabelle over Tamarin?

Gergely B: Well there is room for research in this area

Collin P: Wondering about the gap between how we document IETF protocols
and how Isabelle and similar methods need protocols described.

Hannes: these tools can be more accessible and you can be useful in them
faster than you might think.

chair: should we be doing intermediate or master level training?

Next steps/actions (chairs, 10)

Planning IETF 118 training - we'll discuss on the list but the plan is
to try arrange a session for the Sunday before IETF118 in Prague