[Verifpal] Nonce reuse in Verifpal models

Nadim Kobeissi nadim at symbolic.software
Sat Nov 28 18:36:22 CET 2020


Dear Loup,

First, I want to thank Mike for assisting with answering Loup’s question.

> - Does ENC() behaves as if it uses a different nonce each time?

No, absolutely not. Mike’s answer is correct.

> - Is there any difference in the engine between using ENC or HKDF?

In the symbolic model and for the purposes of your model, using your HKDF workaround should be fine. You could also concatenate the key with a nonce and use that as the key.

For more information, please review slides 8, 9 and potentially subsequent slides in this presentation:
https://prosecco.gforge.inria.fr/personal/bblanche/talks/Facebook16.pdf

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

> On Nov 25, 2020, at 1:10 PM, Loup Vaillant-David <loup at loup-vaillant.fr> wrote:
> 
> Hi,
> 
> 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
> about:
> 
>    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
> other.
> 
> 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?
> 
> Thanks,
> Loup.
> 
> 
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal



More information about the Verifpal mailing list