proofs/crypto/chacha/stream.bend
bend-collections-laws-crypto@1.0.0.0 · 264 lines · 19 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/core.bend as C
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as I
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/core.bend as K
7
8
9
10
11
12
13
14law words_eq:
15 for +xs: List<&2, U32>
16 {I.words(xs) == R.words(xs) : List<&2, U32>}
17
18def words_eq(xs):
19 match xs:
20 case Nil{}: {==}
21 case b0 <> Nil{}: {==}
22 case b0 <> b1 <> Nil{}: {==}
23 case b0 <> b1 <> b2 <> Nil{}: {==}
24 case b0 <> b1 <> b2 <> b3 <> rest:
25 %Equal.sym(List<&2, U32>, I.words(rest), R.words(rest), words_eq(rest)) :
26 {I.word(b0, b1, b2, b3) <> _ == R.word(b0, b1, b2, b3) <> R.words(rest) : List<&2, U32>}
27 {==}
28
29law key_eq:
30 for +ws: List<&2, U32>
31 {I.key_words(ws) == I.K{R.get(ws, 0n), R.get(ws, 1n), R.get(ws, 2n), R.get(ws, 3n), R.get(ws, 4n), R.get(ws, 5n), R.get(ws, 6n), R.get(ws, 7n)} : I.Key}
32
33def key_eq(ws):
34 match ws:
35 case Nil{}: {==}
36 case w0 <> Nil{}: {==}
37 case w0 <> w1 <> Nil{}: {==}
38 case w0 <> w1 <> w2 <> Nil{}: {==}
39 case w0 <> w1 <> w2 <> w3 <> Nil{}: {==}
40 case w0 <> w1 <> w2 <> w3 <> w4 <> Nil{}: {==}
41 case w0 <> w1 <> w2 <> w3 <> w4 <> w5 <> Nil{}: {==}
42 case w0 <> w1 <> w2 <> w3 <> w4 <> w5 <> w6 <> Nil{}: {==}
43 case w0 <> w1 <> w2 <> w3 <> w4 <> w5 <> w6 <> w7 <> rest: {==}
44
45law nonce_eq:
46 for +ws: List<&2, U32>
47 {I.nonce_words(ws) == I.N{R.get(ws, 0n), R.get(ws, 1n), R.get(ws, 2n)} : I.Nonce}
48
49def nonce_eq(ws):
50 match ws:
51 case Nil{}: {==}
52 case w0 <> Nil{}: {==}
53 case w0 <> w1 <> Nil{}: {==}
54 case w0 <> w1 <> w2 <> rest: {==}
55
56
57law hnonce_eq:
58 for +ws: List<&2, U32>
59 {[I.at(ws, 0n), I.at(ws, 1n), I.at(ws, 2n), I.at(ws, 3n)] == [R.get(ws, 0n), R.get(ws, 1n), R.get(ws, 2n), R.get(ws, 3n)] : List<&2, U32>}
60
61def hnonce_eq(ws):
62 match ws:
63 case Nil{}: {==}
64 case w0 <> Nil{}: {==}
65 case w0 <> w1 <> Nil{}: {==}
66 case w0 <> w1 <> w2 <> Nil{}: {==}
67 case w0 <> w1 <> w2 <> w3 <> rest: {==}
68
69
70
71law state_eq:
72 for +ks: List<&2, U32>
73 for +c: U32
74 for +ns: List<&2, U32>
75 {K.vec(I.state(I.key_words(ks), c, I.nonce_words(ns))) == R.state(ks, c, ns) : List<&2, U32>}
76
77def state_eq(ks, c, ns):
78 %Equal.sym(I.Key, I.key_words(ks), I.K{R.get(ks, 0n), R.get(ks, 1n), R.get(ks, 2n), R.get(ks, 3n), R.get(ks, 4n), R.get(ks, 5n), R.get(ks, 6n), R.get(ks, 7n)}, key_eq(ks)) :
79 {K.vec(I.state(_, c, I.nonce_words(ns))) == R.state(ks, c, ns) : List<&2, U32>}
80 %Equal.sym(I.Nonce, I.nonce_words(ns), I.N{R.get(ns, 0n), R.get(ns, 1n), R.get(ns, 2n)}, nonce_eq(ns)) :
81 {K.vec(I.state(I.K{R.get(ks, 0n), R.get(ks, 1n), R.get(ks, 2n), R.get(ks, 3n), R.get(ks, 4n), R.get(ks, 5n), R.get(ks, 6n), R.get(ks, 7n)}, c, _)) == R.state(ks, c, ns) : List<&2, U32>}
82 {==}
83
84law hstate_eq:
85 for +ks: List<&2, U32>
86 for +ns: List<&2, U32>
87 {K.vec(I.hstate(I.key_words(ks), ns)) == R.hstate(ks, ns) : List<&2, U32>}
88
89def hsl(+k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32, +k7: U32, l: List<&2, U32>) -> List<&2, U32>:
90 match l:
91 case n0 <> n1 <> n2 <> n3 <> rest: R.hstate([k0, k1, k2, k3, k4, k5, k6, k7], [n0, n1, n2, n3])
92 case _: Nil{}
93
94def hstate_eq(ks, ns):
95 %Equal.sym(I.Key, I.key_words(ks), I.K{R.get(ks, 0n), R.get(ks, 1n), R.get(ks, 2n), R.get(ks, 3n), R.get(ks, 4n), R.get(ks, 5n), R.get(ks, 6n), R.get(ks, 7n)}, key_eq(ks)) :
96 {K.vec(I.hstate(_, ns)) == R.hstate(ks, ns) : List<&2, U32>}
97 Equal.trans(List<&2, U32>,
98 K.vec(I.hstate(I.K{R.get(ks, 0n), R.get(ks, 1n), R.get(ks, 2n), R.get(ks, 3n), R.get(ks, 4n), R.get(ks, 5n), R.get(ks, 6n), R.get(ks, 7n)}, ns)),
99 hsl(R.get(ks, 0n), R.get(ks, 1n), R.get(ks, 2n), R.get(ks, 3n), R.get(ks, 4n), R.get(ks, 5n), R.get(ks, 6n), R.get(ks, 7n), [I.at(ns, 0n), I.at(ns, 1n), I.at(ns, 2n), I.at(ns, 3n)]),
100 R.hstate(ks, ns),
101 {==},
102 Equal.cong(List<&2, U32>, List<&2, U32>, l => hsl(R.get(ks, 0n), R.get(ks, 1n), R.get(ks, 2n), R.get(ks, 3n), R.get(ks, 4n), R.get(ks, 5n), R.get(ks, 6n), R.get(ks, 7n), l),
103 [I.at(ns, 0n), I.at(ns, 1n), I.at(ns, 2n), I.at(ns, 3n)], [R.get(ns, 0n), R.get(ns, 1n), R.get(ns, 2n), R.get(ns, 3n)], hnonce_eq(ns)))
104
105
106
107law body_correct:
108 for +r: Nat
109 for +kb: List<&2, U32>
110 for +c: U32
111 for +nb: List<&2, U32>
112 {I.keystream(r, I.key(kb), c, I.nonce(nb)) == R.block_body(r, kb, c, nb) : List<&2, U32>}
113
114def sblock(+r: Nat, +s: List<&2, U32>) -> List<&2, U32>:
115 R.serialize(R.add_words(s, R.inner_blocks(r, s)))
116
117def body_correct(r, kb, c, nb):
118 +S = I.state(I.key_words(I.words(kb)), c, I.nonce_words(I.words(nb)))
119 Equal.trans(List<&2, U32>, C.bytes(C.block(r, S)), sblock(r, K.vec(S)), R.block_body(r, kb, c, nb),
120 K.block_correct(r, S),
121 Equal.trans(List<&2, U32>, sblock(r, K.vec(S)), sblock(r, R.state(I.words(kb), c, I.words(nb))), R.block_body(r, kb, c, nb),
122 Equal.cong(List<&2, U32>, List<&2, U32>, l => sblock(r, l), K.vec(S), R.state(I.words(kb), c, I.words(nb)), state_eq(I.words(kb), c, I.words(nb))),
123 Equal.trans(List<&2, U32>, sblock(r, R.state(I.words(kb), c, I.words(nb))), sblock(r, R.state(R.words(kb), c, I.words(nb))), R.block_body(r, kb, c, nb),
124 Equal.cong(List<&2, U32>, List<&2, U32>, l => sblock(r, R.state(l, c, I.words(nb))), I.words(kb), R.words(kb), words_eq(kb)),
125 Equal.cong(List<&2, U32>, List<&2, U32>, l => sblock(r, R.state(R.words(kb), c, l)), I.words(nb), R.words(nb), words_eq(nb)))))
126
127law keystream_correct:
128 for +r: Nat
129 for +kb: List<&2, U32>
130 for +c: U32
131 for +nb: List<&2, U32>
132 {I.keystream(r, I.key(kb), c, I.nonce(nb)) == R.block_rounds(r, kb, c, nb) : List<&2, U32>}
133
134def keystream_correct(r, kb, c, nb):
135 match kb:
136 case Nil{}: body_correct(r, Nil{}, c, nb)
137 case b <> rest: body_correct(r, b <> rest, c, nb)
138
139law block_rounds_correct:
140 for +r: Nat
141 for +kb: List<&2, U32>
142 for +c: U32
143 for +nb: List<&2, U32>
144 {I.block_rounds(r, kb, c, nb) == R.block_rounds(r, kb, c, nb) : List<&2, U32>}
145
146def block_rounds_correct(r, kb, c, nb):
147 match kb:
148 case Nil{}: body_correct(r, Nil{}, c, nb)
149 case b <> rest: body_correct(r, b <> rest, c, nb)
150
151
152law bytes_length:
153 for +s: C.State
154 {List.length(&2, U32, C.bytes(s)) == 64n : Nat}
155
156def bytes_length(s):
157 match s:
158 case C.S{a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15}: {==}
159
160law block_length:
161 for +r: Nat
162 for +kb: List<&2, U32>
163 for +c: U32
164 for +nb: List<&2, U32>
165 {List.length(&2, U32, R.block_rounds(r, kb, c, nb)) == 64n : Nat}
166
167def block_length(r, kb, c, nb):
168 %keystream_correct(r, kb, c, nb) : {List.length(&2, U32, _) == 64n : Nat}
169 bytes_length(C.block(r, I.state(I.key(kb), c, I.nonce(nb))))
170
171
172
173law xor_front_eq:
174 for +ks: List<&2, U32>
175 for +xs: List<&2, U32>
176 {I.xor_front(ks, xs) == R.xor_bytes(R.prefix(List.length(&2, U32, ks), xs), ks) : List<&2, U32>}
177
178def xor_front_eq(ks, xs):
179 match ks xs:
180 case Nil{} _: {==}
181 case k <> kt Nil{}: {==}
182 case k <> kt x <> xt:
183 %Equal.sym(List<&2, U32>, I.xor_front(kt, xt), R.xor_bytes(R.prefix(List.length(&2, U32, kt), xt), kt), xor_front_eq(kt, xt)) :
184 {U32.xor(x, k) <> _ == U32.xor(x, k) <> R.xor_bytes(R.prefix(List.length(&2, U32, kt), xt), kt) : List<&2, U32>}
185 {==}
186
187law skip_eq:
188 for +n: Nat
189 for +xs: List<&2, U32>
190 {I.skip(n, xs) == R.suffix(n, xs) : List<&2, U32>}
191
192def skip_eq(n, xs):
193 match n xs:
194 case 0n _: {==}
195 case 1n+p Nil{}: {==}
196 case 1n+p x <> rest: skip_eq(p, rest)
197
198law take_eq:
199 for +n: Nat
200 for +xs: List<&2, U32>
201 {I.take(n, xs) == R.prefix(n, xs) : List<&2, U32>}
202
203def take_eq(n, xs):
204 match n xs:
205 case 0n _: {==}
206 case 1n+p Nil{}: {==}
207 case 1n+p x <> rest:
208 %Equal.sym(List<&2, U32>, I.take(p, rest), R.prefix(p, rest), take_eq(p, rest)) : {x <> _ == x <> R.prefix(p, rest) : List<&2, U32>}
209 {==}
210
211
212law front_correct:
213 for +r: Nat
214 for +kb: List<&2, U32>
215 for +c: U32
216 for +nb: List<&2, U32>
217 for +xs: List<&2, U32>
218 {I.xor_front(I.keystream(r, I.key(kb), c, I.nonce(nb)), xs) == R.xor_bytes(R.prefix(64n, xs), R.block_rounds(r, kb, c, nb)) : List<&2, U32>}
219
220def front_correct(r, kb, c, nb, xs):
221 +ks = I.keystream(r, I.key(kb), c, I.nonce(nb))
222 Equal.trans(List<&2, U32>, I.xor_front(ks, xs), R.xor_bytes(R.prefix(List.length(&2, U32, ks), xs), ks), R.xor_bytes(R.prefix(64n, xs), R.block_rounds(r, kb, c, nb)),
223 xor_front_eq(ks, xs),
224 Equal.trans(List<&2, U32>, R.xor_bytes(R.prefix(List.length(&2, U32, ks), xs), ks), R.xor_bytes(R.prefix(64n, xs), ks), R.xor_bytes(R.prefix(64n, xs), R.block_rounds(r, kb, c, nb)),
225 Equal.cong(Nat, List<&2, U32>, n => R.xor_bytes(R.prefix(n, xs), ks), List.length(&2, U32, ks), 64n, bytes_length(C.block(r, I.state(I.key(kb), c, I.nonce(nb))))),
226 Equal.cong(List<&2, U32>, List<&2, U32>, l => R.xor_bytes(R.prefix(64n, xs), l), ks, R.block_rounds(r, kb, c, nb), keystream_correct(r, kb, c, nb))))
227
228law stream_correct:
229 for +fuel: Nat
230 for +xs: List<&2, U32>
231 for +r: Nat
232 for +kb: List<&2, U32>
233 for +c: U32
234 for +nb: List<&2, U32>
235 {I.stream(fuel, xs, r, I.key(kb), c, I.nonce(nb)) == R.encrypt_blocks(R.blocks(fuel, xs), r, kb, c, nb) : List<&2, U32>}
236
237def stream_correct(fuel, xs, r, kb, c, nb):
238 match fuel xs:
239 case 0n _: {==}
240 case 1n+p Nil{}: {==}
241 case 1n+p x <> xt:
242 +c1 = U32.add(c, 1)
243 +ih = stream_correct(p, R.suffix(64n, x <> xt), r, kb, c1, nb)
244 +fr = front_correct(r, kb, c, nb, x <> xt)
245 +sk = skip_eq(64n, x <> xt)
246 %Equal.sym(List<&2, U32>, I.skip(64n, x <> xt), R.suffix(64n, x <> xt), sk) :
247 {List.append(&2, U32, I.xor_front(I.keystream(r, I.key(kb), c, I.nonce(nb)), x <> xt), I.stream(p, _, r, I.key(kb), c1, I.nonce(nb))) == R.encrypt_blocks(R.blocks(1n+p, x <> xt), r, kb, c, nb) : List<&2, U32>}
248 %Equal.sym(List<&2, U32>, I.stream(p, R.suffix(64n, x <> xt), r, I.key(kb), c1, I.nonce(nb)), R.encrypt_blocks(R.blocks(p, R.suffix(64n, x <> xt)), r, kb, c1, nb), ih) :
249 {List.append(&2, U32, I.xor_front(I.keystream(r, I.key(kb), c, I.nonce(nb)), x <> xt), _) == R.encrypt_blocks(R.blocks(1n+p, x <> xt), r, kb, c, nb) : List<&2, U32>}
250 %Equal.sym(List<&2, U32>, I.xor_front(I.keystream(r, I.key(kb), c, I.nonce(nb)), x <> xt), R.xor_bytes(R.prefix(64n, x <> xt), R.block_rounds(r, kb, c, nb)), fr) :
251 {List.append(&2, U32, _, R.encrypt_blocks(R.blocks(p, R.suffix(64n, x <> xt)), r, kb, c1, nb)) == R.encrypt_blocks(R.blocks(1n+p, x <> xt), r, kb, c, nb) : List<&2, U32>}
252 {==}
253
254law encrypt_correct:
255 for +r: Nat
256 for +kb: List<&2, U32>
257 for +c: U32
258 for +nb: List<&2, U32>
259 for +pt: List<&2, U32>
260 {I.encrypt_rounds(r, kb, c, nb, pt) == R.encrypt_rounds(r, kb, c, nb, pt) : List<&2, U32>}
261
262def encrypt_correct(r, kb, c, nb, pt):
263 stream_correct(List.length(&2, U32, pt), pt, r, kb, c, nb)
264