[Verifpal] Queries on undefined messages crash verifpal

Nadim Kobeissi nadim at symbolic.software
Wed Oct 21 23:13:58 CEST 2020


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 at 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 at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20201021/13d9108a/attachment.htm>


More information about the Verifpal mailing list