[Verifpal] (Feature request) Unifying primitives

[Nadim Kobeissi]

Dear Loup,

I want to thank you for your interest in Verifpal. It makes me very happy to see the discussion rolling and I really hope we get to discuss more on this list! Also, thank you for your pull request earlier today. My terminal was inserting the newline automatically, so I didn’t run into this issue — but I’m sure others did and I thank you for addressing it.

I will try to answer your points in an organized way:

———————————————————
1. UNIFYING HASH PRIMITIVES
———————————————————

Despite your being correct in that the symbolic model representations of all of Verifpal’s hash functions is similar, I would rather use the triple (HASH, HMAC, HKDF) instead of a unified GENERIC_HASH for two reasons:

a. In the real world, these primitives output different values, i.e. they are different one-way maps. As such, describing them as discrete black boxes in Verifpal illustrates that they behave as discrete one-way maps in real-world cryptography.

b. GENERIC_HASH could be confusing for students and engineers who may have a more “practical crypto” background or expectations, where constructions like HASH and HMAC are common.

I am also against giving HKDF arbitrary inputs because that is not how the scheme works or how it is described in its specification, which labels it with three distinct inputs: salt, ikm and info. Furthermore, note that HASH already accepts arbitrary inputs, so why the bother? I would probably be fine with making HASH produce an arbitrary number of *outputs* (like HKDF does presently), if that would be helpful.

Finally, regarding this construction which is useful to Monokex:
> new_hash, tag = HKDF(old_hash) // I need only one input

For now, I guess what you could do is have principals `knows public null` (representing a null constant), and do this:
> new_hash, tag = HKDF(old_hash, null, null)

———————————————————
2. UNIFYING ENCRYPTION PRIMITIVES
———————————————————

ENC* and AEAD_* are not similar!

a. AEAD_DEC can actually fail on decryption, whereas decryption failures are impossible to cryptographically ascertain with DEC [0]. That’s why AEAD_DEC is a checkable primitive in Verifpal.

b. You say: “the manual doesn't seem to mention something like VERIFY or CHECK_EQUAL, making it difficult to separate authentication from encryption”. I’m happy to inform you that this is not the case! The manual indeed specifies a useful, and checkable, HMACVERIF primitive. You can read more about it on page 13 of Print 1 of the First Edition of the manual [1]. Incidentally, HMACVERIF can be used to check the equality of things other than HMACs.

——— 

Footnotes:
[0] Admittedly, in the real world, this is a bit different since an attacker can very often assume some kind of encoding or structure on the plaintext, and interpret a lack of ASCII or MIME-type-specific output on decryption as decryption failure.
[1] I’m just specifying the print and edition in case people read this email much later in the future, whence the manual's pagination could have evolved.

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

> On Aug 29, 2019, at 2:28 PM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
> 
> Hi,
> 
> I have noticed that some of the primitives here are very similar. The
> most obvious examples is the HASH/HMAC/HKDF triple. While their
> implementations are typically different, in the symbolic model they're
> all a random oracle with a number of inputs and a number of outputs.
> 
> I sense those three could be generalised thus:
> 
>    out1, out2, out3 = GENERIC_HASH(in1, in2, in3)
> 
> Or we could just modify HKDF so it accepts an arbitrary number of
> inputs, instead of exactly 3. That may be simpler, considering that
> HASH, HMAC, and HKDF do differ in their actual implementation.
> 
> (The motivation behind that one is mainly to take advantage of the
> multiple outputs of HKDF, without having to feed it with 3 inputs (2
> inputs are often enough).)
> 
> ---
> 
> Likewise, ENC/DEC, and AEAD_ENC/AEAD_DEC are pretty similar. I get the
> feeling that we should be able to implement the latter in terms of the
> former. That is we should be able to replace this:
> 
>    ciphertext = AEAD_ENC(key, plaintext, ad)
>    ...
>    Alice -> Bob : ad, ciphertext
>    ...
>    plaintext_ = AEAD_DEC(key, ciphertext, ad)?
> 
> 
> by (something like) that:
> 
>    ciphertext = ENC(key, plaintext)
>    tag        = HMAC(key, ciphertext, ad)
>    ...
>    Alice -> Bob : ad, ciphertext, tag
>    ...
>    real_tag  = HMAC(key, ciphertext, ad)
>    CHECK_EQUAL(tag, real_tag)?
>    plaintext_ = DEC(key, ciphertext)
> 
> or like this:
> 
>    ciphertext = ENC(key, plaintext)
>    tag        = AUTH(key,
> ciphertext, ad)
>    ...
>    Alice -> Bob : ad, ciphertext, tag
>    ...
> 
> VERIFY(key, ciphertext, ad, tag)?
>    plaintext_ = DEC(key, ciphertext)
> 
> The manual doesn't seem to mention something like VERIFY or
> CHECK_EQUAL, making it difficult to separate authentication from
> encryption. Right now I'm not sure it's even possible.
> 
> The motivation for this comes from Monokex: instead of using a standard
> AEAD construction, Monokex mixes all inputs (transcript and DH shared
> secrets) within the current hash. Authentication tags are simply
> derived from the current hash:
> 
>    new_hash = HASH(old_hash, zero)
>    tag      = HASH(old_hash, one)
> 
> Or, more simply:
> 
>    new_hash, tag = HKDF(old_hash) // I need only one input
> 
> 
> To give a more complete example, an encrypted payload in Monokex goes
> like this:
> 
>    H1         = HASH(H0, zero)
>    key        = HASH(H0, one)
>    ciphertext = ENC(key, plaintext)
>    H2         = HASH(H1, ciphertext)
>    H3         = HASH(H2, zero)
>    tag        = HASH(H2, one)
>    ...
>    Alice -> Bob : ciphertext, tag
> 
> Or, more simply:
> 
>    H1, key    = HKDF(H0)
>    ciphertext = ENC(key, plaintext)
>    H2    
> = HASH(H1, ciphertext)
>    H3, tag    = HKDF(H2)
>    ...
>    Alice -> Bob
> : ciphertext, tag
> 
> My problem here is that to model this, I need a way to check for
> equality directly, or at least find a way to cheat. (And if there's a
> way to cheat, having syntax sugar for that could be great.)
> 
> ---
> 
> Any chance of making those unifications happen? The first one (hashes)
> is a minor convenience feature, but the last one (adding equality
> verification so that I can do authentication without AEAD_*), if
> possible, would really help.
> 
> Loup.
> 
> 
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal