On Wed, Oct 21, 2020 at 9:59 PM Friedrich Wiemer via Verifpal <firstname.lastname@example.org> wrote:
the following model leads to a crash with verifpal 0.19.2 on Windows:
principal Client[generates nonce_c]
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,
Verifpal mailing list