1	# Modes of operation over any block cipher of any block size (the
2	# block-cipher interface, block.bend): ECB and CBC (NIST SP 800-38A, 6.1 and
3	# 6.2) on lists of blocks and on bytes, and CTR (SP 800-38A, 6.5) as a stream
4	# cipher.
5	#
6	# cipher-modes keeps its own modes for 128-bit ciphers (CBC, XTS, CCM, CMAC);
7	# these are the ones every block size shares, so a 64-bit cipher (DES, 3DES)
8	# and a 128-bit one run through the same code.
9	#
10	# Every loop over blocks or bytes is a tail call (the structural forms the
11	# proofs use are proved equal to them in PROOF.bend).
12	import Base
13	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
14	import ./crypto.bend as Cr
15	import ./stream.bend as St
16	
17	# Lists of blocks
18	
19	def cr.blks.rev_onto(~Blk: Data, bs: List<&2, Blk>, acc: List<&2, Blk>) -> List<&2, Blk>:
20	  match bs:
21	    case Nil{}:
22	      acc
23	    case Con{b, t}:
24	      cr.blks.rev_onto(~Blk, t, Con{b, acc})
25	
26	# ECB: each block on its own (structural, and the loop that runs)
27	
28	def cr.ecb(~K: Data, ~Blk: Data, ~f: K -> Blk -> Blk, +k: K, bs: List<&2, Blk>) -> List<&2, Blk>:
29	  match bs:
30	    case Nil{}:
31	      Nil{}
32	    case Con{b, t}:
33	      Con{f(k, b), cr.ecb(~K, ~Blk, ~f, k, t)}
34	
35	def cr.ecb.go(~K: Data, ~Blk: Data, ~f: K -> Blk -> Blk, +k: K, bs: List<&2, Blk>, acc: List<&2, Blk>) -> List<&2, Blk>:
36	  match bs:
37	    case Nil{}:
38	      cr.blks.rev_onto(~Blk, acc, Nil{})
39	    case Con{b, t}:
40	      cr.ecb.go(~K, ~Blk, ~f, k, t, Con{f(k, b), acc})
41	
42	def CrEcb.encrypt_blocks(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, +k: K, bs: List<&2, Blk>) -> List<&2, Blk>:
43	  cr.ecb.go(~K, ~Blk, ~enc, k, bs, Nil{})
44	
45	def CrEcb.decrypt_blocks(~K: Data, ~Blk: Data, ~dec: K -> Blk -> Blk, +k: K, bs: List<&2, Blk>) -> List<&2, Blk>:
46	  cr.ecb.go(~K, ~Blk, ~dec, k, bs, Nil{})
47	
48	# CBC: C_i = E(P_i xor C_{i-1}), C_0 the IV (structural, and the loops)
49	
50	def cr.cbc.enc(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, bs: List<&2, Blk>, iv: Blk) -> List<&2, Blk>:
51	  match bs:
52	    case Nil{}:
53	      Nil{}
54	    case Con{p, t}:
55	      +c = enc(k, bxor(p, iv))
56	      Con{c, cr.cbc.enc(~K, ~Blk, ~enc, ~bxor, k, t, c)}
57	
58	def cr.cbc.dec(~K: Data, ~Blk: Data, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, bs: List<&2, Blk>, iv: Blk) -> List<&2, Blk>:
59	  match bs:
60	    case Nil{}:
61	      Nil{}
62	    case Con{+c, t}:
63	      Con{bxor(dec(k, c), iv), cr.cbc.dec(~K, ~Blk, ~dec, ~bxor, k, t, c)}
64	
65	def cr.cbc.enc.go(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, bs: List<&2, Blk>, iv: Blk, acc: List<&2, Blk>) -> List<&2, Blk>:
66	  match bs:
67	    case Nil{}:
68	      cr.blks.rev_onto(~Blk, acc, Nil{})
69	    case Con{p, t}:
70	      +c = enc(k, bxor(p, iv))
71	      cr.cbc.enc.go(~K, ~Blk, ~enc, ~bxor, k, t, c, Con{c, acc})
72	
73	def cr.cbc.dec.go(~K: Data, ~Blk: Data, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, bs: List<&2, Blk>, iv: Blk, acc: List<&2, Blk>) -> List<&2, Blk>:
74	  match bs:
75	    case Nil{}:
76	      cr.blks.rev_onto(~Blk, acc, Nil{})
77	    case Con{+c, t}:
78	      cr.cbc.dec.go(~K, ~Blk, ~dec, ~bxor, k, t, c, Con{bxor(dec(k, c), iv), acc})
79	
80	# CBC on blocks: the last ciphertext block of one call is the IV of the next,
81	# so a message may arrive a block at a time
82	def CrCbc.encrypt_blocks(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, iv: Blk, bs: List<&2, Blk>) -> List<&2, Blk>:
83	  cr.cbc.enc.go(~K, ~Blk, ~enc, ~bxor, k, bs, iv, Nil{})
84	
85	def CrCbc.decrypt_blocks(~K: Data, ~Blk: Data, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, +k: K, iv: Blk, bs: List<&2, Blk>) -> List<&2, Blk>:
86	  cr.cbc.dec.go(~K, ~Blk, ~dec, ~bxor, k, bs, iv, Nil{})
87	
88	# Bytes as blocks
89	
90	def cr.pick_n(full: Bool, +n: Nat) -> Nat:
91	  match full:
92	    case True{}:
93	      0n
94	    case False{}:
95	      n
96	
97	def cr.pick_cur(full: Bool, +c: List<&2, U32>) -> List<&2, U32>:
98	  match full:
99	    case True{}:
100	      Nil{}
101	    case False{}:
102	      c
103	
104	def cr.pick_acc(full: Bool, +c: List<&2, U32>, acc: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
105	  match full:
106	    case True{}:
107	      Con{St.cr.rev_onto(c, Nil{}), acc}
108	    case False{}:
109	      acc
110	
111	# the whole n-byte pieces of xs, last first (cur: the piece being filled,
112	# reversed, i bytes long)
113	def cr.chunks(xs: List<&2, U32>, +n: Nat, +i: Nat, +cur: List<&2, U32>, acc: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
114	  match xs:
115	    case Nil{}:
116	      acc
117	    case Con{x, t}:
118	      +c : List<&2, U32> = Con{x, cur}
119	      +full = Nat.is_eq(1n+i, n)
120	      cr.chunks(t, n, cr.pick_n(full, 1n+i), cr.pick_cur(full, c), cr.pick_acc(full, c, acc))
121	
122	# a block onto a list of blocks, None if either is missing
123	def cr.cons_m(~Blk: Data, m: Maybe<&2, Blk>, acc: Maybe<&2, List<&2, Blk>>) -> Maybe<&2, List<&2, Blk>>:
124	  match m acc:
125	    case Some{b} Some{l}:
126	      Some{Con{b, l}}
127	    case _ _:
128	      None{}
129	
130	# the pieces (last first) as blocks, in order, onto acc
131	def cr.blocks_of.go(~Blk: Data, ~blk_of: B.Octets -> Maybe<&2, Blk>, ps: List<&2, List<&2, U32>>, acc: Maybe<&2, List<&2, Blk>>) -> Maybe<&2, List<&2, Blk>>:
132	  match ps:
133	    case Nil{}:
134	      acc
135	    case Con{p, t}:
136	      cr.blocks_of.go(~Blk, ~blk_of, t, cr.cons_m(~Blk, blk_of(B.Octets.of_list(p)), acc))
137	
138	def cr.divides(pos: Bool, +len: Nat, +n: Nat) -> Bool:
139	  match pos:
140	    case True{}:
141	      Nat.is_eq(Nat.mod(len, n), 0n)
142	    case False{}:
143	      False{}
144	
145	def cr.blocks_of.some(~Blk: Data, m: Maybe<&2, List<&2, Blk>>, +len: Nat) -> Result<&2, &2, Cr.CrError, List<&2, Blk>>:
146	  match m:
147	    case None{}:
148	      Fail{Cr.CrBadBlockSize{len}}
149	    case Some{bs}:
150	      Done{bs}
151	
152	def cr.blocks_of.ok(~Blk: Data, ok: Bool, m: Maybe<&2, List<&2, Blk>>, +len: Nat) -> Result<&2, &2, Cr.CrError, List<&2, Blk>>:
153	  match ok:
154	    case False{}:
155	      Fail{Cr.CrNotBlockMultiple{len}}
156	    case True{}:
157	      cr.blocks_of.some(~Blk, m, len)
158	
159	# A byte string of whole blocks as its blocks (CrNotBlockMultiple otherwise)
160	def CrModes.blocks_of(~Blk: Data, ~bsize: Nat, ~blk_of: B.Octets -> Maybe<&2, Blk>, o: B.Octets) -> Result<&2, &2, Cr.CrError, List<&2, Blk>>:
161	  +xs = B.Octets.to_list(o)
162	  +len = B.len.fast(xs)
163	  cr.blocks_of.ok(~Blk, cr.divides(Nat.is_lt(0n, bsize), len, bsize), cr.blocks_of.go(~Blk, ~blk_of, cr.chunks(xs, bsize, 0n, Nil{}, Nil{}), Some{Nil{}}), len)
164	
165	def cr.octets_of.go(~Blk: Data, ~blk_to: Blk -> B.Octets, bs: List<&2, Blk>, acc: List<&2, B.Octets>) -> List<&2, B.Octets>:
166	  match bs:
167	    case Nil{}:
168	      acc
169	    case Con{b, t}:
170	      cr.octets_of.go(~Blk, ~blk_to, t, Con{blk_to(b), acc})
171	
172	# The bytes of a list of blocks
173	def CrModes.octets_of(~Blk: Data, ~blk_to: Blk -> B.Octets, bs: List<&2, Blk>) -> B.Octets:
174	  B.Octets.concat(cr.blks.rev_onto(~B.Octets, cr.octets_of.go(~Blk, ~blk_to, bs, Nil{}), Nil{}))
175	
176	def cr.iv.pick(~Blk: Data, m: Maybe<&2, Blk>, +n: Nat) -> Result<&2, &2, Cr.CrError, Blk>:
177	  match m:
178	    case None{}:
179	      Fail{Cr.CrBadIvLength{n}}
180	    case Some{b}:
181	      Done{b}
182	
183	# an IV of one block (CrBadIvLength otherwise)
184	def cr.iv(~Blk: Data, ~blk_of: B.Octets -> Maybe<&2, Blk>, +iv: B.Octets) -> Result<&2, &2, Cr.CrError, Blk>:
185	  cr.iv.pick(~Blk, blk_of(iv), B.Octets.len(iv))
186	
187	# ECB and CBC on bytes: a message of whole blocks (no padding)
188	
189	def CrEcb.encrypt(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
190	  Result.map(&2, &2, Cr.CrError, List<&2, Blk>, B.Octets, bs => CrModes.octets_of(~Blk, ~blk_to, CrEcb.encrypt_blocks(~K, ~Blk, ~enc, k, bs)), CrModes.blocks_of(~Blk, ~bsize, ~blk_of, m))
191	
192	def CrEcb.decrypt(~K: Data, ~Blk: Data, ~bsize: Nat, ~dec: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
193	  Result.map(&2, &2, Cr.CrError, List<&2, Blk>, B.Octets, bs => CrModes.octets_of(~Blk, ~blk_to, CrEcb.decrypt_blocks(~K, ~Blk, ~dec, k, bs)), CrModes.blocks_of(~Blk, ~bsize, ~blk_of, c))
194	
195	def CrCbc.encrypt(~K: Data, ~Blk: Data, ~bsize: Nat, ~enc: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, iv: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
196	  do Result<&2, &2, Cr.CrError, B.Octets>:
197	    v : Blk <- cr.iv(~Blk, ~blk_of, iv)
198	    bs : List<&2, Blk> <- CrModes.blocks_of(~Blk, ~bsize, ~blk_of, m)
199	    return CrModes.octets_of(~Blk, ~blk_to, CrCbc.encrypt_blocks(~K, ~Blk, ~enc, ~bxor, k, v, bs))
200	
201	def CrCbc.decrypt(~K: Data, ~Blk: Data, ~bsize: Nat, ~dec: K -> Blk -> Blk, ~bxor: Blk -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, +k: K, iv: B.Octets, c: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
202	  do Result<&2, &2, Cr.CrError, B.Octets>:
203	    v : Blk <- cr.iv(~Blk, ~blk_of, iv)
204	    bs : List<&2, Blk> <- CrModes.blocks_of(~Blk, ~bsize, ~blk_of, c)
205	    return CrModes.octets_of(~Blk, ~blk_to, CrCbc.decrypt_blocks(~K, ~Blk, ~dec, ~bxor, k, v, bs))
206	
207	# CTR (SP 800-38A, 6.5): the keystream is E(T_1) E(T_2) ..., T_1 the IV and
208	# T_{i+1} = T_i + 1 (the whole block as a big-endian number, mod 2^(8 bsize):
209	# Appendix B.1's standard incrementing function). It is a keystream
210	# generator, so St.CrXor makes it a stream cipher, with the stream-cipher
211	# laws proved for every block cipher (LAWS.bend: ctr_*).
212	
213	# the state: the key schedule, the next counter block (its bytes), and the
214	# keystream bytes left over from the last block
215	type CrCtrState<-K: Data> is Data:
216	  CrCtrState{key: K, ctr: List<&2, U32>, buf: List<&2, U32>}
217	
218	def cr.ctr.sum(carry: Bool, +b: U32) -> U32:
219	  match carry:
220	    case True{}:
221	      B.byte(U32.add(b, 1))
222	    case False{}:
223	      b
224	
225	def cr.ctr.carry(carry: Bool, +b: U32) -> Bool:
226	  match carry:
227	    case True{}:
228	      U32.is_eq(b, 255)
229	    case False{}:
230	      False{}
231	
232	# one added to a number given by its bytes, least significant first (rs),
233	# the result most significant first, onto acc
234	def cr.ctr.add1(rs: List<&2, U32>, +carry: Bool, acc: List<&2, U32>) -> List<&2, U32>:
235	  match rs:
236	    case Nil{}:
237	      acc
238	    case Con{+b, t}:
239	      cr.ctr.add1(t, cr.ctr.carry(carry, b), Con{cr.ctr.sum(carry, b), acc})
240	
241	# the next counter block
242	def cr.ctr.inc(xs: List<&2, U32>) -> List<&2, U32>:
243	  cr.ctr.add1(St.cr.rev_onto(xs, Nil{}), True{}, Nil{})
244	
245	def cr.ctr.block(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~blk_to: Blk -> B.Octets, m: Maybe<&2, Blk>, +k: K) -> List<&2, U32>:
246	  match m:
247	    case None{}:
248	      Nil{}
249	    case Some{b}:
250	      B.Octets.to_list(blk_to(enc(k, b)))
251	
252	def cr.head(xs: List<&2, U32>) -> U32:
253	  match xs:
254	    case Nil{}:
255	      0
256	    case Con{h, t}:
257	      h
258	
259	def cr.tail(xs: List<&2, U32>) -> List<&2, U32>:
260	  match xs:
261	    case Nil{}:
262	      Nil{}
263	    case Con{h, t}:
264	      t
265	
266	def cr.ctr.next(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, buf: List<&2, U32>, +k: K, +ctr: List<&2, U32>) -> St.CrKsStep<CrCtrState<K>>:
267	  match buf:
268	    case Con{b, t}:
269	      St.CrKsStep{b, CrCtrState{k, ctr, t}}
270	    case Nil{}:
271	      +ks = cr.ctr.block(~K, ~Blk, ~enc, ~blk_to, blk_of(B.Octets.of_list(ctr)), k)
272	      St.CrKsStep{cr.head(ks), CrCtrState{k, cr.ctr.inc(ctr), cr.tail(ks)}}
273	
274	# The keystream generator: the next keystream byte and the state after it
275	def CrCtr.next(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, s: CrCtrState<K>) -> St.CrKsStep<CrCtrState<K>>:
276	  match s:
277	    case CrCtrState{+k, +ctr, buf}:
278	      cr.ctr.next(~K, ~Blk, ~enc, ~blk_of, ~blk_to, buf, k, ctr)
279	
280	def cr.ctr.start(~K: Data, ~bsize: Nat, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, key_o: B.Octets, +iv: List<&2, U32>) -> Result<&2, &2, Cr.CrError, CrCtrState<K>>:
281	  +n = B.len(iv)
282	  do Result<&2, &2, Cr.CrError, CrCtrState<K>>:
283	    Cr.CrError.check(Nat.is_eq(n, bsize), Cr.CrBadIvLength{n})
284	    k : K <- key(key_o)
285	    return CrCtrState{k, iv, Nil{}}
286	
287	# The state for a raw key and an initial counter block of bsize bytes
288	# (CrBadIvLength for another length)
289	def CrCtr.start(~K: Data, ~bsize: Nat, ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>, key_o: B.Octets, iv: B.Octets) -> Result<&2, &2, Cr.CrError, CrCtrState<K>>:
290	  cr.ctr.start(~K, ~bsize, ~key, key_o, B.Octets.to_list(iv))
291	
292	# The next piece of data, encrypted or decrypted, and the state after it
293	def CrCtr.update(~K: Data, ~Blk: Data, ~enc: K -> Blk -> Blk, ~blk_of: B.Octets -> Maybe<&2, Blk>, ~blk_to: Blk -> B.Octets, s: CrCtrState<K>, m: B.Octets) -> St.CrXorOut<CrCtrState<K>>:
294	  St.CrXor.update(~CrCtrState<K>, ~CrCtr.next(~K, ~Blk, ~enc, ~blk_of, ~blk_to), s, m)