1	import Base
2	import ../../../src/crypto/aes/types.bend as T
3	import ./poly.bend as P
4	import ./aes.bend as AES
5	import ../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.
14	def 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	
19	def 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.
27	def 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.
35	def 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).
48	def block(xs: List<&2, U32>) -> Word(128n):
49	  word_of(128n, string_bits(xs))
50	
51	def block_bytes(w: Word(128n)) -> List<&2, U32>:
52	  bits_bytes(P.coefficients(128n, w))
53	
54	def 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.
58	def 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	
63	def 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.
73	def 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	
76	def 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	
81	def 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.
89	def 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).
93	def 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	
100	def 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	
110	def 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.
115	def 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.
125	def 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.
133	def 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.
137	def hash_key(+nk: Nat, +nr: Nat, +key: List<&2, U32>) -> Word(128n):
138	  block(ciph(nk, nr, key, zeros(16n)))
139	
140	def j0(+iv: List<&2, U32>) -> List<&2, U32>:
141	  List.append(&2, U32, iv, [0, 0, 0, 1])
142	
143	def 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.
148	def 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	
152	def 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	
159	def 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.
164	def 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	
171	def 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).
176	def 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	
179	def 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	
182	def 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)