[Verifpal] Handling of constant messages in protocols

Renaud Lifchitz renaud.lifchitz at gmail.com
Tue Jun 23 14:24:17 CEST 2020


As discussed yesterday night on the Discord channel, there is currently no
easy way to model a fixed message in an exchange (for example the "HELLO"
message to initiate a handshake) :
- The "knows public HELLO" statement followed by HELLO transmission throws
an error in current Verfpal "Verifpal! Error: Device is receiving constant
(HELLO) despite already knowing it.", which prevents any further analysis
of the whole protocol
- The only workaround I've found so far is to use "knows private HELLO" and
send HELLO, which is obviously not private...

I suggest current Verifpal error be converted into a warning to allow this
useful and frequent kind of use.

Best regards,

Renaud Lifchitz
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200623/eddb32c9/attachment.htm>

More information about the Verifpal mailing list