def ecb_rt_tdes

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

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

8655def ecb_rt_tdes(+k: T.LcTdesKey, bs: List<&2, L.LcBlock64>) -> {bs == X.m64.ecb(~T.LcTdesKey, ~T.LcTdes.decrypt, k, X.m64.ecb(~T.LcTdesKey, ~T.LcTdes.encrypt, k, bs)) : List<&2, L.LcBlock64>}:
8656  match bs:
8657    case Nil{}:
8658      {==}
8659    case Con{+b, +t}:
8660      %tdes_rt(k, b) : {Con{b, t} == Con{_, X.m64.ecb(~T.LcTdesKey, ~T.LcTdes.decrypt, k, X.m64.ecb(~T.LcTdesKey, ~T.LcTdes.encrypt, k, t))} : List<&2, L.LcBlock64>}
8661      %ecb_rt_tdes(k, t) : {Con{b, t} == Con{b, _} : List<&2, L.LcBlock64>}
8662      {==}