law aes_round_trip

bend-osdev-aes@0.1.0.0 · LAWS.bend:8

import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
import bend-osdev-aes@0.1.0.0/aes.bend as X

8# AES (aes.bend): decryption undoes encryption, for every key (every value
9# of CmAesKey, whatever its number of rounds and round keys: AES-128, AES-192
10# and AES-256 among them) and every block
11law aes_round_trip:
12  for k: X.CmAesKey
13  for +b: M.CmBlock
14  {X.CmAes.decrypt(k, X.CmAes.encrypt(k, b)) == b : M.CmBlock}