[Verifpal] A few comments and questions

Tom Hacohen tom at stosb.com
Thu Feb 6 18:19:59 CET 2020


On 06/02/2020 16:54, Nadim Kobeissi wrote:
>> 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”.

Yeah, I understand the difference between knows and generated. Though
the name "m1" indicates the plain text message, not, for example, the
ephemeral private keys in the Signal protocol.

Assuming m1 really does indicate a plain text message. Should it be
marked as "knows private" (probably) or "generated"? And maybe worth it
to be consistent with how that's used in this use case (assuming I'm
remembering correctly and there is in fact an inconsistency).

> 
>>
>> 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.

Thanks, I'll have to play with it more.

> 
>>
>> 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?

No idea, sorry. :)

> 
>>
>> 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.

Saw you added it. Great, thanks!

> 
>>
>>
>> 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.

:)

--
Tom


More information about the Verifpal mailing list