11:36:22 From Tony Li to Everyone: I have no audio. Is anyone speaking? 11:36:31 From Muhammad Usama Sardar to Everyone: me too 11:36:47 From Dan Jones to Everyone: I can hear you now! 11:36:55 From Sofía Celi to Everyone: we can hear you and see you 11:39:01 From Colin Perkins to Everyone: Can remote people hear me and see the slides? 11:39:09 From randy to Everyone: folk are speaking but audio unintelligible 11:39:18 From Benjamin Beurdouche | Mozilla to Everyone: Se the slides yes. Audio is quite bad 11:39:24 From Tony Li to Everyone: And we can see someone. 11:39:26 From Muhammad Usama Sardar to Everyone: we see the slides 11:39:34 From Muhammad Usama Sardar to Everyone: voice is not clear 11:39:44 From David Guzman to Everyone: audio is not clear 11:39:47 From Sofía Celi to Everyone: better 11:39:52 From Tony Li to Everyone: Yes, that helps 11:39:53 From Dan Jones to Everyone: Audio is better for me 11:39:56 From David Guzman to Everyone: better 11:40:42 From Marc Petit-Huguenin to Everyone: yes! 11:40:47 From randy to Everyone: hear colin well 11:41:06 From Tony Li to Everyone: We have video of your stomach. 11:41:35 From Muhammad Usama Sardar to Everyone: :) 11:41:57 From Tony Li to Everyone: When you turn away from the camera, we lose audio 11:48:29 From Benjamin Beurdouche | Mozilla to Everyone: Better now 11:48:34 From Tony Li to Everyone: Stand right there 11:48:41 From Marc Petit-Huguenin to Everyone: better now 11:48:48 From Dan Jones to Everyone: Audio is great from that position -- thank you 🙂 11:48:52 From Tony Li to Everyone: The split screen is not helpful 11:51:20 From Tony Li to Everyone: Formal specification would also seem to be beneficial 11:54:46 From Robert Lee to Everyone: Is it strictly necessary for the split-screen room camera thing to feature me so prominently? Are people super keen to see me listening to Jonathan? 11:55:50 From Colin Perkins to Everyone: The camera is “intelligent” - if you know how to persuade it to do otherwise, we can change it 11:57:46 From stephenfarrell to Everyone: good list 11:59:34 From stephenfarrell to Everyone: I'm not sure I agree with Carsten about the ordering of goals there 12:03:24 From Sofía Celi to Everyone: I can hear 12:03:36 From Sofía Celi to Everyone: yes 12:03:43 From randy to Everyone: intra-zoom works, of course 12:04:05 From Tony Li to Everyone: Formal specification would be a major accomplishment and a far lower bar than formal analysis and verification. 12:04:33 From Tony Li to Everyone: Even just for human to human communication, it would avoid a great deal of ambiguity. 12:04:40 From lenore to Everyone: Exactly! 12:04:50 From Muhammad Usama Sardar to Everyone: Agree with Tony 12:04:51 From stephenfarrell to Everyone: interesting: I think I think the opposite to tony 12:04:56 From Tony Li to Everyone: Also, publication of analysis as an RFC would be much easier to achieve. 12:04:57 From Jean Quilbeuf to Everyone: Just a quick remark: eBNF is formally specifying the accepted syntax. So in a sense, it is a formal description. 12:05:01 From Sofía Celi to Everyone: my thoughts: support all what Jonathan presented. I think for the publication side, we can organise a workshop. It is not only needed for IETF but for the community in general 12:05:40 From Tony Li to Everyone: Protocols need more than formal syntax. We also need to be able to express temporal properties. 12:06:05 From Tony Li to Everyone: Getting the entire IETF to formal analysis and verification might be very hard. 12:07:27 From Benjamin Beurdouche | Mozilla to Everyone: 1. We need a place to centralise the needs for analysis or verified implementation, wether it is for an algorithm, protocol or infrastructure 12:07:30 From Tony Li to Everyone: @StephenFarrell: Please expound 12:08:03 From Benjamin Beurdouche | Mozilla to Everyone: 2. Both analysis and verification will require either a formal spec or a formal model, which are the basis for everything 12:08:58 From Benjamin Beurdouche | Mozilla to Everyone: 1 is quite easy and already valuable 12:09:14 From Benjamin Beurdouche | Mozilla to Everyone: 2 requires much more work and is not generic 12:09:31 From tim to Everyone: yes 12:09:32 From Colin Perkins to Everyone: Can people hear Ken? 12:09:35 From Benjamin Beurdouche | Mozilla to Everyone: yes 12:09:37 From Sofía Celi to Everyone: yes 12:09:47 From Muhammad Usama Sardar to Everyone: we dont see you 12:16:57 From stephenfarrell to Everyone: /me would like to see how POODLE etc might have been preventerd (but doesn't think that'd have happened as SSL 3 predates all IETF work) 12:19:46 From Jonathan Hoyland to Everyone: So Bhargavan et al. did model weak ciphers across multiple modes in one of their TLS 1.3 analyses. I think it was the REFTLS paper? 12:20:14 From Jonathan Hoyland to Everyone: Oh, actually, maybe it was weak DH groups? 12:20:51 From Benjamin Beurdouche | Mozilla to Everyone: Generally, solving this is not a question of technology, it is a question of effort. 12:20:53 From Jonathan Hoyland to Everyone: But still, you could model them easily, but I think the only conclusion you could reach would be "If you (only) use weak ciphers you're stuffed" 12:21:11 From stephenfarrell to Everyone: so I thikn doing this kind of work alongside IETF work is great but assuming it replaces IETF work seems like not a good target 12:21:53 From Jonathan Hoyland to Everyone: I don't thnk it replaces any IETF work? I think it just adds another source of feedback into the WG 12:22:07 From Tony Li to Everyone: I would agree with that. Formal specification improves the RFC, it doesn't displace the English. 12:23:10 From Jonathan Hoyland to Everyone: Having a formal specification would be very useful if you wanted to make sure there was one description to rule them all, but of course, in practice, people would still do whatever they want. 12:23:20 From Jonathan Hoyland to Everyone: Sadly there are no Internet police. 12:28:36 From Dennis Jackson to Everyone: @Ken:, sorry if I missed this, is your specification of QUIC public / open source? 12:31:54 From stephenfarrell to Everyone: so I guess the question of when and how to beneficially inject formal methods into real world development processes is an interesting one 12:32:40 From Jonathan Hoyland to Everyone: I agree, maybe the first question we should try and answer is "when do we start with the formal stuff?" 12:32:45 From lenore to Everyone: Yes, the spec is open source 12:33:50 From Muhammad Usama Sardar to Everyone: audio is not clear 12:37:44 From Marc Petit-Huguenin to Everyone: We cannot hear the presenter. 12:38:19 From Tony Li to Everyone: I'll again suggest that the first step is to aim for formal specifications. That means teaching the IETF IVY or whatever else is appropriate. And then trying it out on a protocol or protocol change. 12:38:38 From Marc Petit-Huguenin to Everyone: yes 12:38:38 From Benjamin Beurdouche | Mozilla to Everyone: Much better yes 12:39:22 From Jonathan Hoyland to Everyone: I def. agree with Carsten. It's difficult to even get reviewers to look at your specification, let alone getting academics to look at it, let alone getting implementors to look at it. What can we do to make the models/specifications/proofs more accessible? Better education? Better tools? Better languages? 12:42:06 From Jonathan Hoyland to Everyone: @Tony Li, I think the reason people like me are pushing back on that is that, at least in the security area, we already have done specification, analysis, implementation, and verification. It's not a new field of study that we don't know how to do. It might not be widespread in other groups, but that doesn't mean doing more is out-of-scope / unreasonable. 12:42:31 From Marc Petit-Huguenin to Everyone: Cannot go wrong starting with better education. 12:42:44 From Tony Li to Everyone: No objection to that, but there's other low hanging fruit. 12:43:06 From Stephen McQuistin to Everyone: I guess a first step might be to bring in and socialise that learning from the security area? 12:43:55 From Jonathan Hoyland to Everyone: Yeah the lowest hanging fruit is probably providing a venue for discussing this. 12:45:44 From lenore to Everyone: KM: I don’t think the problem of formal specification is a closed one from the point of view of research. It is very hard to write a formal spec that is useful for formal verification or specification-based testing that is also interpretable for engineers. 12:47:07 From Tony Li to Everyone: Another useful educational step might be easily accessible examples. A formal specification of RIP might be helpful. 12:47:26 From Marc Petit-Huguenin to Everyone: yes 12:51:53 From Jonathan Hoyland to Everyone: Proving privacy properties in the tools we have currently is still pretty painful. Even by the usual standards of formal methods. 12:55:21 From Tony Li to Everyone: As a prospective consumer, yes this is interesting. 12:57:07 From Sofía Celi to Everyone: I support the creation of this RG 12:57:33 From Marc Petit-Huguenin to Everyone: Yes/Nothing I can see/I'll participate/Not sure. 12:58:11 From A.Winfield. to Everyone: Definitely interested in this. 12:58:14 From Javier Alejandro Bustos Jiménez to Everyone: (Yes/Nothing I can see/I'll participate/Not sure.)++ 12:58:59 From Sofía Celi to Everyone: Initial research directions: 1. think about formal methods on CFRG specs 2. continue the formal analysis of QUIC 12:59:08 From Benjamin Beurdouche | Mozilla to Everyone: Yes/Nothing/Yes/Collecting needs from WGs 13:01:24 From Sofía Celi to Everyone: thank you! 13:01:29 From Benjamin Beurdouche | Mozilla to Everyone: Thanks ! 13:01:35 From Muhammad Usama Sardar to Everyone: thanks 13:01:36 From Dan Jones to Everyone: Thanks 🙂