Sorry I sent them so late!
", "time": "2023-05-24T15:03:28Z"}, {"author": "Felix Linker", "text": "I can try to take some notes, too. Sorry, browser froze.
", "time": "2023-05-24T15:04:45Z"}, {"author": "Talia Ringer", "text": "Just want to say hello, since I haven't been to one of these before---I'm Talia and I'm a UIUC professor working on tools to make it easier to formally prove things about software systems
", "time": "2023-05-24T15:10:03Z"}, {"author": "Colin Perkins", "text": "Welcome!
", "time": "2023-05-24T15:10:36Z"}, {"author": "Felix Linker", "text": "Hi Talia!
", "time": "2023-05-24T15:11:23Z"}, {"author": "Felix Linker", "text": "@Stephen: What workshop were you referring to?
", "time": "2023-05-24T15:11:31Z"}, {"author": "Jonathan Hoyland", "text": "ANRW is the IRTF's yearly conference / workshop thing
", "time": "2023-05-24T15:12:04Z"}, {"author": "Colin Perkins", "text": "", "time": "2023-05-24T15:12:17Z"}, {"author": "Stephen Farrell", "text": "Hi Talia, and thanks Felix!
", "time": "2023-05-24T15:13:54Z"}, {"author": "Stephen Farrell", "text": "BTW, in case people are wondering, we do have non-crypto topics coming up:-)
", "time": "2023-05-24T15:14:17Z"}, {"author": "Stephen Farrell", "text": "the RFC I was asking about there was https://datatracker.ietf.org/doc/rfc9180/
", "time": "2023-05-24T15:18:45Z"}, {"author": "Christopher Patton", "text": "Wowwww what a huge case study!
", "time": "2023-05-24T15:21:41Z"}, {"author": "Stephen Farrell", "text": "anyone have a useful reference for this work? I can ask at the end, but maybe someone knows now
", "time": "2023-05-24T15:24:17Z"}, {"author": "Christoph Egger", "text": "not really yet
", "time": "2023-05-24T15:24:33Z"}, {"author": "Stephen Farrell", "text": "fair enough:-)
", "time": "2023-05-24T15:24:44Z"}, {"author": "Christoph Egger", "text": "we should get something written and out soon but ..
", "time": "2023-05-24T15:24:50Z"}, {"author": "Stephen Farrell", "text": "just shoot a mail to the list whenever is fine
", "time": "2023-05-24T15:25:47Z"}, {"author": "Bas Spitters", "text": "@Stephen hpke in hacspec
\nhttps://cryspen.com/hpke-spec/hpke/index.html
This is probably something we should add to the \"Usability Issues\" talk.
", "time": "2023-05-24T15:30:05Z"}, {"author": "Jonathan Hoyland", "text": "Toolchains.
", "time": "2023-05-24T15:30:11Z"}, {"author": "Jonathan Hoyland", "text": "I think this is more \"model checking\"
", "time": "2023-05-24T15:31:28Z"}, {"author": "Christoph Egger", "text": "code is \"just\" specification in that sense, not something you want to run
", "time": "2023-05-24T15:31:51Z"}, {"author": "Christopher Brzuska", "text": "Here is a link to the SSP analysis of Yao's Garbling scheme: https://eprint.iacr.org/2021/1453
", "time": "2023-05-24T15:32:28Z"}, {"author": "Stephen Farrell", "text": "is this the right link for rosette? https://emina.github.io/rosette/
", "time": "2023-05-24T15:46:10Z"}, {"author": "Stephen Farrell", "text": "I assume it's not this one:-) https://roserosette.org/
", "time": "2023-05-24T15:46:30Z"}, {"author": "Jonathan Hoyland", "text": "It's the first one
", "time": "2023-05-24T15:46:39Z"}, {"author": "Talia Ringer", "text": "Agreed there's too much emphasis on end-to-end formal verification, but starting from unit tests and just getting stronger guarantees for important or commonly used parts of a program is huge and such a good starting point
", "time": "2023-05-24T15:51:17Z"}, {"author": "Talia Ringer", "text": "like, given most people are writing unit tests, starting from that and saying \"well you can get something stronger than your unit tests for those same parts of your program\" is going to be a good selling point
", "time": "2023-05-24T15:51:59Z"}, {"author": "Talia Ringer", "text": "esp. given that once you have a formal spec, you can also use it to generate more tests...so you can get free, quick returns coupled with longer-term returns with more investment
", "time": "2023-05-24T15:52:36Z"}, {"author": "Jonathan Hoyland", "text": "One important thing I found with Rosette when I tried it, is the documentation is really good.
", "time": "2023-05-24T15:52:42Z"}, {"author": "Marc Petit-Huguenin", "text": "Related to what was just said: Zave, P. and F. Park, \"Experiences with Protocol Description\", 2011 https://www.researchgate.net/profile/Pamela_Zave/publication/266230560_Experiences_with_Protocol_Description/links/56eaf9fb08ae9dcdd82a6590.pdf
", "time": "2023-05-24T15:54:00Z"}, {"author": "Nikita Borisov", "text": "having trouble with mic, will ask bob offline :-/
", "time": "2023-05-24T15:54:54Z"}, {"author": "Yaron Sheffer", "text": "I probably missed it during the talk: did the tool translate his Python into Racket, or did he have to do it by hand?
", "time": "2023-05-24T15:55:14Z"}, {"author": "Carsten Bormann", "text": "he did it by hand
", "time": "2023-05-24T15:55:32Z"}, {"author": "Yaron Sheffer", "text": "TY
", "time": "2023-05-24T15:55:37Z"}, {"author": "Jonathan Hoyland", "text": "That sounded like a promise to me :Joy:
", "time": "2023-05-24T15:55:40Z"}, {"author": "Talia Ringer", "text": "need to head out, but enjoyed this
", "time": "2023-05-24T16:00:39Z"}, {"author": "Carsten Bormann", "text": "Hmm, IMAP and its UIDs are seriously arcane
", "time": "2023-05-24T16:03:54Z"}, {"author": "Colin Perkins", "text": "Some of my colleagues were using POP3 as an example, because it's small scale and well specified. IMAP might be less arcane - it's at least more currently used.
", "time": "2023-05-24T16:05:08Z"}, {"author": "Christopher Wood", "text": "I don't have any self-contained and known incorrect examples that don't have a heavy crypto element to it, but I'll give it some thought and send a message to the list if anything pops out the other end.
", "time": "2023-05-24T16:11:30Z"}, {"author": "Jonathan Hoyland", "text": "@Marc Are you talking about RFC 3261 https://www.rfc-editor.org/rfc/rfc3261 ?
", "time": "2023-05-24T16:12:56Z"}, {"author": "Marc Petit-Huguenin", "text": "yes
", "time": "2023-05-24T16:13:03Z"}, {"author": "Marc Petit-Huguenin", "text": "RFC 6026 is the fixx
", "time": "2023-05-24T16:13:33Z"}, {"author": "Jonathan Hoyland", "text": "Very few
", "time": "2023-05-24T16:14:13Z"}, {"author": "Carsten Bormann", "text": "This!
", "time": "2023-05-24T16:14:34Z"}, {"author": "Christopher Patton", "text": "I've always read Security Considerations as \"these are the security properties we intend the system to have\"
", "time": "2023-05-24T16:15:52Z"}, {"author": "Christopher Patton", "text": "Is that about right?
", "time": "2023-05-24T16:16:01Z"}, {"author": "Jonathan Hoyland", "text": "That's what I use them for, so at least sometimes
", "time": "2023-05-24T16:17:04Z"}, {"author": "Carsten Bormann", "text": "3552 Guidelines for Writing RFC Text on Security Considerations. E.
\n Rescorla, B. Korver. July 2003. (Format: TXT, HTML) (Updated by
\n RFC8996) (Also BCP0072) (Status: BEST CURRENT PRACTICE) (DOI:
\n 10.17487/RFC3552)
Code correctness vs. design correctness
", "time": "2023-05-24T16:19:33Z"}, {"author": "Stephen Farrell", "text": "wrt rfc3552, updating that would be a fairly major thing, for reasons nothing to do with formalisms (and it's been tried a couple of times without producing useful output)
", "time": "2023-05-24T16:22:26Z"}, {"author": "Felix Linker", "text": "Yes. I read it and it's pretty alright. I don't think a missing BCP is the source of the problem for \"hard to use\" security considerations.
", "time": "2023-05-24T16:23:09Z"}, {"author": "Christopher Patton", "text": "I would love to not have to write pen-and-paper proofs.
", "time": "2023-05-24T16:24:36Z"}, {"author": "Christopher Patton", "text": "But from where I sit today, it feels like my only option. (Which is why I'm here :D)
", "time": "2023-05-24T16:25:02Z"}, {"author": "Stephen Farrell", "text": "does anyone love pen and paper proofs and want to disagree? if so, now's an ideal chance!
", "time": "2023-05-24T16:25:05Z"}, {"author": "Colin Perkins", "text": "Are we thinking about building tools or about identifying classes of usability issues?
", "time": "2023-05-24T16:26:03Z"}, {"author": "Guido Schmitz", "text": "Pen and paper proofs enable you to go beyond the capabilities of current tools.
", "time": "2023-05-24T16:26:52Z"}, {"author": "Christopher Patton", "text": "Another reason: The quality of pen-and-proofs varies extremely widely.
", "time": "2023-05-24T16:27:04Z"}, {"author": "Guido Schmitz", "text": "But I agree that from a usability/verifiability perspective, mechanized proofs are certainly better.
", "time": "2023-05-24T16:28:11Z"}, {"author": "Christopher Wood", "text": "Do you think the quality of machine checkable proofs would be any different?
", "time": "2023-05-24T16:28:12Z"}, {"author": "Christopher Patton", "text": "I think it has the potential to be better.
", "time": "2023-05-24T16:28:46Z"}, {"author": "Guido Schmitz", "text": "With a machine checkable proof, you at least get guarantees that the argument is consistent in itself.
", "time": "2023-05-24T16:28:57Z"}, {"author": "Christopher Patton", "text": "It's kind of the difference between writing and programming
", "time": "2023-05-24T16:29:00Z"}, {"author": "Christopher Patton", "text": "when programming it's easier (and often required) to be consistent. When you're writing English the world is your oyster.
", "time": "2023-05-24T16:29:28Z"}, {"author": "Nikita Borisov", "text": "I remember an assertion that, in math, a huge fraction of published proofs are wrong, and a significant fraction of them are proving false things
", "time": "2023-05-24T16:29:29Z"}, {"author": "Lino Demasi", "text": "Just as a note, ISO recently published an updated version of ISO 29128 - Verification of Cryptographic Protocols. Pen and Paper proofs were included in the previous version, but were removed in favour of only considering computer verified proofs.
", "time": "2023-05-24T16:29:35Z"}, {"author": "Nikita Borisov", "text": "but to Guido's point, pen and paper are still involved at trying to argue that what the machine is proving is what you actually want.
", "time": "2023-05-24T16:30:15Z"}, {"author": "Christopher Wood", "text": "+1 Nikita -- they complement each other nicely.
", "time": "2023-05-24T16:30:48Z"}, {"author": "Christopher Patton", "text": "\n", "time": "2023-05-24T16:31:18Z"}, {"author": "Christopher Patton", "text": "I remember an assertion that, in math, a huge fraction of published proofs are wrong, and a significant fraction of them are proving false things+1. I'll just add here (and fess up to the fact that) some one recently reviewed an old paper of mine on ePrint and found a few bugs. I can fix them on ePrint, but they're forever enscribed in the CRYPTO '19 proceedings and I wish I could have avoided them.
\n
(Let me try that again) +1 Nikita. I'll just add here (and fess up to the fact that) some one recently reviewed an old paper of mine on ePrint and found a few bugs. I can fix them on ePrint, but they're forever enscribed in the CRYPTO '19 proceedings and I wish I could have avoided them.
", "time": "2023-05-24T16:32:05Z"}, {"author": "Felix Linker", "text": "@Christopher: best UI != good UI :)
", "time": "2023-05-24T16:32:08Z"}, {"author": "Nikita Borisov", "text": "UI designed by tetrachromats
", "time": "2023-05-24T16:33:07Z"}, {"author": "Felix Linker", "text": "I use Tamarin as well and completely second Jonathan. It's nice to have a UI, but it makes me so angry so often.
", "time": "2023-05-24T16:34:03Z"}, {"author": "Christoph Egger", "text": "still the complaints sound very much easily solveable and not so much conceptual
", "time": "2023-05-24T16:34:25Z"}, {"author": "Christoph Egger", "text": "like its \"just\" a engineering issue
", "time": "2023-05-24T16:34:37Z"}, {"author": "Felix Linker", "text": "It definitely is. But universities don't have the capacity most of the time to push on the UI more. This is connected to publishability.
", "time": "2023-05-24T16:35:18Z"}, {"author": "Christoph Egger", "text": "and also it definitely is important to solve, not questioning ;-)
", "time": "2023-05-24T16:35:42Z"}, {"author": "Guido Schmitz", "text": "One reason to go with pen and paper in my previous works on analyses of protocols that build upon web infrastructure are the limitations of the tools to deal with the huge complexity of the overall environment. For example, it is hard to capture unbounded/recursive data structures, unbounded loops, etc.
", "time": "2023-05-24T16:37:27Z"}, {"author": "Carsten Bormann", "text": "Different skills: Designing and analyzing protocols...
", "time": "2023-05-24T16:37:27Z"}, {"author": "Guido Schmitz", "text": "But as the tools are improving, this argument becomes weaker of course. However, we are still not there yet
", "time": "2023-05-24T16:38:33Z"}, {"author": "Christoph Egger", "text": "and recursive datastructures (even lists) really are hard to solve
", "time": "2023-05-24T16:39:29Z"}, {"author": "Felix Linker", "text": "I could see myself being involved in Tamarin training material
", "time": "2023-05-24T16:40:22Z"}, {"author": "Carsten Bormann", "text": "I would certainly join as an attendee :-)
", "time": "2023-05-24T16:41:26Z"}, {"author": "Yaron Sheffer", "text": "Correct
", "time": "2023-05-24T16:43:44Z"}, {"author": "Colin Perkins", "text": "There's two types of training: teaching protocol people how to use formal methods; and teaching formal methods people about interesting protocol challenges
", "time": "2023-05-24T16:44:20Z"}, {"author": "Nikita Borisov", "text": "In my limited experience, when I look at a mechanized proof I don't so much care \"can I reproduce proving the result\" but \"can I play around with the assumptions / constructions\". So a PCP certificate of a proof would have limited value for me
", "time": "2023-05-24T16:47:31Z"}, {"author": "Stephen Farrell", "text": "given Jonathan's good points about publishability it may be nicely ironic if his if-time-permits presentation has to be skipped a 2nd time;-)
", "time": "2023-05-24T16:47:40Z"}, {"author": "Guido Schmitz", "text": "Regarding verifiability, there are tools available that yield such artifacts. In F*, for example, proofs are built by pushing the prover in the right direction by assertion requests and lemmas. Furthermore, the tool also generates hints for the tool how to find the correct proof.
", "time": "2023-05-24T16:48:55Z"}, {"author": "Lucas Pardue", "text": "financial or temporal denial of verifcation attack
", "time": "2023-05-24T16:49:00Z"}, {"author": "Stephen Farrell", "text": "once these slides are done I'm gonna ask \"who wants to do what?\" so esp if something hasn't yet been mentioned, please be ready to join the queue to bring up your fav thing to be done (that you're willing to work on)
", "time": "2023-05-24T16:50:07Z"}, {"author": "Jan Winkelmann", "text": "yeah, groth16 and plonk and friends
", "time": "2023-05-24T16:52:02Z"}, {"author": "Felix Linker", "text": "Many great things to work on have been mentioned already :)
", "time": "2023-05-24T16:55:37Z"}, {"author": "Marc Petit-Huguenin", "text": "One day we may have a formal method directorate that will verify protocol before publication.
", "time": "2023-05-24T16:56:42Z"}, {"author": "Carsten Bormann", "text": "not \"we\", but \"they\" (IETF)
", "time": "2023-05-24T16:57:06Z"}, {"author": "Marc Petit-Huguenin", "text": "Right
", "time": "2023-05-24T16:57:19Z"}, {"author": "Carsten Bormann", "text": "great meeting, actually
", "time": "2023-05-24T16:57:23Z"}, {"author": "Colin Perkins", "text": "+1
", "time": "2023-05-24T16:57:28Z"}, {"author": "Christopher Brzuska", "text": "Thanks, bye!
", "time": "2023-05-24T16:59:10Z"}, {"author": "Felix Linker", "text": "Thanks! Good bye!
", "time": "2023-05-24T16:59:11Z"}, {"author": "Guido Schmitz", "text": "Thanks everyone!
", "time": "2023-05-24T16:59:13Z"}]