law tdes_cbc_round_trip
bend-osdev-legacy-ciphers@0.1.0.0 · LAWS.bend:244
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
244law tdes_cbc_round_trip:
245 for +k: T.LcTdesKey
246 for +iv: L.LcBlock64
247 for +bs: List<&2, L.LcBlock64>
248 {X.Lc64.cbc_decrypt_blocks(~T.LcTdesKey, ~T.LcTdes.decrypt, k, iv, X.Lc64.cbc_encrypt_blocks(~T.LcTdesKey, ~T.LcTdes.encrypt, k, iv, bs)) == bs : List<&2, L.LcBlock64>}