problematic-solution-crypto

void expand(u8 out[32], const u8 in[32], u32 x, u32 y)
{
    for (u32 i = 0; i < 32; ++i)
    {
        out[i] = (in[i] - x) ^ y;

        x = ROL(x, 1);
        y = ROL(y, 1);
    }
}


x = symbolic value
y = symbolic value

Algo:

First, try to solve the problem by hand a bit to develop a feel of the difficulty of the problem. For any single byte pair of plaintext and ciphertext (pi, ci) it’s quite easy to find 8 bits within the key so that the mapping is correct. In fact, you can choose ANY byte in EBX to subtract, since you can adjust the difference via the xor by the corresponding byte in EDX.
The value of the key for each byte mapping is completely open ended (256 possibilities). But actually choosing a value for the key for that mapping propagates a constraint across the possibilities of the other parts of the key. And this is the beauty of the algorithm.


Conditional statement - ~(P → Q) = ~( ~ P V Q) = P Λ ~Q

E.g FFFF:


\begin{array}{lr}
& (\sin(x)^3 = \cos(\log(y)\cdot x) \vee b \vee -x^2 \geq 2.3y) \wedge \left(\neg b \vee y < -34.4 \vee \exp(x) > {y \over x}\right)
\end{array}
where
b \in {\mathbb B}, x,y \in {\mathbb R}
OR
https://upload.wikimedia.org/math/3/2/6/326141c4149d5f41a2f281cc388370ec.png
where
https://upload.wikimedia.org/math/7/7/8/7782c0a89922c157cf16f3b34eae56b9.png

Get qabaga gel dala :F
sym1 = x
sym2 = y

shl edx, 0xF   ; EDX=sym1 << 0xf
add edx, 0b10001   ; EDX=((sym1 << 0xf) + 17)
not edx	; EDX ~= (sym1 << 0xf) + 17)
and edx, 0xfffffff   ; EDX= ~((sym1 << 0xf) + 17) & 0xfffffff)
sub eax,0x2 ; EAX = sym2 - 0x2
xor eax, edx ; EAX=(sym2 - 0x2) ^ ~((sym1 << 0xf) + 17) & 0xfffffff)

we are to use z3 to try find specific value.

solve(((sym2 - 0x2) ^ ~(((sym1 << 0xf) + 17) & 0xfffffff)) == 0x3b17f78)