law blowfish_block_round_trip_dual

bend-osdev-crypto@0.1.0.0 · LAWS.bend:975

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/blowfish.bend as Bf

975# Blowfish (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
976law blowfish_block_round_trip_dual:
977  for k: Bf.LcBlowfishKey
978  for +b: L.LcBlock64
979  {Bf.LcBlowfish.encrypt(k, Bf.LcBlowfish.decrypt(k, b)) == b : L.LcBlock64}