[Verifpal] Nonce reuse in Verifpal models

Loup Vaillant-David loup at loup-vaillant.fr
Wed Nov 25 13:10:05 CET 2020


We are currently trying to translate my last version of the Monokex
protocols into Verifpal models. There's one step I'm not too sure

    H1 || K1 = STREAM_CIPHER(key=H0, nonce=0, plaintext=zeroes)

(`||` denotes concatenation, H1 and K1 are 32-byte strings, and the
plaintext is 64-bytes long.)

Basically, I'm doing key derivation with a stream cipher. Which should
be okay because of reasons. Our problem here is that Verifpal can't
split the ciphertext in two. We need to work around that.

The first workaround I've thought of just uses HKDF:

    H1, K1 = HKDF(zero, H0, zero)

But that's not very honest. I'm using a stream cipher here, not a key
derivation algorithm. Deriving keys with stream ciphers only works when
the input key material is already a suitable key.

The second workaround uses ENC twice:

    H1 = ENC(H0, zero)
    K1 = ENC(H0, zero)

But then I have another problem: in the real world, this would mean
nonce reuse, and I'd have H1 == K1. So unless Verifpal considers
different ENC calls to be independent as if they had different nonces,
I may have problems with K1 and H1 not being independent from each

So my questions are:

- Does ENC() behaves as if it uses a different nonce each time?
- Is there any difference in the engine between using ENC or HKDF?


More information about the Verifpal mailing list