[{"author": "Stephen Farrell", "text": "

we'll start at :33 - just letting people wander in

", "time": "2023-03-29T00:32:12Z"}, {"author": "Jonathan Hoyland", "text": "

I had someone suggest SIP last night.

", "time": "2023-03-29T00:43:19Z"}, {"author": "Tony Li", "text": "

Prove that SCION is secure.

", "time": "2023-03-29T00:44:44Z"}, {"author": "Pieter Kasselman", "text": "

There is some work ongoing on the OAuth Device Authorization Grant

", "time": "2023-03-29T00:46:08Z"}, {"author": "Stephen Farrell", "text": "

forgot to say; we have note-takers and thanks to them!

", "time": "2023-03-29T00:48:28Z"}, {"author": "Stephen Farrell", "text": "

so if remote folks have questions/comments please also feel free to join the queue

", "time": "2023-03-29T00:51:53Z"}, {"author": "Richard Barnes", "text": "

you can tell how user-friendly the Tamarin UI is

", "time": "2023-03-29T00:57:06Z"}, {"author": "Richard Barnes", "text": "

to be clear, i have found Tamarin quite useful, including for non-cryptographic uses (e.g., analyzing access controls)

", "time": "2023-03-29T01:02:14Z"}, {"author": "Pieter Kasselman", "text": "

Interesting, do you have an example of how you did that?

", "time": "2023-03-29T01:02:55Z"}, {"author": "Christopher Patton", "text": "

Tamarin is quite popular

", "time": "2023-03-29T01:03:12Z"}, {"author": "Richard Barnes", "text": "

Not a public example. Used it to analyze some stuff internal Cisco stuff -- first build a representation of the system as-is and verified that found (at least) the known set of vulnerabilities, then updated the representation to reflect proposed mitigations and verified that the mitigations in fact fixed the vulnerabilities

", "time": "2023-03-29T01:06:13Z"}, {"author": "Stephen Farrell", "text": "

again, remote folks: don't be shy about joining the queue and pleasing us with your audio:-)

", "time": "2023-03-29T01:06:32Z"}, {"author": "Christopher Patton", "text": "

Wes is next in the quuee?

", "time": "2023-03-29T01:08:39Z"}, {"author": "Marc Petit-Huguenin", "text": "

Can someone spell the name of the tool/system that people talked about just right now?

", "time": "2023-03-29T01:09:16Z"}, {"author": "Christopher Inacio", "text": "


", "time": "2023-03-29T01:09:45Z"}, {"author": "Christopher Inacio", "text": "


", "time": "2023-03-29T01:09:57Z"}, {"author": "Marc Petit-Huguenin", "text": "

Hmm, the transcription said Ava?

", "time": "2023-03-29T01:10:09Z"}, {"author": "Marc Petit-Huguenin", "text": "

Anyway thanks.

", "time": "2023-03-29T01:10:39Z"}, {"author": "Christopher Inacio", "text": "

Ben (I think) named a whole bunch of tools, I know a number of them, but not the whole list.

", "time": "2023-03-29T01:10:52Z"}, {"author": "Tim W\u00fcrtele", "text": "


", "time": "2023-03-29T01:10:57Z"}, {"author": "Guido Schmitz", "text": "

I don't think avispa was mentioned

", "time": "2023-03-29T01:11:21Z"}, {"author": "Felix Linker", "text": "

AVISPA was briefly mentioned but not discussed

", "time": "2023-03-29T01:11:35Z"}, {"author": "Marc Petit-Huguenin", "text": "

That's it, thanks.

", "time": "2023-03-29T01:12:55Z"}, {"author": "Benjamin Beurdouche", "text": "

One key element for the IETF is to make progress in formalizing protocols

", "time": "2023-03-29T01:14:36Z"}, {"author": "Pieter Kasselman", "text": "

I wonder if we can teach ChatGPT to translate protocols into Tamarin...

", "time": "2023-03-29T01:16:23Z"}, {"author": "Benjamin Beurdouche", "text": "

Finding a good language in which people can express protocols in (say HACSPEC) would be a great first step

", "time": "2023-03-29T01:16:28Z"}, {"author": "Christopher Patton", "text": "

Good work Richard! Quite a feat

", "time": "2023-03-29T01:17:37Z"}, {"author": "\u67f3\u7530 \u6dbc", "text": "

@Benjamin Beurdouche Don't worry about modifying the notes others wrote! I struggle to keep up, so additions/edits are very welcome!

", "time": "2023-03-29T01:24:56Z"}, {"author": "Stephen Farrell", "text": "

thanks again to Ben & Chris for note-taking

", "time": "2023-03-29T01:25:54Z"}, {"author": "Richard Barnes", "text": "

Here's a snippet from the Tamarin model I build showing people what slightly more expressive Tamarin looks like: https://gist.github.com/bifurcation/0bdb4bd3f7bd44a98ba871760699291f

", "time": "2023-03-29T01:27:20Z"}, {"author": "Richard Barnes", "text": "

one of the things that's nice about Tamarin is that it forces you to admit that any system fails under sufficiently terrible circumstances :)

", "time": "2023-03-29T01:28:39Z"}, {"author": "Richard Barnes", "text": "

overall project was around 2k lines of Tamarin model

", "time": "2023-03-29T01:29:45Z"}, {"author": "Stephen Farrell", "text": "

start from a paper: ideally a 20 year old one (IPR and all that:-)

", "time": "2023-03-29T01:36:10Z"}, {"author": "Tim W\u00fcrtele", "text": "

Related to the current discussion around security properties: Regardless of whether the respective WG or some researchers do security analysis of IETF standards, the standards should in some way or another be explicit about the desired security properties. See, e.g., the OIDF's FAPI 2.0 Attacker Model document for an example.

", "time": "2023-03-29T01:39:58Z"}, {"author": "Pieter Kasselman", "text": "

Perhaps a \"security goals\" section as part of the Security Considerations section of the spec?

", "time": "2023-03-29T01:43:26Z"}, {"author": "Tim W\u00fcrtele", "text": "

Also, machine-checked proofs are not a silver bullet: reviewers (whether in the scientific sense or protocol designers trying to use analysis results) still need to understand a) what is modelled (does the protocol model truly model the standard?), and b) what exactly are the security properties.

", "time": "2023-03-29T01:43:41Z"}, {"author": "Richard Barnes", "text": "

i think QUIC crypto had multiple machine-checked proofs when it was broken :) they had some assumptions that turned out not to be true

", "time": "2023-03-29T01:44:16Z"}, {"author": "Stephen Farrell", "text": "

sorry Richard would like to try get our remote speaker started so could you hold your comment 'till later?

", "time": "2023-03-29T01:45:01Z"}, {"author": "Felix Linker", "text": "

Seconding Tim, I would like to add that machine-checked proofs also have their downsides, e.g., usually requiring more abstractions, and must be reviewed with the same care as pen-and-paper proofs.

", "time": "2023-03-29T01:45:02Z"}, {"author": "Jonathan Hoyland", "text": "

The best way to limit mistakes in models is ... standardisation!

", "time": "2023-03-29T01:45:03Z"}, {"author": "Stephen Farrell", "text": "


", "time": "2023-03-29T01:45:09Z"}, {"author": "Richard Barnes", "text": "

@Wes - To your point about assumptions -- these modeling tools force you to make assumptions more explicit, which makes them easier to validate

", "time": "2023-03-29T01:45:46Z"}, {"author": "Felix Linker", "text": "

@Pieter Kasselman Absolutely! I think this would be a value regardless of formal analysis (or verification? I am confused...)

", "time": "2023-03-29T01:45:50Z"}, {"author": "Tim W\u00fcrtele", "text": "

@Pieter Kasselman: Something like that would indeed help. Benjamin already pointed out above that the protocol itself should also given in an at least somewhat formalized language, the security goals could then be stated in the same kind of formalized language.However, having _some_ explicit security goal is certainly better than nothing. Such a section is also useful for people who want to use the protocol.

", "time": "2023-03-29T01:46:33Z"}, {"author": "Richard Barnes", "text": "

there are limits to machine checking. i believe the tools had to grow some new features to cover TLS 1.3 and MLS

", "time": "2023-03-29T01:47:00Z"}, {"author": "Richard Barnes", "text": "

... which could be a good interaction between the proposed RG and IETF WGs! i.e., looking at whether tools have sufficient semantics to cover the protocols being developed

", "time": "2023-03-29T01:48:04Z"}, {"author": "Carsten Bormann", "text": "

... and carrying back real-world requirements to the research community is one of the things RGs can be useful in...

", "time": "2023-03-29T01:48:04Z"}, {"author": "Jonathan Hoyland", "text": "

I had the exceedingly fun experience of finding a bug in a machine checked proof where somebody had failed to close a comment half-way through the proof. Checker said the proof held, but wasn't checking half the proof. :man_facepalming:

", "time": "2023-03-29T01:48:23Z"}, {"author": "Christopher Inacio", "text": "

As to composability of proofs, some researchers at Carnegie Mellon have been building a formally proven hypervisor (https://uberxmhf.org) \u00fcber xmhf. that's primarily written in TLA+ with the proofs discharged using Coq. That's a large set of composed proofs to pull that off.

", "time": "2023-03-29T01:48:50Z"}, {"author": "Jonathan Hoyland", "text": "

There is a good list of tools in this SoK https://hal.inria.fr/hal-03046757/file/BarbosaetalOakland21.pdf

", "time": "2023-03-29T01:49:51Z"}, {"author": "Christopher Inacio", "text": "

Right now, actually, the work has progressed as to how to extend that system to the PVH API (the Xen hardware interface) so that virtual machines can be secured in \"cloud\" environments.

", "time": "2023-03-29T01:50:54Z"}, {"author": "Doug Montgomery", "text": "

The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications\u0001- https://people.inf.ethz.ch/basin/pubs/avispa05.pdf

", "time": "2023-03-29T01:52:30Z"}, {"author": "Arnaud Taddei", "text": "

Thank you for the list of tools, maybe some knoweldge to stabilise in this potential working group

", "time": "2023-03-29T01:52:43Z"}, {"author": "Richard Barnes", "text": "

@Doug yikes, www.avispa-project.org is badly bitrotted

", "time": "2023-03-29T01:55:30Z"}, {"author": "Guido Schmitz", "text": "

The ufmrg wiki also contains an overview on case studies / tools: https://wiki.ietf.org/en/group/ufm

", "time": "2023-03-29T01:57:03Z"}, {"author": "Christopher Patton", "text": "

Anyone have a link to the SoK Bas mentioned?

", "time": "2023-03-29T01:58:10Z"}, {"author": "Jonathan Hoyland", "text": "

I posted it upthread

", "time": "2023-03-29T01:58:19Z"}, {"author": "Felix Linker", "text": "


", "time": "2023-03-29T01:58:26Z"}, {"author": "Jonathan Hoyland", "text": "


", "time": "2023-03-29T01:58:26Z"}, {"author": "Richard Barnes", "text": "

didn't hacspec used to be python?

", "time": "2023-03-29T01:59:43Z"}, {"author": "Christopher Patton", "text": "

libcrux: Do you take PRs :D

", "time": "2023-03-29T02:01:00Z"}, {"author": "Guido Schmitz", "text": "

There is also a good overview on the topic of formal methods as part of CyBoK: https://www.cybok.org/media/downloads/Formal_Methods_for_Security_v1.0.0.pdf

", "time": "2023-03-29T02:01:29Z"}, {"author": "Guido Schmitz", "text": "

(not only focussing on tools)

", "time": "2023-03-29T02:02:20Z"}, {"author": "Jonathan Hoyland", "text": "

@Guido Schmitz Please can you add that to the wiki?

", "time": "2023-03-29T02:02:29Z"}, {"author": "Guido Schmitz", "text": "

Yes, I'll do that

", "time": "2023-03-29T02:02:52Z"}, {"author": "Doug Montgomery", "text": "

Richard Barnes said:


@Doug yikes, www.avispa-project.org is badly bitrotted


How do you mean? Not that I have any affiliation to AVISPA. And like many research projects the developers have probably moved on. Having said that the tools seemed viable ~2 years ago when we had a guest research explore using them to model BRSKI.

", "time": "2023-03-29T02:02:57Z"}, {"author": "Jonathan Hoyland", "text": "

Thanks :thank_you:

", "time": "2023-03-29T02:03:11Z"}, {"author": "Richard Barnes", "text": "

@doug mainly that when i clicked the web tool link it was totally broken https://www.avispa-project.org/web-interface/index.php

", "time": "2023-03-29T02:03:42Z"}, {"author": "Richard Barnes", "text": "

(at least in Firefox Nightly)

", "time": "2023-03-29T02:03:51Z"}, {"author": "Richard Barnes", "text": "

don't mean any judgement about the tool, just that the website seems abandoned

", "time": "2023-03-29T02:04:28Z"}, {"author": "Jonathan Hoyland", "text": "

Having worked on the armcc compiler, I can confirm. C compilers can indeed have bugs. Sorry.

", "time": "2023-03-29T02:06:04Z"}, {"author": "Doug Montgomery", "text": "

@Richard Barnes that might be - I don't think we ever tried the web-interface. ~2 summers ago the tools were viable. An exploratory project for us - Tech Note about the effort here: https://nvlpubs.nist.gov/nistpubs/TechnicalNotes/NIST.TN.2123.pdf

", "time": "2023-03-29T02:08:50Z"}, {"author": "Jonathan Hoyland", "text": "

I think AVISPA last got an update in ~2006.

", "time": "2023-03-29T02:10:21Z"}, {"author": "Stephen Farrell", "text": "

I'm guessing the \"what do we do next part\" is maybe gonna have to be done on the list and/or a call in the next month or two?

", "time": "2023-03-29T02:26:16Z"}, {"author": "Pieter Kasselman", "text": "

Does the Wiki already contain a list of IETF protocols being analysed?

", "time": "2023-03-29T02:26:57Z"}, {"author": "Felix Linker", "text": "

Since the queue is closed, I presume it's best to respond to Jonathan here.


Resources are always useful, however, I fear that many models are so tuned to details and non-composable that \"using other models\" is virtually impossible for many proof attempts (at least that would be my feeling for Tamarin).

", "time": "2023-03-29T02:27:09Z"}, {"author": "Jonathan Hoyland", "text": "

I think the current list is of protocols that have been analysed, not of ones currently under analysis.

", "time": "2023-03-29T02:27:27Z"}, {"author": "Cheng Zhou", "text": "

A Survey on Network Verification and Testing With Formal Methods: Approaches and Challenges
\nhttps://ieeexplore.ieee.org/document/8453007Some work (if not all) mentioned in this paper could be in the scope of the RG.

", "time": "2023-03-29T02:28:13Z"}, {"author": "Cheng Zhou", "text": "


", "time": "2023-03-29T02:28:52Z"}, {"author": "Jonathan Hoyland", "text": "

So Tamarin models can be made reusable if you put the effort in.

", "time": "2023-03-29T02:28:55Z"}, {"author": "Tim W\u00fcrtele", "text": "

@Pieter Kasselman Yes, the wiki contains such a list (probably incomplete)

", "time": "2023-03-29T02:29:01Z"}, {"author": "Felix Linker", "text": "

@Jonathan Are you aware of any Tamarin models that have put this effort in?

", "time": "2023-03-29T02:29:48Z"}, {"author": "Pieter Kasselman", "text": "

Jonathan, perhaps we can add protocols under analysis and also use those experiences to develop best practices for protocol development in conjunction with formal methods?

", "time": "2023-03-29T02:30:04Z"}, {"author": "Benson Muite", "text": "

Useful session. thanks.

", "time": "2023-03-29T02:30:52Z"}, {"author": "Jonathan Hoyland", "text": "

@Felix Linker Our TLS 1.3 Tamarin model had this as a feature, and has been reused for at least 5 different analyses to my direct knowledge.

", "time": "2023-03-29T02:31:00Z"}, {"author": "Felix Linker", "text": "

That's great! Perhaps I underestimated the composability of Tamarin models.

", "time": "2023-03-29T02:31:20Z"}]