def cbc_rt_tdes

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

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/tdes.bend as T
import bend-osdev-legacy-ciphers@0.1.0.0/modes64.bend as X

8664def cbc_rt_tdes(+k: T.LcTdesKey, bs: List<&2, L.LcBlock64>, +iv: L.LcBlock64) -> {bs == X.m64.cbc.dec(~T.LcTdesKey, ~T.LcTdes.decrypt, k, X.m64.cbc.enc(~T.LcTdesKey, ~T.LcTdes.encrypt, k, bs, iv), iv) : List<&2, L.LcBlock64>}:
8665  match bs:
8666    case Nil{}:
8667      {==}
8668    case Con{+p, +t}:
8669      %tdes_rt(k, L.LcBlock64.xor(iv, p)) : {Con{p, t} == Con{L.LcBlock64.xor(iv, _), X.m64.cbc.dec(~T.LcTdesKey, ~T.LcTdes.decrypt, k, X.m64.cbc.enc(~T.LcTdesKey, ~T.LcTdes.encrypt, k, t, T.LcTdes.encrypt(k, L.LcBlock64.xor(iv, p))), T.LcTdes.encrypt(k, L.LcBlock64.xor(iv, p)))} : List<&2, L.LcBlock64>}
8670      %b64_xx2(iv, p) : {Con{p, t} == Con{_, X.m64.cbc.dec(~T.LcTdesKey, ~T.LcTdes.decrypt, k, X.m64.cbc.enc(~T.LcTdesKey, ~T.LcTdes.encrypt, k, t, T.LcTdes.encrypt(k, L.LcBlock64.xor(iv, p))), T.LcTdes.encrypt(k, L.LcBlock64.xor(iv, p)))} : List<&2, L.LcBlock64>}
8671      %cbc_rt_tdes(k, t, T.LcTdes.encrypt(k, L.LcBlock64.xor(iv, p))) : {Con{p, t} == Con{p, _} : List<&2, L.LcBlock64>}
8672      {==}