[Verifpal] A few comments and questions
nadim at symbolic.software
Thu Feb 6 15:54:21 CET 2020
> On 5 Feb 2020, at 9:01 AM, Tom Hacohen <tom at stosb.com> wrote:
> Great work with verifpal. It's something I've been wanting to have for a
> while now, and from playing with it, it looks great. Thanks a lot!
Thanks for these questions!
> I have a few comments and questions from playing around with it. I'll
> send them all in this email, and will send a separate one for a bug
> report I have. They are all pretty minor paper-cuts, so no rush on
> addressing or commenting on them.
> I got a "No match found" error, which took me a while to figure out. The
> issue was that I added a semi-colon (muscle memory) to a send directive.
> So for example "Alice -> Bob: e1;". Maybe consider banning ; from the
> syntax altogether and error about it nicely? I'm sure I'm not the only
> one that appends semi-colons.
Verifpal uses the Pigeon parser generator (https://github.com/mna/pigeon) which can sometimes offer lackluster syntax error messages. I’ll see what I can do to improve that.
> A small inconsistency in the doc that I noticed is that "m1" is
> sometimes marked as "generated" and sometimes as "knows private". I
> guess both make sense to an extent, though they both mean different
> things in the case of an active attacker analysis and the back and forth
> was confusing. Which one is preferred (if at all)?
“Generated” refers to constants that differ between each protocol execution, such as random numbers, while “knows” are static no matter how many times the protocol is run. In Signal, ephemeral private keys would be “generated” while long-term identity keys would be “known”.
> I also have a small question about phases. How are they different to
> just the linear execution order within a phase? Maybe I missed
> something, though it wasn't clear from the docs. I understand the actual
> difference that was mentioned, that values there can only be discovered
> in that phase, but isn't that linear anyway, in the sense that values
> can only be uncovered once sent in the clear?
When Verifpal analyzes a protocol under an active attacker, it will execute the entire protocol an unbounded number of times until it decides that it cannot learn any new information. In that scenario, if you were not to use phases, then values learned by Verifpal at the end of a protocol execution would be usable at the beginning of the next execution. This would not allow modeling for scenarios like forward secrecy, which depend on an event happening strictly after a protocol has run its course.
> Primitive suggestion: zero-knowledge-proofs. I guess you can somehow
> describe them already using a signature for some aspects. Though I'd say
> a primitive is still needed.
Indeed, could you suggest an interface?
> One more piece of syntax that I found a bit counter-intuitive, or at
> least, not semantic is how PFS is checked. "Alice -> Bob: a", while
> conveys the idea that Alice's private key has been leaked, it also
> specifically indicates that Alice sends Bob the key as part of the
> protocol, which is not the case. The more likely case is that Eve stole
> Alice's device. Maybe a "becomes public a" or "leaks a" would be better
> (those are just suggestions, better find something that you feel is more
> consistent with the rest of verifpal).
Huh — “leaks” is really nice, actually. Let me think about it.
> These are my comments and questions. I also have a bug report that I'll
> send in a separate email.
> Thanks a lot for all your work. Verifpal has been great so far, and I
> look forward to modelling the next iteration of the protocol I'm working
> on with it. It looks like exactly what I've been looking for!
Thank you; receiving discussions like this makes it all worthwhile.
> Verifpal mailing list
> Verifpal at lists.symbolic.software
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 833 bytes
Desc: Message signed with OpenPGP
More information about the Verifpal