law aria_block_round_trip_dual

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

import bend-osdev-crypto@0.1.0.0/LAWS.bend as LAWS
import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-legacy-ciphers@0.1.0.0/aria.bend as Ar

887# ARIA (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
888law aria_block_round_trip_dual:
889  for k: Ar.LcAriaKey
890  for +b: M.CmBlock
891  {Ar.LcAria.encrypt(k, Ar.LcAria.decrypt(k, b)) == b : M.CmBlock}

Uses (5)

Used by (0)

No other definition uses this definition.