[{"author": "Sofia Celi", "text": "

great idea!

", "time": "2023-09-01T16:11:00Z"}, {"author": "Sofia Celi", "text": "

perfect!

", "time": "2023-09-01T16:13:33Z"}, {"author": "Nadim Kobeissi", "text": "

I would agree that Tamarin and ProVerif overlap a lot. Can't comment on the other potential case that was mentioned.

", "time": "2023-09-01T16:17:16Z"}, {"author": "Steve Crocker", "text": "

It might be helpful to have a rough taxonomy of what properties each of these tools can be used for. My quick, non-comprehensive, list of suggested categories is the following...

", "time": "2023-09-01T16:20:04Z"}, {"author": "Jonathan Hoyland", "text": "

It has the best GUI. However the bar is _very_ low.

", "time": "2023-09-01T16:20:17Z"}, {"author": "Steve Crocker", "text": "
    \n
  1. Proofs that an implementation of a protocol correctly implements the protocol. This requires a high level specification of the protocol.
    2. \n
", "time": "2023-09-01T16:21:09Z"}, {"author": "Sofia Celi", "text": "

Thom Wiggers can help on tamarin as well: we cna prob ask him

", "time": "2023-09-01T16:21:17Z"}, {"author": "Jonathan Hoyland", "text": "

@Steve there is an SoK out there somewhere https://inria.hal.science/hal-03046757/document

", "time": "2023-09-01T16:21:34Z"}, {"author": "Jonathan Hoyland", "text": "

Not sure exactly that maps on to what you want, but it might be useful tool.

", "time": "2023-09-01T16:22:49Z"}, {"author": "Steve Crocker", "text": "
    \n
  1. Proofs that the protocol accomplishes specific functionality. For example, for TCP, that a stream of bytes is transferred, and for DNS that queries result in retrieving the the expected recrods.
    2. \n
", "time": "2023-09-01T16:23:12Z"}, {"author": "Steve Crocker", "text": "
    \n
  1. Proofs involving resilience against attack.
    2. \n
", "time": "2023-09-01T16:23:49Z"}, {"author": "Steve Crocker", "text": "
    \n
  1. Etc.
    2. \n
", "time": "2023-09-01T16:23:52Z"}, {"author": "Jonathan Hoyland", "text": "

I mean, Tamarin will tell you that something is secure even if it isn't, because it doesn't (by default) do EUF-CMA asymmetric ciphers.

", "time": "2023-09-01T16:26:40Z"}, {"author": "Nadim Kobeissi", "text": "

All symbolic model tools have wonks like that! Verifpal moreso than others since it's basically the Lego of modeling tools, but still, that's why people started working on CryptoVerif and EasyCrypt eventually.

", "time": "2023-09-01T16:28:40Z"}, {"author": "Sofia Celi", "text": "

oh that is nice @hans

", "time": "2023-09-01T16:29:28Z"}, {"author": "Jonathan Hoyland", "text": "

I think it might be useful to have one general purpose thing, and one domain specific tool.

", "time": "2023-09-01T16:31:29Z"}, {"author": "Sofia Celi", "text": "

+1

", "time": "2023-09-01T16:31:40Z"}, {"author": "Steve Crocker", "text": "

Crypto proofs are obviously one large area, but there are other properties worth proving. I'm particularly interested in properties related to the distributed nature of protocols. In the DNS area, continuity of resolution and validation during changes in keys, changes in name servers, etc.

", "time": "2023-09-01T16:31:46Z"}, {"author": "Nadim Kobeissi", "text": "

@Justin: I agree

", "time": "2023-09-01T16:33:03Z"}, {"author": "Jonathan Hoyland", "text": "

Arm do things with VeriLog, no?

", "time": "2023-09-01T16:33:16Z"}, {"author": "Nadim Kobeissi", "text": "

Sure, happy to help

", "time": "2023-09-01T16:36:44Z"}, {"author": "Nadim Kobeissi", "text": "

Gladiator arena battle

", "time": "2023-09-01T16:37:26Z"}, {"author": "Sofia Celi", "text": "

Tamarin seems very solid to have

", "time": "2023-09-01T16:37:34Z"}, {"author": "Sofia Celi", "text": "

and Coq as well

", "time": "2023-09-01T16:37:41Z"}, {"author": "Jonathan Hoyland", "text": "

The options are Coq, Tamarin, ProVerif,, and VerifPal

", "time": "2023-09-01T16:37:56Z"}, {"author": "Sofia Celi", "text": "

great!

", "time": "2023-09-01T16:41:51Z"}, {"author": "Sofia Celi", "text": "

awesome! thank you!

", "time": "2023-09-01T16:44:14Z"}, {"author": "Nadim Kobeissi", "text": "

No gladiator battle... darn

", "time": "2023-09-01T16:44:28Z"}, {"author": "Felix Linker", "text": "

@Stephen/Jonathan: I took notes in the agenda, because I didn't see the meeting notes section. I hope they're alright as they are!

", "time": "2023-09-01T16:44:45Z"}, {"author": "Nadim Kobeissi", "text": "

Byebye!

", "time": "2023-09-01T16:44:53Z"}, {"author": "Hans-Dieter Hiep", "text": "

Thanks!

", "time": "2023-09-01T16:44:53Z"}, {"author": "Muhammad Sardar", "text": "

Thank you, bye.

", "time": "2023-09-01T16:44:59Z"}]