proofs/crypto/aes/ghash_defs.bend checks
raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend as Ghash_defs
4 imports
import Base import ../../../src/crypto/aes/gcm.bend as I import ../../../spec/crypto/aes/gcm.bend as G import ./gf.bend as GF
Definitions
def R source · line 11 · raw
@z:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Block -> Word(128n)
The field element of an implementation block (its 16 bytes, as SP 800-38D reads them).
def bit source · line 15 · raw
@c:Bool -> U32
The U32 the implementation reads for a coefficient c.
def F source · line 20 · raw
@acc:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc -> @cs:List<&2, Bool> -> Word(128n)
Algorithm 1 continued from an implementation accumulator (Z, V) over the coefficients cs.
def steps source · line 26 · raw
@cs:List<&2, Bool> -> @acc:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc -> 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.Acc
The implementation's steps over a list of coefficients.