proofs/crypto/aes/ghash_defs.bend

bend-collections-laws-crypto@1.0.0.0 · 31 lines · 4 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend as I
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G
4import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gf.bend as GF
5
6# The relation between the implementation's GHASH state and the
7# specification's field elements.
8
9# The field element of an implementation block (its 16 bytes, as SP 800-38D
10# reads them).
11def R(z: I.Block) -> Word(128n):
12  G.block(I.unpack(z))
13
14# The U32 the implementation reads for a coefficient c.
15def bit(c: Bool) -> U32:
16  U32{WCon{c, Word.zero(31n)}}
17
18# Algorithm 1 continued from an implementation accumulator (Z, V) over the
19# coefficients cs.
20def F(acc: I.Acc, cs: List<&2, Bool>) -> Word(128n):
21  match acc:
22    case I.Acc{z, v}:
23      GF.sa(128n, G.low(), cs, R(z), R(v))
24
25# The implementation's steps over a list of coefficients.
26def steps(cs: List<&2, Bool>, acc: I.Acc) -> I.Acc:
27  match cs:
28    case Nil{}:
29      acc
30    case c <> r:
31      steps(r, I.step(bit(c), acc))