modes.bend

bend-osdev-crypto@0.1.0.0 · 294 lines · 42 definitions

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).
12import Base
13import bend-osdev-bytes@0.1.0.0/bytes.bend as B
14import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
15import bend-osdev-crypto@0.1.0.0/stream.bend as St
16
17# Lists of blocks
18
19def 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
28def 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
35def 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
42def 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
45def 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
50def 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
58def 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
65def 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
73def 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
82def 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
85def 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
90def cr.pick_n(full: Bool, +n: Nat) -> Nat:
91  match full:
92    case True{}:
93      0n
94    case False{}:
95      n
96
97def 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
104def 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)
113def 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
123def 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
131def 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
138def 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
145def 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
152def 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)
160def 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
165def 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
173def 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
176def 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)
184def 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
189def 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
192def 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
195def 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
201def 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
215type CrCtrState<-K: Data> is Data:
216  CrCtrState{key: K, ctr: List<&2, U32>, buf: List<&2, U32>}
217
218def 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
225def 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
234def 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
242def cr.ctr.inc(xs: List<&2, U32>) -> List<&2, U32>:
243  cr.ctr.add1(St.cr.rev_onto(xs, Nil{}), True{}, Nil{})
244
245def 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
252def cr.head(xs: List<&2, U32>) -> U32:
253  match xs:
254    case Nil{}:
255      0
256    case Con{h, t}:
257      h
258
259def 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
266def 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
275def 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
280def 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)
289def 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
293def 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)