Dear Friedrich,

Thanks for reporting this. Fixed here:
https://source.symbolic.software/verifpal/verifpal/-/commit/7336b7bc901170e2948b341f9a51d793888b4151

Nadim Kobeissi
Symbolic Software https://symbolic.software
Sent from office


On Wed, Oct 21, 2020 at 9:59 PM Friedrich Wiemer via Verifpal <verifpal@lists.symbolic.software> wrote:
Hi,

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

attacker[active]

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

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

Best,
Friedrich

--
Dr. Friedrich Wiemer,
orcid.org/0000-0003-2998-6777
_______________________________________________
Verifpal mailing list
Verifpal@lists.symbolic.software
https://lists.symbolic.software/mailman/listinfo/verifpal