The Gimli non-linear operator

NORX replaces all the additions of the Chacha20 quarter-round function with the non-linear $$x \oplus y \oplus ((x \land y) \ll 1)$$ operation. Gimli supposedly improves on it with $$x \oplus y \oplus ((z \land y) \ll 1)$$, adding a third input $$z$$ because as they claim it removes the need for the additional xor that NORX has. In addition the Gimli paper says "Gimli varies the 1-bit shift distance, improving diffusion compared to NORX and possibly even compared to ARX". So we end up with $$a \gets z \oplus y \oplus ((x \land y) \ll 3) \\ b \gets y \oplus x \oplus ((x \lor z) \ll 1) \\ c \gets x \oplus (z \ll 1) \oplus ((y \land z) \ll 2)$$

My issue with this is that nowhere in the Gimli specification (as far as I could tell anyway) it explains why they did $$z \ll 1$$ or why they used bitwise or in $$x \lor z$$ nor does it explain the exact parameter choices for the non-linear operation (why $$a \gets z \oplus y \oplus ((x \land y) \ll 3)$$ rather than $$a \gets z \oplus x \oplus ((z \land y) \ll 3)$$ for example).

Is there any justification for these changes that I might have missed?

• I don't see a $c<<1$ in the equations. You do realize that the alternative expression you suggest is algebraically equivalent to what they have (one of the AND'ed variables appears as a term in the outside sum, as well as a third variable which is not AND'ed) – kodlu Mar 31 '20 at 23:31
• @kodlu Apologies, fixed it. As for the rest of your comment I am not sure what you mean. – Bob Semple Mar 31 '20 at 23:37
• Take $a\leftarrow x_1\oplus x_2 \oplus ((x_1 \land x_3)<<3).$ Due to commutativity both of the expressions above are equivalent to this. – kodlu Mar 31 '20 at 23:59
• Yes, I am aware of that. – Bob Semple Apr 1 '20 at 0:12

a bit late, if I had been pinged on this, I could have answered earlier.

• $$x \vee z$$ was chosen for the following reason:

• $$a \wedge b$$ is biased towards 0. As a result if we only used $$\wedge$$ the linear weight of the equation would have a strong bias towards 0.
• As $$a \vee b$$ is biased towards 1, this aims to compensate.
• The $$z ≪ 1$$ instead of just $$z$$ in the equation is necessary to ensure that this is a permutation, otherwise the equations do not have an inverse and we really wanted a permutation and not a transformation.

• As for the why $$𝑧⊕𝑥⊕((𝑧∧𝑦)≪3)$$, if you remove the $$x \leftrightarrow z$$ swap, you realize that the shape of the expression is:
$$x \leftarrow x \oplus z' \oplus EXPR$$
$$y \leftarrow y \oplus x \oplus EXPR$$
$$z \leftarrow z \oplus y \oplus EXPR$$
We already discussed why $$z'$$ is $$z ≪ 1$$, now if you look at $$EXPR$$ you notice that in all cases, the destination is not included in the non-linear binary expression, as a result, this increase the complexity of linear trails as you have to track more variables.