spec/crypto/aes/gcm.bend

bend-collections-laws-crypto@1.0.0.0 · 183 lines · 30 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as P
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as AES
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend as Eq
6
7# Executable specification of GCM (NIST SP 800-38D) over AES (FIPS 197),
8# for 96-bit IVs and 128-bit tags. Bit strings are byte strings (U32 values
9# below 256); a block is 16 bytes.
10
11# ---- bits (section 6.1) ----
12
13# The bits of a byte, the most significant (leftmost) first.
14def byte_bits(x: U32) -> List<&2, Bool>:
15  match x:
16    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, rest}}}}}}}}}:
17      [b7, b6, b5, b4, b3, b2, b1, b0]
18
19def string_bits(xs: List<&2, U32>) -> List<&2, Bool>:
20  match xs:
21    case Nil{}:
22      Nil{}
23    case x <> rest:
24      List.append(&2, Bool, byte_bits(x), string_bits(rest))
25
26# The byte whose bits, leftmost first, are the next eight of a bit string.
27def bits_bytes(bs: List<&2, Bool>) -> List<&2, U32>:
28  match bs:
29    case b7 <> b6 <> b5 <> b4 <> b3 <> b2 <> b1 <> b0 <> rest:
30      U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, Word.zero(24n)}}}}}}}}} <> bits_bytes(rest)
31    case _:
32      Nil{}
33
34# The first n bits of a bit string, zero-filled.
35def word_of(n: Nat, bs: List<&2, Bool>) -> Word(n):
36  match n bs:
37    case 0n _:
38      WNil{}
39    case 1n+p Nil{}:
40      WCon{False{}, word_of(p, Nil{})}
41    case 1n+p b <> rest:
42      WCon{b, word_of(p, rest)}
43
44# ---- GF(2^128) (section 6.3) ----
45
46# Bit i of a block (bit 0 the leftmost) is the coefficient of x^i, and
47# f(x) = 1 + x + x^2 + x^7 + x^128: x^128 = 1 + x + x^2 + x^7 (R = 11100001 || 0^120).
48def block(xs: List<&2, U32>) -> Word(128n):
49  word_of(128n, string_bits(xs))
50
51def block_bytes(w: Word(128n)) -> List<&2, U32>:
52  bits_bytes(P.coefficients(128n, w))
53
54def low() -> Word(128n):
55  WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, Word.zero(120n)}}}}}}}}
56
57# X * Y: the polynomial product reduced modulo f.
58def mul(x: Word(128n), y: Word(128n)) -> Word(128n):
59  P.reduce(128n, low(), P.mul(P.coefficients(128n, x), P.coefficients(128n, y)))
60
61# ---- GHASH (section 6.4, Algorithm 2): Y_i = (Y_(i-1) xor X_i) * H ----
62
63def ghash(+h: Word(128n), x: List<&2, U32>, y: Word(128n)) -> Word(128n):
64  match x:
65    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> b12 <> b13 <> b14 <> b15 <> rest:
66      ghash(h, rest, mul(Word.xor(128n, y, block([b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15])), h))
67    case _:
68      y
69
70# ---- GCTR (section 6.5) ----
71
72# inc_32: the rightmost 32 bits, as an integer, plus one modulo 2^32.
73def int32(+a: U32, +b: U32, +c: U32, +d: U32) -> U32:
74  U32{word_of(32n, List.reverse(&2, Bool, string_bits([a, b, c, d])))}
75
76def str32(w: U32) -> List<&2, U32>:
77  match w:
78    case U32{bits}:
79      bits_bytes(List.reverse(&2, Bool, P.coefficients(32n, bits)))
80
81def inc32(x: List<&2, U32>) -> List<&2, U32>:
82  match x:
83    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> c0 <> c1 <> c2 <> c3 <> rest:
84      List.append(&2, U32, [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11], str32(U32.inc(int32(c0, c1, c2, c3))))
85    case _:
86      Nil{}
87
88# CIPH_K on a 16-byte block.
89def ciph(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +x: List<&2, U32>) -> List<&2, U32>:
90  AES.bytes_of(AES.encrypt(nk, nr, key, AES.state_of(x)))
91
92# X xor K over the length of X (MSB_len(X) of K when X is the shorter).
93def xor_bytes(x: List<&2, U32>, k: List<&2, U32>) -> List<&2, U32>:
94  match x k:
95    case a <> xs b <> ks:
96      U32.xor(a, b) <> xor_bytes(xs, ks)
97    case _ _:
98      Nil{}
99
100def gctr(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +x: List<&2, U32>, +cb: List<&2, U32>) -> List<&2, U32>:
101  match x:
102    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> b12 <> b13 <> b14 <> b15 <> rest:
103      List.append(&2, U32, xor_bytes([b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15], ciph(nk, nr, key, cb)),
104        gctr(nk, nr, key, rest, inc32(cb)))
105    case _:
106      xor_bytes(x, ciph(nk, nr, key, cb))
107
108# ---- GCM (section 7) ----
109
110def zeros(n: Nat) -> List<&2, U32>:
111  List.replicate(U32, n, 0)
112
113# X || 0^v, v = 128*ceil(len(X)/128) - len(X): zero bytes complete the last
114# 16-byte block.
115def pad(+x: List<&2, U32>) -> List<&2, U32>:
116  match x:
117    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> b12 <> b13 <> b14 <> b15 <> rest:
118      b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> b12 <> b13 <> b14 <> b15 <> pad(rest)
119    case Nil{}:
120      Nil{}
121    case _:
122      List.append(&2, U32, x, zeros(Nat.sub(16n, List.length(&2, U32, x))))
123
124# [n]_(8*width), most significant byte first.
125def octets(width: Nat, +n: Nat) -> List<&2, U32>:
126  match width:
127    case 0n:
128      Nil{}
129    case 1n+p:
130      List.append(&2, U32, octets(p, Nat.div(n, 256n)), [U32.from_nat(Nat.mod(n, 256n))])
131
132# [len(X)]_64: the bit length of X.
133def len64(+xs: List<&2, U32>) -> List<&2, U32>:
134  octets(8n, Nat.mul(8n, List.length(&2, U32, xs)))
135
136# Algorithm 4, J0 = IV || 0^31 || 1 for a 96-bit IV.
137def hash_key(+nk: Nat, +nr: Nat, +key: List<&2, U32>) -> Word(128n):
138  block(ciph(nk, nr, key, zeros(16n)))
139
140def j0(+iv: List<&2, U32>) -> List<&2, U32>:
141  List.append(&2, U32, iv, [0, 0, 0, 1])
142
143def tag(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, +c: List<&2, U32>) -> List<&2, U32>:
144  gctr(nk, nr, key, block_bytes(ghash(hash_key(nk, nr, key),
145    List.append(&2, U32, pad(aad), List.append(&2, U32, pad(c), List.append(&2, U32, len64(aad), len64(c)))), Word.zero(128n))), j0(iv))
146
147# GCM-AE_K(IV, P, A) = (C, T), returned as C || T.
148def seal(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, pt: List<&2, U32>) -> List<&2, U32>:
149  +c = gctr(nk, nr, key, pt, inc32(j0(iv)))
150  List.append(&2, U32, c, tag(nk, nr, key, iv, aad, c))
151
152def accept(ok: Bool, p: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
153  match ok:
154    case True{}:
155      Some{p}
156    case False{}:
157      None{}
158
159def open_checked(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, +c: List<&2, U32>, t: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
160  accept(Eq.equal(t, tag(nk, nr, key, iv, aad, c)), gctr(nk, nr, key, c, inc32(j0(iv))))
161
162# GCM-AD_K(IV, C, A, T), the input being C || T: FAIL (None) unless T is
163# the tag of C.
164def open_split(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, +input: List<&2, U32>, +n: Nat, short: Bool) -> Maybe<&2, List<&2, U32>>:
165  match short:
166    case True{}:
167      None{}
168    case False{}:
169      open_checked(nk, nr, key, iv, aad, List.take(&2, U32, input, Nat.sub(n, 16n)), List.drop(&2, U32, input, Nat.sub(n, 16n)))
170
171def open(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, +input: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
172  +n = List.length(&2, U32, input)
173  open_split(nk, nr, key, iv, aad, input, n, Nat.is_lt(n, 16n))
174
175# GCM over AES with the key's own Nk and Nr (FIPS 197 Figure 4).
176def aes_seal(+key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, pt: List<&2, U32>) -> List<&2, U32>:
177  seal(AES.nk(key), AES.nr(key), key, iv, aad, pt)
178
179def aes_open(+key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, +input: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
180  open(AES.nk(key), AES.nr(key), key, iv, aad, input)
181
182def aes_tag(+key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, +c: List<&2, U32>) -> List<&2, U32>:
183  tag(AES.nk(key), AES.nr(key), key, iv, aad, c)