def cbc_rt_des

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:8634

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
import bend-osdev-legacy-ciphers@0.1.0.0/des.bend as D
import bend-osdev-legacy-ciphers@0.1.0.0/modes64.bend as X

8634def cbc_rt_des(+k: D.LcDesKey, bs: List<&2, L.LcBlock64>, +iv: L.LcBlock64) -> {bs == X.m64.cbc.dec(~D.LcDesKey, ~D.LcDes.decrypt, k, X.m64.cbc.enc(~D.LcDesKey, ~D.LcDes.encrypt, k, bs, iv), iv) : List<&2, L.LcBlock64>}:
8635  match bs:
8636    case Nil{}:
8637      {==}
8638    case Con{+p, +t}:
8639      %des_rt(k, L.LcBlock64.xor(iv, p)) : {Con{p, t} == Con{L.LcBlock64.xor(iv, _), X.m64.cbc.dec(~D.LcDesKey, ~D.LcDes.decrypt, k, X.m64.cbc.enc(~D.LcDesKey, ~D.LcDes.encrypt, k, t, D.LcDes.encrypt(k, L.LcBlock64.xor(iv, p))), D.LcDes.encrypt(k, L.LcBlock64.xor(iv, p)))} : List<&2, L.LcBlock64>}
8640      %b64_xx2(iv, p) : {Con{p, t} == Con{_, X.m64.cbc.dec(~D.LcDesKey, ~D.LcDes.decrypt, k, X.m64.cbc.enc(~D.LcDesKey, ~D.LcDes.encrypt, k, t, D.LcDes.encrypt(k, L.LcBlock64.xor(iv, p))), D.LcDes.encrypt(k, L.LcBlock64.xor(iv, p)))} : List<&2, L.LcBlock64>}
8641      %cbc_rt_des(k, t, D.LcDes.encrypt(k, L.LcBlock64.xor(iv, p))) : {Con{p, t} == Con{p, _} : List<&2, L.LcBlock64>}
8642      {==}