[Verifpal] (Feature request) Unifying primitives

[Loup Vaillant David]

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.