UFMRG at IETF-124

Agenda

Note taker: Chris Inacio (thanks! np)

• Agenda Bash (chairs, 5)

• SEAT and proofs (Muhammad Usama Sardar, 25)
  https://datatracker.ietf.org/wg/seat/documents/

  • Looking for help and resolutions with Lowe's Hierarchy. Not sure
    they believe the "weak agreement" strength. Might be looking for
    compound authentication. More support on list or in SEAT WG.
  • The tooling to help visualize the proofs, and in particular the
    counter-examples, is done by hand currently. There isn't tooling
    to support this.

  Stephen: How did you make the visualization
  Muhammad: How I think about a participation and then showed single
  traces and said how do you interpret it. These visualizations are
  not exhaustive of the cases.
  Stephen: Any tooling to generate these?
  Muhammad: No, all hand drawn currently.

  Muhammad: Opinions on Lowe's Hierarchy
  Jonathan: It's a weirdness of the terminology. idc just means
  you're talking to the same client, not that you know who the
  client is. It doesn't present any identity information about the
  client other than they know some part of the secret for the
  communication channel
  Felix: Don't understand the question; there are 2 questions, but you
  say "week agreement" is wrong. That's a philosophical question - is
  that what you want to discuss? Maybe "weak agreement" is the wrong
  assertion/statement for your protocol.
  Muhammad: if you have 1-way vs. 2-way injective agreement
  something, details not captured
  Jonathan: I think want you're looking for, going toward of "compound
  authentication"
  [ed: taking this conversation to the list; appears that SEAT may be
  looking for a slightly different construction; would like help
  finding it.]

  Rowen S.: what were some of the changes you had to make with the
  protocol developers because of this analysis
  Mohammad: Being able to explain and visualize the proof for the
  engineers so that the protocol designers can understand and adjust
  to iterate better protocol design

• SecureDrop proofs (Felix Linker, Cory Francis Myers, 25)

  Muhammad: TLS already has computation & symbolic proofs; was your
  combination novel?
  Felix: No, its a good case study; we followed Cas's methods.
  Muhammad: What was FPF's background, did you know Tammarind?
  Cory: We are a SWEng team, we didn't have deep formal methods.
  Learned Tammarind at the Prague tutorial.

  Jacob: How big was your model in the end
  Felix: not sure, 300-500 lines of code in the end?
  Jacob: Have you considered doing the unobservational /
  undetectability in Tammarind?
  Felix: Have considered it, but thought the state would explode
  Jacob: Have you considered doing some of those models in ProVerif,
  had more success there.
  Felix: I beleive that's because ProVerif has a more nieve model of
  observability, so ProVerif is faster, but less accurate.

  Antonio: Something about generating more noise in the messaging?
  Cory: We're aware of that gap, and we're interested in exploring
  that more in the future

• Proof Ladders (Deirdre Connolly, 25)
  https://proof-ladders.github.io/

  Muhammad: Main focus is cryptographers, how far is it from engineers
  usability? In scope / out of scope?
  Dierdre: Not necessarily out of scope, but we want to give
  cryptographers who write proofs, usually by hand, that you can do
  those with computers. Want to show those cryptographers, that
  focusing on only the lowest level set of building blocks isn't
  enough for folks to build usable systems, that you have to build all
  the layers. So, engineers are not out of scope, but need to build
  up; but not the current target. It's about learning how to write
  proofs with these tools.
  Muhammad: For someone like me, who does some work with ProVerif, and
  some symbolic proofs, would this be for me?
  Dierdre: Maybe, it can be. But the focus is on building up those
  proofs and skills.

• AOB (what's left or 10)

  Muhammad: Trying to start a RG on confidential computing and would
  like to get contributions from the formal methods
  chair: send a link to the side meeting to the list.

  Stuart: Trusted computing center of excellence: trying to push
  formal methods out there to critical infrastructure and we need
  help. We're still out there.
  chair: submit a pointer to the list.