[Verifpal] (Feature request) Unifying primitives

[Nadim Kobeissi]

Don’t forget that Verifpal is still under development, and may miss attacks :-)

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

> On Aug 29, 2019, at 4:42 PM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
> 
> 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
>> 
>> 
>