def gctr_part1

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

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

244def gctr_part1(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +x0: U32, +cb: List<&2, U32>) -> {G.gctr(nk, nr, key, [x0], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n))] : List<&2, U32>}:
245  %Equal.sym(List<&2, U32>, S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), [S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 0n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 1n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 2n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 3n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 4n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 5n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 6n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 7n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 8n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 9n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 10n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 11n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 12n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 13n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 14n), S.nth_byte(S.bytes_of(S.encrypt(nk, nr, key, S.state_of(cb))), 15n)], ks_ok(S.encrypt(nk, nr, key, S.state_of(cb)))) : {G.xor_bytes([x0], _) == [U32.xor(x0, kb(nk, nr, key, cb, 0n))] : List<&2, U32>}
246  {==}