[Verifpal] Error message (for mispelled keyword)

Friedrich Wiemer friedrich.wiemer at rub.de
Mon Mar 2 20:38:19 CET 2020

Dear Nadim,

consider the attached model. Here, the auth querry is mispelled
(authentification instead of authentication). Again, the error message
is a very generic:

> % verifpal verify auth.vp
> Verifpal 0.11.8 - https://verifpal.com
>   Warning • Verifpal is experimental software.
>  Verifpal • Parsing model 'auth.vp'...
>  Verifpal! Error: auth.vp:1:1 (0): no match found.

Does the parser allow e.g. to give the exact line of code, where the
error occured in the model? I guess this would be very helpful (and
looks like much less work than finding all possible misspelled keywords


Dr. Friedrich Wiemer,
Research Assistant

Symmetric Cryptography
Horst Goertz Institute for IT-Security,
Ruhr-University Bochum,

-------------- next part --------------

principal Alice[
    knows private k_ab
principal Bob[
    knows private k_ab

principal Alice[
    generates m1

    e_m = AEAD_ENC(k_ab, m1, nil)
Alice -> Bob: e_m

principal Bob[
    m_dec = AEAD_DEC(k_ab, e_m, nil)?

    authentification? Alice -> Bob: e_m
    //authentication? Alice -> Bob: e_m

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200302/65869092/attachment.sig>

More information about the Verifpal mailing list