[Verifpal] (Feature request) Unifying primitives

Thu Aug 29 16:42:12 CEST 2019

Dear Nadim,

Thanks for the quick answer. I'll be able to check Monokex with
Verifpal, and *at last* be reasonably sure I didn't make some fatal
mistake (my earlier attempts had several such mistakes).

About unifying hash primitives, I agree with you. Giving HKDF arbitrary
inputs or adding a GENERIC_HASH would be confusing. We'd better not.

Allowing HASH several outputs however could be neat for stuff like hash
splitting: take a 512-bit hash, cut it in half, use both halves for
different purposes (like 2 different session keys). Monokex does this
at the end of the handshake: with one hash, we can have two keys.

About HMACVERIF… sorry, I must have been tired when I read your manual.
This is *exactly* what I need.  I may have been mislead by the "unused"
output, which I had interpreted to mean that the whole primitive was
not even implemented. The syntax is not ideal, though, I'll talk about
it in a separate thread.

Loup.

On Thu, 2019-08-29 at 15:14 +0200, Nadim Kobeissi wrote:
> 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
> 
> 