An amature cryptographer posted a new block cipher called xcrush. Usually I ignore these posts, but seeing as this guy knew it to be an educational exercise and made a somewhat digestable document I took the bait.
A common question to ask is if the key expansion function is injective. This is important because a non-injective key expansion function means two keys result in the same block cipher operation, and thus the security is actually less than the key size would lead one to believe.
While some block ciphers have a trivially injective key expansion, such as Simon or Speck, a quick glance at this specification shows the key expansion is far more complex. It didn't take much work to make a Cryptol specification (http://www.cryptol.net) and ask a solver to show me if the expansion is indeed injective.
This document is literate Cryptol and can be loaded and executed by Cryptol. Notice I am not trying to teach Cryptol or the XCrush algorithm, there are acceptable sources for both these tasks already. As such, here is a huge blob of code that implements XCrush followed by the query.
Key_Expansion : [2][64] -> [16][64]
Key_Expansion k = take `{16} [Y | (Y,_) <- drop `{1} ys2]
where
S0 : [5][64]
S0 = take `{5} (k # [Cx,Cx,Cx])
ys1 = [ (zero, S0) ] # [ N S | (_,S) <- ys1 ]
S1 : [5][64]
S1 = (ys1@10).1
ys2 = [(zero,S1)] # [ N S | (_,S) <- ys2]
Cx : [64]
Cx = 4142135623730950488
N : [5][64] -> ([64], [5][64])
N S0 = (Y,S)
where
S = [S1,S2,S3,S4,S5]
T = S0 @ 1
S2 = S0 @ 2
S3 = S0 @ 3
S4 = S0 @ 4
S5 = S0 @ 0
Y = A (S0 @ 0) ((S0@0) + T)
S1 = Y
A : [64] -> [64] -> [64]
A x a = (x + a) <<< (C a)
C : [64] -> [64]
C x = y
where
x0 = (x >> 32) + x
x1 = (x0 >> 11) ^ x0
x2 = (x1 >> 9) + x1
x3 = (x2 >> 6) + x2
y = x3 && `0x3f
Now the interesting part is the question "Do all distinct keys result in distinct expansions?" Or perhaps "Prove distinct keys implies distinct expansions." In logical primitives this can be formed as "Prove that for any two keys, either they are equal or their expansions are not equal." Such a formulation of implication is common and frequently observed in Cryptol... or Cryptol code that I write at least.
The property is:
property injective_expansion k1 k2 = k1 == k2 || Key_Expansion k1 != Key_Expansion k2
To execute this property just load this markdown document into cryptol and try
(after selecting your prover) :prove injective_expansion. The computer will think hard
for a while then give you a counter example, meaning that the function is not injective.