def gctr_part11

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

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

284def gctr_part11(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, +x8: U32, +x9: U32, +x10: U32, +cb: List<&2, U32>) -> {G.gctr(nk, nr, key, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10], cb) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n))] : List<&2, U32>}:
285  %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, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10], _) == [U32.xor(x0, kb(nk, nr, key, cb, 0n)), U32.xor(x1, kb(nk, nr, key, cb, 1n)), U32.xor(x2, kb(nk, nr, key, cb, 2n)), U32.xor(x3, kb(nk, nr, key, cb, 3n)), U32.xor(x4, kb(nk, nr, key, cb, 4n)), U32.xor(x5, kb(nk, nr, key, cb, 5n)), U32.xor(x6, kb(nk, nr, key, cb, 6n)), U32.xor(x7, kb(nk, nr, key, cb, 7n)), U32.xor(x8, kb(nk, nr, key, cb, 8n)), U32.xor(x9, kb(nk, nr, key, cb, 9n)), U32.xor(x10, kb(nk, nr, key, cb, 10n))] : List<&2, U32>}
286  {==}