law Cipher.value

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/laws.bend:58

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes.bend as A
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S

58# The implementation's cipher with its expanded key is FIPS 197's Cipher
59# with KeyExpansion, for every Nk, Nr, key and state.
60law Cipher.value:
61  for +nk: Nat
62  for +nr: Nat
63  for +key: List<&2, U32>
64  for +s: T.State
65  {A.encrypt(nk, nr, key, s) == S.encrypt(nk, nr, key, s) : T.State}