[Verifpal] Queries on undefined messages crash verifpal

Friedrich Wiemer friedrich.wiemer at rub.de
Wed Oct 21 21:59:26 CEST 2020


the following model leads to a crash with verifpal 0.19.2 on Windows:


principal Client[generates nonce_c]
principal Server[]
Client -> Server: nonce_c

    authentication? Client -> Server: bla

My guess is, that this is due to 'bla' being not defined.
The crash I get is a "panic: runtime error: index out of range [-1]"

Please let me know, if you need the stack trace.

BTW: it would be nice to be able to upload models to verifhub without first 'verify'ing them. I would have done so with this model, but the crash prevented it.


Dr. Friedrich Wiemer,
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20201021/78bc75e0/attachment.htm>

More information about the Verifpal mailing list