[Verifpal] A few comments and questions
tom at stosb.com
Wed Feb 5 09:01:11 CET 2020
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!
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.
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)?
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?
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.
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).
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!
More information about the Verifpal