law tdes_ecb_round_trip
bend-osdev-legacy-ciphers@0.1.0.0 · LAWS.bend:239
import bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend as LAWS
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
239law tdes_ecb_round_trip:
240 for +k: T.LcTdesKey
241 for +bs: List<&2, L.LcBlock64>
242 {X.Lc64.ecb_decrypt_blocks(~T.LcTdesKey, ~T.LcTdes.decrypt, k, X.Lc64.ecb_encrypt_blocks(~T.LcTdesKey, ~T.LcTdes.encrypt, k, bs)) == bs : List<&2, L.LcBlock64>}