[Verifpal] (feature request) Better unused outputs

[Nadim Kobeissi]

Dear Loup,

Thank you for another insightful and constructive email.

I think that having a “_” output for HMACVERIF and SIGNVERIF is a good idea, and I will look into it for the next major version of the Verifpal language. For now, I will not make such a large change that closely to the language’s initial release, in order not to confuse newcomers who may have not even had enough time to finish reading the User Manual for the first time.

Rest assured however that this will be kept for more serious work in the next major release.

Looking forward to hearing more thoughts from you on how we can continue to improve Verifpal!

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On Aug 29, 2019, at 5:13 PM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
> 
> Hi,
> 
> Looking a bit more closely at HMACVERIF, I see that its syntax is
> currently not ideal (I can sense why: this simplifies your parser,
> letting you (Nadim) concentrate on more important stuff).
> 
> Currently, we have to declare a new constant for each call of
> HMACVERIF:
> 
>    unused1 = HMACVERIF(tag1, real tag1)
>    unused2 = HMACVERIF(tag2, real tag2)
>    unused3 = HMACVERIF(tag3, real tag3)
> 
> But we never use those constants! So I was thinking of two possible
> alternatives. The first one is simply to allow some primitives to not
> have otuputs at all (currently only HMACVERIF):
> 
>    HMACVERIF(tag1, real tag1)
>    HMACVERIF(tag2, real tag2)
>    HMACVERIF(tag3, real tag3)
> 
> The second one is to have a special keyword for ignored outputs:
> 
>    _ = HMACVERIF(tag1, real tag1)
>    _ = HMACVERIF(tag2, real tag2)
>    _ = HMACVERIF(tag3, real tag3)
> 
> We could use "null" or "nil" instead of "_". The Ocaml programming
> language does this: "_" is a place holder for ignored variables (useful
> for pattern matching), so the compiler doesn't complain with "unused
> variable".
> 
> We could also interpret that keyword as a known public constant
> (without requiring users to declare it). This would facilitate some
> questionable uses of HKDF, such as:
> 
>    key1, key2 = HKDF(_, ikm, _)
> 
> But that's a separate feature, and a potentially confusing one. We
> might want to force the user to be explicit there.
> 
> ---
> 
> My personal preference would be to use "_" as a special keyword for
> unused values (on the left of the "=" sign). It's a clear marker that
> the user intend to ignore that output, and keeps the syntax simple and
> regular.
> 
> Ideally, I think we would:
> 
> - Mandate that HMACVERIF use "_" as its output.
> - Allow SIGNVERIF to use "_" as its output.
> - Forbid the other primitives to use "_" as their output.
> 
> (Personally, I'm not sure the output of SIGNVERIF has any use. NaCl
> wanted to make sure users didn't forget to verify the signature, but
> Verifpal is not a C program: if we forget to verify a signature, the
> model will likely be vulnerable, and Verifpal will catch the problem.)
> 
> Loup.
> 
> 
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal