ccm.bend

bend-osdev-cipher-modes@0.1.0.0 · 270 lines · 41 definitions

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.
15import Base
16import bend-osdev-bytes@0.1.0.0/bytes.bend as B
17import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
18
19# the low n bytes of v, most significant first (zeros above the 32 bits of v)
20def 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
24def 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
28def 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
35def 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
44def 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
52def 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
59def 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)
63def 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)
67def 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
75def 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
81def 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
84def 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)
89def 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
96def 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
103def ccm.len_ok(+l: Nat, +n: Nat) -> Bool:
104  ccm.len_ok.two(Nat.is_eq(l, 2n), l, n)
105
106def 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
113def 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
120def 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
128def 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
132def 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
137def 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
144def 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
152def 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
159def 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
166def 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
179def 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
182def 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
190def 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
196def 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
200def 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
207def 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
210def 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
215def 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
220def 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
227def 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
234def 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
241def 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)
250def 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
255def 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
260def 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
268def 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)