[{"author": "Jonathan Hoyland", "text": "

Surely we should just provide a Tamarin model.

", "time": "2022-07-26T19:00:14Z"}, {"author": "Lucas Pardue", "text": "

I want an \"RF-C\" ML bot that can just make the spec based on the keywords and title

", "time": "2022-07-26T19:01:19Z"}, {"author": "Lucas Pardue", "text": "

\"XYZ over QUIC, using no extension frames\"

", "time": "2022-07-26T19:01:49Z"}, {"author": "Jeffrey Haas", "text": "

We're still having the usual cookie break issue and people are lingering in the halls.

", "time": "2022-07-26T19:02:03Z"}, {"author": "Colin Perkins", "text": "

We'll give it a couple of minutes

", "time": "2022-07-26T19:03:02Z"}, {"author": "Lucas Pardue", "text": "

yes

", "time": "2022-07-26T19:04:24Z"}, {"author": "Jeffrey Haas", "text": "

Also previously seen in IETF specifications: XDR, thrift.

", "time": "2022-07-26T19:12:57Z"}, {"author": "Jeffrey Haas", "text": "

and, of course, asn.1

", "time": "2022-07-26T19:14:09Z"}, {"author": "Joerg Ott", "text": "

quite a bit of this is just about syntax, which is the easy part

", "time": "2022-07-26T19:15:57Z"}, {"author": "Joerg Ott", "text": "

well: easier

", "time": "2022-07-26T19:16:13Z"}, {"author": "Colin Perkins", "text": "

Also, not just syntax

", "time": "2022-07-26T19:17:06Z"}, {"author": "Joerg Ott", "text": "

(was referring to XDR, ASN.1, ...)

", "time": "2022-07-26T19:17:30Z"}, {"author": "George Michaelson", "text": "

Jeffrey Haas said:

\n
\n

and, of course, asn.1

\n
\n

It's lovely that we kept the .1 even though we went through DER, BER and at least one other form of rep. So .. its all ASN.1 but not ASN1.bis or ASN1.ter

", "time": "2022-07-26T19:17:32Z"}, {"author": "Jonathan Hoyland", "text": "

The issue with having a fixed syntax is that the first thing people will do is complain that it's not expressive enough, whilst simultaneously complaining it's too expressive.

", "time": "2022-07-26T19:17:35Z"}, {"author": "Colin Perkins", "text": "

Note at https://notes.ietf.org/notes-ietf-114-anrw

", "time": "2022-07-26T19:17:56Z"}, {"author": "Jeffrey Haas", "text": "

The asn.1 fun is partially about how serialization format was considered a separate item from the language.

", "time": "2022-07-26T19:19:44Z"}, {"author": "Jeffrey Haas", "text": "

We have similar considerations at the moment with how YANG can be serialized over different mechanisms in different formats.

", "time": "2022-07-26T19:20:21Z"}, {"author": "Lucas Pardue", "text": "

i'm now reminded of the \"fun\" I had developing user interfaces in UML - https://lucaspardue.com/wp-content/uploads/2014/04/states_5.png

\n
", "time": "2022-07-26T19:20:35Z"}, {"author": "Lucas Pardue", "text": "

https://lucaspardue.com/2014/04/22/uml-modelling-user-interfaces-part-1-hierarchy-and-navigation/

", "time": "2022-07-26T19:21:01Z"}, {"author": "Rich Salz", "text": "

ASN.1 was naively optimistic; folks creating it thought there would be an ASN.2

", "time": "2022-07-26T19:21:07Z"}, {"author": "Jeffrey Haas", "text": "

When the author of the mechanism admits it is very fluid, that means at best you have nice stencils you can use for your drawing tool but not necessarily much else. :-)

", "time": "2022-07-26T19:21:36Z"}, {"author": "George Michaelson", "text": "

I'm glad he said isomorphisms, I felt saying \"defined by an FSM\" was an uneccessary restriction

", "time": "2022-07-26T19:21:37Z"}, {"author": "Jeffrey Haas", "text": "

The 'read between the lines' issue prevalent in RFCs

", "time": "2022-07-26T19:24:06Z"}, {"author": "George Michaelson", "text": "

I also think he just said that even Normative RFC language is not an isomorphism to an FSM

", "time": "2022-07-26T19:24:22Z"}, {"author": "Jonathan Hoyland", "text": "

There's a key step missing here. Defining the security properties. What is an \"attack\" depends on what the spec is trying to protect you from.

", "time": "2022-07-26T19:24:23Z"}, {"author": "Jeffrey Haas", "text": "

^

", "time": "2022-07-26T19:24:53Z"}, {"author": "Jonathan Hoyland", "text": "

My favourite one is the ORIGIN Frame RFC which uses the word \"origin\" with at least three different meanings (in different contexts).

", "time": "2022-07-26T19:25:47Z"}, {"author": "George Michaelson", "text": "

Wait: He's a formal-methods person and he just said \"Heuristic\" HERESY!!!

", "time": "2022-07-26T19:27:00Z"}, {"author": "Lucas Pardue", "text": "

how about the word frame Jonathan? that's quite overloaded too

", "time": "2022-07-26T19:27:22Z"}, {"author": "Jonathan Hoyland", "text": "

Tools like Tamarin and ProVerif rely heavily on heuristics, because the problems are only semi-decidable.

", "time": "2022-07-26T19:27:34Z"}, {"author": "George Michaelson", "text": "

This missing FIN thing.. isn't it an argument to \"the RFC could have been better written\" ?

", "time": "2022-07-26T19:35:34Z"}, {"author": "George Michaelson", "text": "

implicit behaviour and ambiguities are inherently unhelpful

", "time": "2022-07-26T19:35:53Z"}, {"author": "George Michaelson", "text": "

so as a proof of concept of \"well written\" this feels like quite a strong test: easy to FSMise, is a good spec

", "time": "2022-07-26T19:36:12Z"}, {"author": "Olaf Kolkman", "text": "

I was thinking the same thing - one step further - this could be integrated in the WG processes, as a sort last-call tool.

", "time": "2022-07-26T19:36:35Z"}, {"author": "Jonathan Hoyland", "text": "

Well many protocols, e.g. TLS cannot be described (correctly) with an FSM, so I'm not sure that would help.

", "time": "2022-07-26T19:36:43Z"}, {"author": "Michael T\u00fcxen", "text": "

The text CLOSE_WAIT--- FIN! ---> LAST-ACK is from the TCP RFC.

", "time": "2022-07-26T19:36:50Z"}, {"author": "Michael T\u00fcxen", "text": "

In particular, from handling the RECEIVE primitive. And in that case there should be no state transition...

", "time": "2022-07-26T19:37:26Z"}, {"author": "Jeffrey Haas", "text": "

Having such tools part of a step similar to a \"grammar check\" would certainly be useful. If the markup step that produces the procedural elements for the identified fsm were to be carried into the rfc xml, it means you can iterate over your human readable text until the correct fsm can be identified from the text.That basically means we end up training the humans to write text the tool likes. It likely is more declarative and, possibly, easier to read.

", "time": "2022-07-26T19:41:17Z"}, {"author": "George Michaelson", "text": "

I was always attracted to Milners CCS. I wonder if things which won't express well in an FSM can be represented in CCS or derived systems better?

", "time": "2022-07-26T19:43:26Z"}, {"author": "Jonathan Hoyland", "text": "

IIUC CCS is more expressive, so yes.

", "time": "2022-07-26T19:44:35Z"}, {"author": "George Michaelson", "text": "

Jeffrey Haas said:

\n
\n

Having such tools part of a step similar to a \"grammar check\" would certainly be useful. If the markup step that produces the procedural elements for the identified fsm were to be carried into the rfc xml, it means you can iterate over your human readable text until the correct fsm can be identified from the text.That basically means we end up training the humans to write text the tool likes. It likely is more declarative and, possibly, easier to read.

\n
\n

He went there

", "time": "2022-07-26T19:45:26Z"}, {"author": "Jeffrey Haas", "text": "

Glad he did.

", "time": "2022-07-26T19:45:39Z"}, {"author": "Jonathan Hoyland", "text": "

Tamarin is based on Pattern-Matching Recursion Schemes that are (much) more expressive than FSMs, and it's difficult to fully describe TLS in PMRSs.

", "time": "2022-07-26T19:45:50Z"}, {"author": "Jeffrey Haas", "text": "

If the tools interactively guide the humans to help with the generated stuff, among other things it helps people to whom English is not a first language.

", "time": "2022-07-26T19:46:14Z"}, {"author": "George Michaelson", "text": "

I'm going to be honest I was skeptical, but I come out of this one less skeptical. I think he's adding value.

", "time": "2022-07-26T19:46:19Z"}, {"author": "Jeffrey Haas", "text": "

As someone who didn't study formal systems in school and hasn't kept up with natural language processing, it was nice to see that the tooling can get a good part of the way therel.

", "time": "2022-07-26T19:47:49Z"}, {"author": "Jeffrey Haas", "text": "

Even if it's just a form of \"the computer is the developer and can they implement the rfc\"

", "time": "2022-07-26T19:48:09Z"}, {"author": "Lucas Pardue", "text": "

or we write the diagrams in SVG and use XML attributes to help!

", "time": "2022-07-26T19:49:29Z"}, {"author": "Jeffrey Haas", "text": "

There's sometimes the issue that sometimes attempts to clean up text and turn them into FSMs that it doesn't always lead to cleaner rfcs. I offer BGP RFC 4271 as an example.

", "time": "2022-07-26T19:49:54Z"}, {"author": "Rob Austein", "text": "

I want a tool that reports things like \"there is no plausible way to implement RFC 793 without goto\"

", "time": "2022-07-26T19:52:01Z"}, {"author": "Rich Salz", "text": "

@Colin Perkins require the queue tool to be used? Jonathan's been waiting for awhile.

", "time": "2022-07-26T19:54:55Z"}, {"author": "Jeffrey Haas", "text": "

FSMs with states can be expressed with sub-states. Unexplored sub-states in a deterministic FSM are often a pointer to bugs. (again, I offer BGP)

", "time": "2022-07-26T19:57:46Z"}, {"author": "Jonathan Hoyland", "text": "

@Jeffrey Haas some FSMs with states can be represented that way. If the number of tokens is finite that can be done, but if the number of tokens is infinite (or even very large) then you can't express it with sub-FSMs

", "time": "2022-07-26T19:59:36Z"}, {"author": "Jeffrey Haas", "text": "

Even for modestly large, it becomes impractical for human comprehension. That was part of our findings in the BGP work. However, it also was good for illustrating that elements that contributed to sub-states as inputs were sources of ambiguity and bugs. Somewhat by proxy, large numbers of sub-states were a sign of hidden complexity that still needed deterministic handling.

", "time": "2022-07-26T20:07:32Z"}, {"author": "Jeffrey Haas", "text": "

One thing I love about the current presentation is the usual tie-in as to whether a cleanly logical bit of text would let us map nicely into easily readable language for a native speaker. (See also, English sucks...)

", "time": "2022-07-26T20:10:28Z"}, {"author": "Jonathan Hoyland", "text": "

The main thing that can't be done is dependencies between different parts of the protocol. For example checking that agreed parameter values are the ones that are used. Even saying \"is the nonce I sent the same as the nonce I got back\" is not possible in a true FSM, unless you have two states per value in your nonce space.

", "time": "2022-07-26T20:10:30Z"}, {"author": "Jonathan Hoyland", "text": "

(But yes, I do have to agree that English is horribly ambiguous)

", "time": "2022-07-26T20:11:38Z"}, {"author": "Jeffrey Haas", "text": "

Your one phrase example on nonces both showing the mess and that for a native speaker it's \"easy\". :-)

", "time": "2022-07-26T20:12:16Z"}, {"author": "Jeffrey Haas", "text": "

Great presentation, Yu-Chuan. Thanks.

", "time": "2022-07-26T20:18:24Z"}, {"author": "Lucas Pardue", "text": "

how does the IESG's definition of quality line up to slide 10's definition?

", "time": "2022-07-26T20:32:25Z"}, {"author": "Rich Salz", "text": "

What IESG definition of quality?

", "time": "2022-07-26T20:33:05Z"}, {"author": "Rich Salz", "text": "

(serious question)

", "time": "2022-07-26T20:33:23Z"}, {"author": "Lucas Pardue", "text": "

I see a relatively high frequency of \"thank you for a well-written document\" in IESG reviews - I hope you're not suggesting that's IESG boilerplate :P

", "time": "2022-07-26T20:35:29Z"}, {"author": "Randy Bush", "text": "

@rich: we have relied on sufficient for interop. this is a long way from a model that can be evaluated with any formality

", "time": "2022-07-26T20:35:41Z"}, {"author": "Randy Bush", "text": "

did celeste's and harry's implementations interop? and we can not even formalise 'interop' in a formally complete and testable fashion.

", "time": "2022-07-26T20:37:52Z"}, {"author": "Rich Salz", "text": "

ack to both Randy and Lucas.

", "time": "2022-07-26T20:38:12Z"}, {"author": "Lucas Pardue", "text": "

what's the line between \"easy to understand\" and \"better off documented in other literature artforms\"

", "time": "2022-07-26T20:39:48Z"}, {"author": "Rob Austein", "text": "

Basic test has been whether multiple implementer brains parse the text the same way, as demonstrated by interop testing of their respective implementations. Sometimes if we're lucky we have someone with a wicked sense of humor who enjoys fuzz testing the spec by obeying the letter while violating the spirit wherever s/he can. But it's still just human interpretation.

", "time": "2022-07-26T20:42:10Z"}, {"author": "Jonathan Hoyland", "text": "

Get a non-expert to implement it. You'd be amazed at the kind of things n00bs will get wrong.

", "time": "2022-07-26T20:43:34Z"}, {"author": "Rich Salz", "text": "

A non-native speaker is almost as good for this.

", "time": "2022-07-26T20:44:33Z"}, {"author": "Jonathan Hoyland", "text": "

Also, it's probably a good way to train people in writing crypto code.

", "time": "2022-07-26T20:44:55Z"}, {"author": "Rich Salz", "text": "

A problem is they rarely point out problems, thinking it's their fault for being bad English speakers.

", "time": "2022-07-26T20:45:06Z"}, {"author": "Lucas Pardue", "text": "

to rephrase my questions: I've seen people ask to document deeply aspects of HTTP in a spec that extends it minimally. That seems beyond the remit of a specification. The understanding of the entire protocol needs all of the other things

", "time": "2022-07-26T20:45:10Z"}, {"author": "Randy Bush", "text": "

and how do you say \"constant time\" and \"constant power\" formally? :)

", "time": "2022-07-26T20:45:23Z"}, {"author": "George Michaelson", "text": "

Again, thanks to the ANRW PC for selecting really nice content to muse over, kept my interest all the way through

", "time": "2022-07-26T20:45:27Z"}, {"author": "Lucas Pardue", "text": "

+1

", "time": "2022-07-26T20:45:42Z"}, {"author": "Rich Salz", "text": "

+many

", "time": "2022-07-26T20:45:49Z"}, {"author": "Jonathan Hoyland", "text": "

Hear hear

", "time": "2022-07-26T20:45:49Z"}, {"author": "Jeffrey Haas", "text": "

++

", "time": "2022-07-26T20:46:02Z"}, {"author": "George Michaelson", "text": "

I think the isomorphic/strictly equivalent thing might be a road to say \"heres a bunch of techniques to write a spec which is better to formally verify and implement\" without having to be proscriptive which one is used. The tools approach, to a bunch of tests, I would see as something which worked in a CI document management method. Modify the draft? it does a bunch of check tasks, even human mediated heuristics, tells you a score

", "time": "2022-07-26T20:48:34Z"}, {"author": "Lucas Pardue", "text": "

on consistency, shoutout to HTTP folks that have been writing (and enforcing) style guides documented at - https://httpwg.org/admin/editors/style-guide

", "time": "2022-07-26T20:49:03Z"}, {"author": "George Michaelson", "text": "

I really struggled with this kind of CI check on a patch for a while, but watching it nitpick me for my code attempts really told me how I was working wrongly

", "time": "2022-07-26T20:49:10Z"}, {"author": "Rich Salz", "text": "

Julian is a machine. Literally.

", "time": "2022-07-26T20:49:25Z"}, {"author": "Lucas Pardue", "text": "

I started trying to implement HTTP style checks in Vale but ran out of time

", "time": "2022-07-26T20:49:31Z"}, {"author": "George Michaelson", "text": "

Julia is a machine, figurarively and literally

", "time": "2022-07-26T20:49:40Z"}, {"author": "Rich Salz", "text": "

lol

", "time": "2022-07-26T20:49:46Z"}, {"author": "Rob Austein", "text": "

This cognitive load point is important. Years ago I read editorial guidelines for a SF mag, one of their guidelines was \"you get to introduce one hard concept per story, after that you lose your audience\"

", "time": "2022-07-26T20:49:48Z"}, {"author": "George Michaelson", "text": "

Oh no.. language wars on a slide. Noooo

", "time": "2022-07-26T20:50:46Z"}, {"author": "Lucas Pardue", "text": "

pyhton2 or 3?

", "time": "2022-07-26T20:51:10Z"}, {"author": "Rob Austein", "text": "

py2 is dead

", "time": "2022-07-26T20:51:19Z"}, {"author": "George Michaelson", "text": "

I really increasingly regret we didn't go with S-Expressions. At the time I was meh, but now I am more 'wish we had'

", "time": "2022-07-26T20:51:24Z"}, {"author": "Rob Austein", "text": "

Heh. I tried, George you were in the room :)

", "time": "2022-07-26T20:51:42Z"}, {"author": "George Michaelson", "text": "

(in PKI)

", "time": "2022-07-26T20:51:45Z"}, {"author": "George Michaelson", "text": "

yes. you did, and you were right

", "time": "2022-07-26T20:51:51Z"}, {"author": "Randy Bush", "text": "

cfrg intra-rg review is much more thorough than wg..ietf..directorate review of ietf docs.

", "time": "2022-07-26T20:56:08Z"}, {"author": "Colin Perkins", "text": "

Please use the meetecho queue so we can manage local and remote questions

", "time": "2022-07-26T20:56:48Z"}, {"author": "Jonathan Hoyland", "text": "

I've been pretty enamoured of DY*'s approach lately.Formally verified implementation and formally analysed spec from one document.https://hal.inria.fr/hal-03178425/document

", "time": "2022-07-26T20:58:22Z"}, {"author": "Jonathan Hoyland", "text": "

The spec is law?

", "time": "2022-07-26T21:01:25Z"}, {"author": "Rob Austein", "text": "

The fact that some reference implementations suck does not mean that all do. Strongly support reference implementations as I don't believe that it runs until I see it boot. Whenever there are multiple sources of truth (text vs pseudo code vs reference code) the spec has to state which one is authoritative :)

", "time": "2022-07-26T21:02:29Z"}, {"author": "George Michaelson", "text": "

I absolutely think Colin is on the money with pursuing this. I think its worth it, and would add value.

", "time": "2022-07-26T21:02:36Z"}, {"author": "Colin Perkins", "text": "

https://notes.ietf.org/notes-ietf-114-anrw

", "time": "2022-07-26T21:02:56Z"}, {"author": "Rich Salz", "text": "

I think CFRG gets interested academics to do deep studies, and their motivation is ..not sure what adjective... IETF/directorate/etc reviews are hard to get similar enthusiasm if it's not your particular WG.

", "time": "2022-07-26T21:03:24Z"}, {"author": "Rich Salz", "text": "

I really enjoyed this and look forward to seeing what next steps happen.

", "time": "2022-07-26T21:03:37Z"}, {"author": "Jonathan Hoyland", "text": "

@MeetEcho: Adjourned

", "time": "2022-07-26T21:03:47Z"}]