proofs/crypto/aes/ghash.bend checks
raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash.bend as Ghash
10 imports
import Base import ../../../src/crypto/aes/types.bend as T import ../../../src/crypto/aes/aes.bend as A import ../../../src/crypto/aes/gcm.bend as I import ../../../spec/crypto/aes/poly.bend as P import ../../../spec/crypto/aes/aes.bend as S import ../../../spec/crypto/aes/gcm.bend as G import ./gf.bend as GF import ./ghash_defs.bend as D import ./ghash_bits.bend as B
Definitions
def step_ok source · line 18 · raw
@+c:Bool -> @+z:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Block -> @+v:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Block -> @+rest:List<&2, Bool> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.F(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc{z, v}, c <> rest) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.F(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.step(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.bit(c), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc{z, v}), rest) : Word(128n)}One bit of Algorithm 1: Z += c*V, V = V*x.
def steps_ok source · line 23 · raw
@+cs:List<&2, Bool> -> @+acc:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc -> @+rest:List<&2, Bool> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.F(acc, List.append(&2, Bool, cs, rest)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.F(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.steps(cs, acc), rest) : Word(128n)}
def steps_append source · line 33 · raw
@+l1:List<&2, Bool> -> @+l2:List<&2, Bool> -> @+acc:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.steps(List.append(&2, Bool, l1, l2), acc) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.steps(l2, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.steps(l1, acc)) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc}
def mul_bytes_steps source · line 40 · raw
@+xs:List<&2, U32> -> @+acc:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.mul_bytes(xs, acc) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.steps(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.string_bits(xs), acc) : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc}
def append_nil source · line 49 · raw
@+l:List<&2, Bool> -> {List.append(&2, Bool, l, []) == l : List<&2, Bool>}
def f_nil source · line 57 · raw
@+acc:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.F(acc, []) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.acc_z(acc)) : Word(128n)}
def absorb_ok source · line 63 · raw
@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Block -> @+y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Block -> @+x0:U32 -> @+x1:U32 -> @+x2:U32 -> @+x3:U32 -> @+x4:U32 -> @+x5:U32 -> @+x6:U32 -> @+x7:U32 -> @+x8:U32 -> @+x9:U32 -> @+x10:U32 -> @+x11:U32 -> @+x12:U32 -> @+x13:U32 -> @+x14:U32 -> @+x15:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.mul(Word.xor(128n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(y), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(h)) : Word(128n)}(Y xor X) * H for one 16-byte block.
def ghash_ok source · line 75 · raw
@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Block -> @+xs:List<&2, U32> -> @+rest:List<&2, U32> -> @+y:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Block -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.ghash(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(h), List.append(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.pad(xs), rest), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(y)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.ghash(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(h), rest, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.ghash(h, xs, y))) : Word(128n)}GHASH over X || 0^v (then more blocks) is the implementation's GHASH over X.
def ghash_all_ok source · line 129 · raw
@+h:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Block -> @+aad:List<&2, U32> -> @+c:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.ghash(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(h), List.append(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.pad(aad), List.append(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.pad(c), List.append(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.len64(aad), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.len64(c)))), Word.zero(128n)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.ghash(h, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.lengths(aad, c), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.ghash(h, c, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.ghash(h, aad, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.zero)))) : Word(128n)}GHASH_H(A || 0^v || C || 0^u || [len(A)]_64 || [len(C)]_64).
def pack_ok source · line 143 · raw
@+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.R(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.pack(st)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.block(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bytes_of(st)) : Word(128n)}The hash subkey: the implementation packs E_K(0^128) into words.