def aria_xor2

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:7915
import bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-legacy-ciphers@0.1.0.0/aria.bend as A

7915# a round key XORed twice
7916def aria_xor2(s: A.LcAriaSt, k: M.CmBlock) -> {s == A.aria.xor(A.aria.xor(s, k), k) : A.LcAriaSt}:
7917  match s k:
7918    case A.LcAriaSt{+x0, +x1, +x2, +x3, +x4, +x5, +x6, +x7, +x8, +x9, +x10, +x11, +x12, +x13, +x14, +x15} M.CmBlock{U32{+k0}, U32{+k1}, U32{+k2}, U32{+k3}}:
7919      %word_xx(8n, x0, A.aria.byte0(k0)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{_, Word.xor(8n, Word.xor(8n, x1, A.aria.byte1(k0)), A.aria.byte1(k0)), Word.xor(8n, Word.xor(8n, x2, A.aria.byte2(k0)), A.aria.byte2(k0)), Word.xor(8n, Word.xor(8n, x3, A.aria.byte3(k0)), A.aria.byte3(k0)), Word.xor(8n, Word.xor(8n, x4, A.aria.byte0(k1)), A.aria.byte0(k1)), Word.xor(8n, Word.xor(8n, x5, A.aria.byte1(k1)), A.aria.byte1(k1)), Word.xor(8n, Word.xor(8n, x6, A.aria.byte2(k1)), A.aria.byte2(k1)), Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7920      %word_xx(8n, x1, A.aria.byte1(k0)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, _, Word.xor(8n, Word.xor(8n, x2, A.aria.byte2(k0)), A.aria.byte2(k0)), Word.xor(8n, Word.xor(8n, x3, A.aria.byte3(k0)), A.aria.byte3(k0)), Word.xor(8n, Word.xor(8n, x4, A.aria.byte0(k1)), A.aria.byte0(k1)), Word.xor(8n, Word.xor(8n, x5, A.aria.byte1(k1)), A.aria.byte1(k1)), Word.xor(8n, Word.xor(8n, x6, A.aria.byte2(k1)), A.aria.byte2(k1)), Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7921      %word_xx(8n, x2, A.aria.byte2(k0)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, _, Word.xor(8n, Word.xor(8n, x3, A.aria.byte3(k0)), A.aria.byte3(k0)), Word.xor(8n, Word.xor(8n, x4, A.aria.byte0(k1)), A.aria.byte0(k1)), Word.xor(8n, Word.xor(8n, x5, A.aria.byte1(k1)), A.aria.byte1(k1)), Word.xor(8n, Word.xor(8n, x6, A.aria.byte2(k1)), A.aria.byte2(k1)), Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7922      %word_xx(8n, x3, A.aria.byte3(k0)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, _, Word.xor(8n, Word.xor(8n, x4, A.aria.byte0(k1)), A.aria.byte0(k1)), Word.xor(8n, Word.xor(8n, x5, A.aria.byte1(k1)), A.aria.byte1(k1)), Word.xor(8n, Word.xor(8n, x6, A.aria.byte2(k1)), A.aria.byte2(k1)), Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7923      %word_xx(8n, x4, A.aria.byte0(k1)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, _, Word.xor(8n, Word.xor(8n, x5, A.aria.byte1(k1)), A.aria.byte1(k1)), Word.xor(8n, Word.xor(8n, x6, A.aria.byte2(k1)), A.aria.byte2(k1)), Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7924      %word_xx(8n, x5, A.aria.byte1(k1)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, _, Word.xor(8n, Word.xor(8n, x6, A.aria.byte2(k1)), A.aria.byte2(k1)), Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7925      %word_xx(8n, x6, A.aria.byte2(k1)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, _, Word.xor(8n, Word.xor(8n, x7, A.aria.byte3(k1)), A.aria.byte3(k1)), Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7926      %word_xx(8n, x7, A.aria.byte3(k1)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, _, Word.xor(8n, Word.xor(8n, x8, A.aria.byte0(k2)), A.aria.byte0(k2)), Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7927      %word_xx(8n, x8, A.aria.byte0(k2)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, _, Word.xor(8n, Word.xor(8n, x9, A.aria.byte1(k2)), A.aria.byte1(k2)), Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7928      %word_xx(8n, x9, A.aria.byte1(k2)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, _, Word.xor(8n, Word.xor(8n, x10, A.aria.byte2(k2)), A.aria.byte2(k2)), Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7929      %word_xx(8n, x10, A.aria.byte2(k2)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, _, Word.xor(8n, Word.xor(8n, x11, A.aria.byte3(k2)), A.aria.byte3(k2)), Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7930      %word_xx(8n, x11, A.aria.byte3(k2)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, _, Word.xor(8n, Word.xor(8n, x12, A.aria.byte0(k3)), A.aria.byte0(k3)), Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7931      %word_xx(8n, x12, A.aria.byte0(k3)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, _, Word.xor(8n, Word.xor(8n, x13, A.aria.byte1(k3)), A.aria.byte1(k3)), Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7932      %word_xx(8n, x13, A.aria.byte1(k3)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, _, Word.xor(8n, Word.xor(8n, x14, A.aria.byte2(k3)), A.aria.byte2(k3)), Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7933      %word_xx(8n, x14, A.aria.byte2(k3)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, _, Word.xor(8n, Word.xor(8n, x15, A.aria.byte3(k3)), A.aria.byte3(k3))} : A.LcAriaSt}
7934      %word_xx(8n, x15, A.aria.byte3(k3)) : {A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15} == A.LcAriaSt{x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, _} : A.LcAriaSt}
7935      {==}
def aria_xor2

Uses (10)

Used by (2)
