def kb

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G

49# Byte i of the keystream block of counter block cb.
50def kb(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +cb: List<&2, U32>, +i: Nat) -> U32:
51  S.nth_byte(G.ciph(nk, nr, key, cb), i)