1	# CCM, counter with CBC-MAC (NIST SP 800-38C; RFC 3610), authenticated
2	# encryption over any 128-bit block cipher (only its encryption is used; see
3	# cipher-modes.bend for the template arguments).
4	#
5	# Parameters: the tag length M (4, 6, 8, 10, 12, 14 or 16 bytes) and the nonce
6	# length N (7 to 13 bytes), which fixes the length field L = 15 - N. The
7	# message must be shorter than 2^(8L) bytes.
8	#   B_0 = flags || nonce || l(m)    flags = 64*Adata + 8*((M-2)/2) + (L-1)
9	#   then l(a) encoded and a (if a is not empty), zero-padded to a block, and m,
10	#   zero-padded: their CBC-MAC (IV 0) is the tag T (its first M bytes).
11	#   A_i = (L-1) || nonce || i,  S_i = E(A_i):
12	#   ciphertext = m xor S_1 S_2 ..., then T xor the first M bytes of S_0.
13	# CCM needs the message length before it starts (it is in B_0), so it has no
14	# streaming interface.
15	import Base
16	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
17	import ./cipher_modes.bend as M
18	
19	# the low n bytes of v, most significant first (zeros above the 32 bits of v)
20	def ccm.be(n: Nat, +v: U32) -> List<&2, U32>:
21	  B.drop(Nat.sub(8n, n), B.append(B.zeros(4n), M.cm.unword(v, Nil{})))
22	
23	# xs zero-padded to a whole number of blocks
24	def ccm.pad(+xs: List<&2, U32>) -> List<&2, U32>:
25	  B.append(xs, B.zeros(Nat.mod(Nat.sub(16n, Nat.mod(B.len(xs), 16n)), 16n)))
26	
27	# l(a): two bytes below 65280 (2^16 - 2^8), else 0xFF 0xFE and four bytes
28	def ccm.alen.pick(short: Bool, +v: U32) -> List<&2, U32>:
29	  match short:
30	    case True{}:
31	      ccm.be(2n, v)
32	    case False{}:
33	      Con{255, Con{254, ccm.be(4n, v)}}
34	
35	def ccm.aad.pick(empty: Bool, +a: List<&2, U32>) -> List<&2, U32>:
36	  match empty:
37	    case True{}:
38	      Nil{}
39	    case False{}:
40	      +v = U32.from_nat(B.len(a))
41	      ccm.pad(B.append(ccm.alen.pick(U32.is_lt(v, 65280), v), a))
42	
43	# CBC-MAC of whole blocks, from x
44	def ccm.cbcmac(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, x: M.CmBlock) -> M.CmBlock:
45	  match bs:
46	    case Nil{}:
47	      x
48	    case Con{b, t}:
49	      ccm.cbcmac(~K, ~enc, k, t, enc(k, M.CmBlock.xor(x, b)))
50	
51	# the CBC-MAC of B_0, the encoded a and the padded p
52	def ccm.mac(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +l: Nat, +nonce: List<&2, U32>, +a: List<&2, U32>, +p: List<&2, U32>) -> M.CmBlock:
53	  +adata = B.len(a)
54	  +flags = U32.from_nat(Nat.add(Nat.add(Nat.mul(64n, Nat.min(adata, 1n)), Nat.mul(8n, Nat.div(Nat.sub(m, 2n), 2n))), Nat.sub(l, 1n)))
55	  +input = B.append(Con{flags, B.append(nonce, ccm.be(l, U32.from_nat(B.len(p))))}, B.append(ccm.aad.pick(Nat.is_eq(adata, 0n), a), ccm.pad(p)))
56	  ccm.cbcmac(~K, ~enc, k, M.cm.split.blocks(M.cm.split(input)), M.CmBlock.zero())
57	
58	# the tag: the first m bytes of the MAC
59	def ccm.tag(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +l: Nat, +nonce: List<&2, U32>, +a: List<&2, U32>, +p: List<&2, U32>) -> List<&2, U32>:
60	  B.take(m, M.cm.bytes_of(ccm.mac(~K, ~enc, k, m, l, nonce, a, p)))
61	
62	# A_i = A_0 with counter i (i < 2^(8L), so it stays in the counter field)
63	def ccm.ai(a0: M.CmBlock, i: U32) -> M.CmBlock:
64	  M.CmBlock.xor(a0, M.CmBlock{0, 0, 0, i})
65	
66	# CTR on whole blocks: b_j xor S_(i+j)
67	def ccm.ctrb(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +a0: M.CmBlock, +i: U32) -> List<&2, M.CmBlock>:
68	  match bs:
69	    case Nil{}:
70	      Nil{}
71	    case Con{b, rest}:
72	      Con{M.CmBlock.xor(b, enc(k, ccm.ai(a0, i))), ccm.ctrb(~K, ~enc, k, rest, a0, U32.add(i, 1))}
73	
74	# CTR from counter 1: the whole blocks, then the tail xor the next S_i
75	def ccm.xcrypt(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +a0: M.CmBlock, s: M.CmSplit) -> List<&2, U32>:
76	  match s:
77	    case M.CmSplit{+bs, tail}:
78	      M.cm.join_onto(ccm.ctrb(~K, ~enc, k, bs, a0, 1), M.cm.xor_bytes(tail, M.cm.bytes_of(enc(k, ccm.ai(a0, U32.add(1, U32.from_nat(List.length(&2, M.CmBlock, bs))))))))
79	
80	# A_0: (L-1) || nonce || zeros
81	def ccm.a0(+l: Nat, +nonce: List<&2, U32>) -> M.CmBlock:
82	  M.cm.block_of(Con{U32.from_nat(Nat.sub(l, 1n)), B.append(nonce, B.zeros(l))})
83	
84	def ccm.tag_ok(+m: Nat) -> Bool:
85	  Bool.and(Nat.is_le(4n, m), Bool.and(Nat.is_le(m, 16n), Nat.is_eq(Nat.mod(m, 2n), 0n)))
86	
87	# the message must be shorter than 2^(8L) bytes: a bound only for L = 2 or 3
88	# (with L >= 4 every list is shorter)
89	def ccm.len_ok.three(three: Bool, +n: Nat) -> Bool:
90	  match three:
91	    case True{}:
92	      U32.is_lt(U32.from_nat(n), 16777216)
93	    case False{}:
94	      True{}
95	
96	def ccm.len_ok.two(two: Bool, +l: Nat, +n: Nat) -> Bool:
97	  match two:
98	    case True{}:
99	      U32.is_lt(U32.from_nat(n), 65536)
100	    case False{}:
101	      ccm.len_ok.three(Nat.is_eq(l, 3n), n)
102	
103	def ccm.len_ok(+l: Nat, +n: Nat) -> Bool:
104	  ccm.len_ok.two(Nat.is_eq(l, 2n), l, n)
105	
106	def ccm.checks.len(ok: Bool, +n: Nat) -> Result<&2, &2, M.CmError, Unit>:
107	  match ok:
108	    case True{}:
109	      Done{Unit{}}
110	    case False{}:
111	      Fail{M.CmTooLong{n}}
112	
113	def ccm.checks.nonce(ok: Bool, +nl: Nat, +n: Nat) -> Result<&2, &2, M.CmError, Unit>:
114	  match ok:
115	    case True{}:
116	      ccm.checks.len(ccm.len_ok(Nat.sub(15n, nl), n), n)
117	    case False{}:
118	      Fail{M.CmBadNonceLength{nl}}
119	
120	def ccm.checks.tag(ok: Bool, +m: Nat, +nl: Nat, +n: Nat) -> Result<&2, &2, M.CmError, Unit>:
121	  match ok:
122	    case True{}:
123	      ccm.checks.nonce(Bool.and(Nat.is_le(7n, nl), Nat.is_le(nl, 13n)), nl, n)
124	    case False{}:
125	      Fail{M.CmBadTagLength{m}}
126	
127	# the tag length, the nonce length and the message length n, in that order
128	def ccm.checks(+m: Nat, +nl: Nat, +n: Nat) -> Result<&2, &2, M.CmError, Unit>:
129	  ccm.checks.tag(ccm.tag_ok(m), m, nl, n)
130	
131	# the ciphertext of pv, then the tag
132	def ccm.ebody(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +nv: List<&2, U32>, +av: List<&2, U32>, +pv: List<&2, U32>) -> List<&2, U32>:
133	  +l = Nat.sub(15n, B.len(nv))
134	  +a0 = ccm.a0(l, nv)
135	  B.append(ccm.xcrypt(~K, ~enc, k, a0, M.cm.split(pv)), M.cm.xor_bytes(ccm.tag(~K, ~enc, k, m, l, nv, av, pv), M.cm.bytes_of(enc(k, a0))))
136	
137	def ccm.e2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +nv: List<&2, U32>, +av: List<&2, U32>, +pv: List<&2, U32>, r: Result<&2, &2, M.CmError, Unit>) -> Result<&2, &2, M.CmError, B.Octets>:
138	  match r:
139	    case Fail{e}:
140	      Fail{e}
141	    case Done{u}:
142	      Done{B.Octets.of_list(ccm.ebody(~K, ~enc, k, m, nv, av, pv))}
143	
144	def ccm.open(ok: Bool, p: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
145	  match ok:
146	    case True{}:
147	      Done{B.Octets.of_list(p)}
148	    case False{}:
149	      Fail{M.CmTagMismatch{}}
150	
151	# the plaintext, if the tag (compared with no early exit) matches
152	def ccm.dbody(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +nv: List<&2, U32>, +av: List<&2, U32>, +cv: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
153	  +body = Nat.sub(B.len(cv), m)
154	  +l = Nat.sub(15n, B.len(nv))
155	  +a0 = ccm.a0(l, nv)
156	  +pv = ccm.xcrypt(~K, ~enc, k, a0, M.cm.split(B.take(body, cv)))
157	  ccm.open(M.cm.ct_eq(M.cm.xor_bytes(B.drop(body, cv), M.cm.bytes_of(enc(k, a0))), ccm.tag(~K, ~enc, k, m, l, nv, av, pv)), pv)
158	
159	def ccm.d3(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +nv: List<&2, U32>, +av: List<&2, U32>, +cv: List<&2, U32>, r: Result<&2, &2, M.CmError, Unit>) -> Result<&2, &2, M.CmError, B.Octets>:
160	  match r:
161	    case Fail{e}:
162	      Fail{e}
163	    case Done{u}:
164	      ccm.dbody(~K, ~enc, k, m, nv, av, cv)
165	
166	def ccm.d2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ok: Bool, +k: K, +m: Nat, +nv: List<&2, U32>, +av: List<&2, U32>, +cv: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
167	  match ok:
168	    case False{}:
169	      Fail{M.CmTooShort{B.len(cv)}}
170	    case True{}:
171	      ccm.d3(~K, ~enc, k, m, nv, av, cv, ccm.checks(m, B.len(nv), Nat.sub(B.len(cv), m)))
172	
173	# The same, tail-recursive. Bend 2.0.37's runtime overflows its stack at some
174	# tens of thousands of nested non-tail calls, so the structural forms above,
175	# which the proofs reason about, cannot run on long messages; Ccm.encrypt and
176	# Ccm.decrypt run these, and PROOF.bend proves each equal to its structural
177	# form for every input (ccmp is the structural layer's proof).
178	
179	def ccm.pad.fast(+xs: List<&2, U32>) -> List<&2, U32>:
180	  B.append.fast(xs, B.zeros(Nat.mod(Nat.sub(16n, Nat.mod(B.len.fast(xs), 16n)), 16n)))
181	
182	def ccm.aad.pick.fast(empty: Bool, +a: List<&2, U32>) -> List<&2, U32>:
183	  match empty:
184	    case True{}:
185	      Nil{}
186	    case False{}:
187	      +v = U32.from_nat(B.len.fast(a))
188	      ccm.pad.fast(B.append(ccm.alen.pick(U32.is_lt(v, 65280), v), a))
189	
190	def ccm.mac.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +l: Nat, +nonce: List<&2, U32>, +a: List<&2, U32>, +p: List<&2, U32>) -> M.CmBlock:
191	  +adata = B.len.fast(a)
192	  +flags = U32.from_nat(Nat.add(Nat.add(Nat.mul(64n, Nat.min(adata, 1n)), Nat.mul(8n, Nat.div(Nat.sub(m, 2n), 2n))), Nat.sub(l, 1n)))
193	  +input = B.append(Con{flags, B.append(nonce, ccm.be(l, U32.from_nat(B.len.fast(p))))}, B.append.fast(ccm.aad.pick.fast(Nat.is_eq(adata, 0n), a), ccm.pad.fast(p)))
194	  ccm.cbcmac(~K, ~enc, k, M.cm.split.blocks(M.cm.split.fast(input)), M.CmBlock.zero())
195	
196	def ccm.tag.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +l: Nat, +nonce: List<&2, U32>, +a: List<&2, U32>, +p: List<&2, U32>) -> List<&2, U32>:
197	  B.take(m, M.cm.bytes_of(ccm.mac.fast(~K, ~enc, k, m, l, nonce, a, p)))
198	
199	# the blocks so far kept reversed in acc
200	def ccm.ctrb.go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +a0: M.CmBlock, +i: U32, acc: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
201	  match bs:
202	    case Nil{}:
203	      M.cm.blocks.rev_onto(acc, Nil{})
204	    case Con{b, rest}:
205	      ccm.ctrb.go(~K, ~enc, k, rest, a0, U32.add(i, 1), Con{M.CmBlock.xor(b, enc(k, ccm.ai(a0, i))), acc})
206	
207	def ccm.ctrb.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +a0: M.CmBlock, +i: U32) -> List<&2, M.CmBlock>:
208	  ccm.ctrb.go(~K, ~enc, k, bs, a0, i, Nil{})
209	
210	def ccm.xcrypt.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +a0: M.CmBlock, s: M.CmSplit) -> List<&2, U32>:
211	  match s:
212	    case M.CmSplit{+bs, tail}:
213	      M.cm.join_onto.fast(ccm.ctrb.fast(~K, ~enc, k, bs, a0, 1), M.cm.xor_bytes(tail, M.cm.bytes_of(enc(k, ccm.ai(a0, U32.add(1, U32.from_nat(M.cm.blocks.len(bs))))))))
214	
215	def ccm.ebody.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +nv: List<&2, U32>, +av: List<&2, U32>, +pv: List<&2, U32>) -> List<&2, U32>:
216	  +l = Nat.sub(15n, B.len(nv))
217	  +a0 = ccm.a0(l, nv)
218	  B.append.fast(ccm.xcrypt.fast(~K, ~enc, k, a0, M.cm.split.fast(pv)), M.cm.xor_bytes(ccm.tag.fast(~K, ~enc, k, m, l, nv, av, pv), M.cm.bytes_of(enc(k, a0))))
219	
220	def ccm.e2.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +nv: List<&2, U32>, +av: List<&2, U32>, +pv: List<&2, U32>, r: Result<&2, &2, M.CmError, Unit>) -> Result<&2, &2, M.CmError, B.Octets>:
221	  match r:
222	    case Fail{e}:
223	      Fail{e}
224	    case Done{u}:
225	      Done{B.Octets.of_list(ccm.ebody.fast(~K, ~enc, k, m, nv, av, pv))}
226	
227	def ccm.dbody.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +nv: List<&2, U32>, +av: List<&2, U32>, +cv: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
228	  +body = Nat.sub(B.len.fast(cv), m)
229	  +l = Nat.sub(15n, B.len(nv))
230	  +a0 = ccm.a0(l, nv)
231	  +pv = ccm.xcrypt.fast(~K, ~enc, k, a0, M.cm.split.fast(B.take.fast(body, cv)))
232	  ccm.open(M.cm.ct_eq(M.cm.xor_bytes(B.drop(body, cv), M.cm.bytes_of(enc(k, a0))), ccm.tag.fast(~K, ~enc, k, m, l, nv, av, pv)), pv)
233	
234	def ccm.d3.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +nv: List<&2, U32>, +av: List<&2, U32>, +cv: List<&2, U32>, r: Result<&2, &2, M.CmError, Unit>) -> Result<&2, &2, M.CmError, B.Octets>:
235	  match r:
236	    case Fail{e}:
237	      Fail{e}
238	    case Done{u}:
239	      ccm.dbody.fast(~K, ~enc, k, m, nv, av, cv)
240	
241	def ccm.d2.fast(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ok: Bool, +k: K, +m: Nat, +nv: List<&2, U32>, +av: List<&2, U32>, +cv: List<&2, U32>) -> Result<&2, &2, M.CmError, B.Octets>:
242	  match ok:
243	    case False{}:
244	      Fail{M.CmTooShort{B.len.fast(cv)}}
245	    case True{}:
246	      ccm.d3.fast(~K, ~enc, k, m, nv, av, cv, ccm.checks(m, B.len(nv), Nat.sub(B.len.fast(cv), m)))
247	
248	# Ccm.encrypt and Ccm.decrypt through the structural forms (the laws' proofs
249	# reason about these; PROOF.bend proves them equal to the public defs)
250	def Ccm.encrypt.ref(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, nonce: B.Octets, aad: B.Octets, p: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
251	  +nv = B.Octets.to_list(nonce)
252	  +pv = B.Octets.to_list(p)
253	  ccm.e2(~K, ~enc, k, m, nv, B.Octets.to_list(aad), pv, ccm.checks(m, B.len(nv), B.len(pv)))
254	
255	def Ccm.decrypt.ref(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, nonce: B.Octets, aad: B.Octets, c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
256	  +cv = B.Octets.to_list(c)
257	  ccm.d2(~K, ~enc, Nat.is_le(m, B.len(cv)), k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), cv)
258	
259	# p with associated data aad under the nonce: the ciphertext, then the m-byte tag
260	def Ccm.encrypt(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, nonce: B.Octets, aad: B.Octets, p: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
261	  +nv = B.Octets.to_list(nonce)
262	  +pv = B.Octets.to_list(p)
263	  ccm.e2.fast(~K, ~enc, k, m, nv, B.Octets.to_list(aad), pv, ccm.checks(m, B.len(nv), B.len.fast(pv)))
264	
265	# the plaintext of c (the ciphertext, then the m-byte tag), or CmTagMismatch
266	# when the tag does not match; no plaintext is released from a message that
267	# fails
268	def Ccm.decrypt(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, nonce: B.Octets, aad: B.Octets, c: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>:
269	  +cv = B.Octets.to_list(c)
270	  ccm.d2.fast(~K, ~enc, Nat.is_le(m, B.len.fast(cv)), k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), cv)