proofs/crypto/chacha/involution.bend

bend-collections-laws-crypto@1.0.0.0 · 220 lines · 13 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/stream.bend as T
6
7# The ChaCha20 stream cipher is an involution: encrypting the ciphertext
8# with the same key, counter and nonce gives the plaintext back, for every
9# byte list (every list of U32: the XOR works on whole words) and every
10# number of double rounds. The specification's block-by-block encryption is
11# first shown to be one XOR with the concatenated keystream ks, whose length
12# covers the message; XOR with the same keystream twice cancels.
13
14# ---------------------------------------------------------------- words
15
16law wxor_inv:
17  for +n: Nat
18  for +a: Word(n)
19  for +b: Word(n)
20  {Word.xor(n, Word.xor(n, a, b), b) == a : Word(n)}
21
22def wxor_inv(n, a, b):
23  match n:
24    case 0n:
25      match a b:
26        case WNil{} WNil{}: {==}
27    case 1n+p:
28      match a b:
29        case WCon{False{}, at} WCon{False{}, bt}: Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, Word.xor(p, Word.xor(p, at, bt), bt), at, wxor_inv(p, at, bt))
30        case WCon{False{}, at} WCon{True{}, bt}: Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, Word.xor(p, Word.xor(p, at, bt), bt), at, wxor_inv(p, at, bt))
31        case WCon{True{}, at} WCon{False{}, bt}: Equal.cong(Word(p), Word(1n+p), w => WCon{True{}, w}, Word.xor(p, Word.xor(p, at, bt), bt), at, wxor_inv(p, at, bt))
32        case WCon{True{}, at} WCon{True{}, bt}: Equal.cong(Word(p), Word(1n+p), w => WCon{True{}, w}, Word.xor(p, Word.xor(p, at, bt), bt), at, wxor_inv(p, at, bt))
33
34law u32_xor_inv:
35  for +a: U32
36  for +b: U32
37  {U32.xor(U32.xor(a, b), b) == a : U32}
38
39def u32_xor_inv(a, b):
40  match a b:
41    case U32{x} U32{y}:
42      Equal.cong(Word(32n), U32, w => U32{w}, Word.xor(32n, Word.xor(32n, x, y), y), x, wxor_inv(32n, x, y))
43
44# ---------------------------------------------------------------- lengths
45
46law length_append:
47  for +xs: List<&2, U32>
48  for +ys: List<&2, U32>
49  {List.length(&2, U32, List.append(&2, U32, xs, ys)) == Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}
50
51def length_append(xs, ys):
52  match xs:
53    case Nil{}: {==}
54    case x <> xt:
55      Equal.cong(Nat, Nat, n => 1n+n, List.length(&2, U32, List.append(&2, U32, xt, ys)), Nat.add(List.length(&2, U32, xt), List.length(&2, U32, ys)), length_append(xt, ys))
56
57law le_add:
58  for +p: Nat
59  for +l: Nat
60  for +k: Nat
61  for +h: {Nat.is_le(p, l) == True{} : Bool}
62  {Nat.is_le(p, Nat.add(k, l)) == True{} : Bool}
63
64def le_add(p, l, k, h):
65  match k:
66    case 0n: h
67    case 1n+j: N.le_trans(p, Nat.add(j, l), 1n+Nat.add(j, l), le_add(p, l, j, h), N.le_succ(Nat.add(j, l)))
68
69law xor_length:
70  for +xs: List<&2, U32>
71  for +ks: List<&2, U32>
72  for +h: {Nat.is_le(List.length(&2, U32, xs), List.length(&2, U32, ks)) == True{} : Bool}
73  {List.length(&2, U32, R.xor_bytes(xs, ks)) == List.length(&2, U32, xs) : Nat}
74
75def xor_length(xs, ks, h):
76  match xs ks:
77    case Nil{} _: {==}
78    case x <> xt Nil{}: Empty.absurd({0n == 1n+List.length(&2, U32, xt) : Nat}, L.false_true(h))
79    case x <> xt k <> kt:
80      Equal.cong(Nat, Nat, n => 1n+n, List.length(&2, U32, R.xor_bytes(xt, kt)), List.length(&2, U32, xt), xor_length(xt, kt, h))
81
82law xor_twice:
83  for +xs: List<&2, U32>
84  for +ks: List<&2, U32>
85  for +h: {Nat.is_le(List.length(&2, U32, xs), List.length(&2, U32, ks)) == True{} : Bool}
86  {R.xor_bytes(R.xor_bytes(xs, ks), ks) == xs : List<&2, U32>}
87
88def xor_twice(xs, ks, h):
89  match xs ks:
90    case Nil{} _: {==}
91    case x <> xt Nil{}: Empty.absurd({Nil{} == x <> xt : List<&2, U32>}, L.false_true(h))
92    case x <> xt k <> kt:
93      %Equal.sym(List<&2, U32>, R.xor_bytes(R.xor_bytes(xt, kt), kt), xt, xor_twice(xt, kt, h)) :
94        {U32.xor(U32.xor(x, k), k) <> _ == x <> xt : List<&2, U32>}
95      %Equal.sym(U32, U32.xor(U32.xor(x, k), k), x, u32_xor_inv(x, k)) :
96        {_ <> xt == x <> xt : List<&2, U32>}
97      {==}
98
99# ---------------------------------------------------------------- one keystream
100
101# The keystream of fuel blocks from counter c.
102def ks(fuel: Nat, +r: Nat, +kb: List<&2, U32>, +c: U32, +nb: List<&2, U32>) -> List<&2, U32>:
103  match fuel:
104    case 0n: Nil{}
105    case 1n+p: List.append(&2, U32, R.block_rounds(r, kb, c, nb), ks(p, r, kb, U32.add(c, 1), nb))
106
107law ks_length:
108  for +fuel: Nat
109  for +r: Nat
110  for +kb: List<&2, U32>
111  for +c: U32
112  for +nb: List<&2, U32>
113  {Nat.is_le(fuel, List.length(&2, U32, ks(fuel, r, kb, c, nb))) == True{} : Bool}
114
115def ks_length(fuel, r, kb, c, nb):
116  match fuel:
117    case 0n: {==}
118    case 1n+p:
119      +c1 = U32.add(c, 1)
120      %Equal.sym(Nat, List.length(&2, U32, List.append(&2, U32, R.block_rounds(r, kb, c, nb), ks(p, r, kb, c1, nb))), Nat.add(List.length(&2, U32, R.block_rounds(r, kb, c, nb)), List.length(&2, U32, ks(p, r, kb, c1, nb))), length_append(R.block_rounds(r, kb, c, nb), ks(p, r, kb, c1, nb))) :
121        {Nat.is_le(1n+p, _) == True{} : Bool}
122      %Equal.sym(Nat, List.length(&2, U32, R.block_rounds(r, kb, c, nb)), 64n, T.block_length(r, kb, c, nb)) :
123        {Nat.is_le(1n+p, Nat.add(_, List.length(&2, U32, ks(p, r, kb, c1, nb)))) == True{} : Bool}
124      le_add(p, List.length(&2, U32, ks(p, r, kb, c1, nb)), 63n, ks_length(p, r, kb, c1, nb))
125
126law xor_append:
127  for +bs: List<&2, U32>
128  for +xs: List<&2, U32>
129  for +k: List<&2, U32>
130  {R.xor_bytes(xs, List.append(&2, U32, bs, k)) == List.append(&2, U32, R.xor_bytes(R.prefix(List.length(&2, U32, bs), xs), bs), R.xor_bytes(R.suffix(List.length(&2, U32, bs), xs), k)) : List<&2, U32>}
131
132def xor_append(bs, xs, k):
133  match bs xs:
134    case Nil{} _: {==}
135    case b <> bt Nil{}: {==}
136    case b <> bt x <> xt:
137      %xor_append(bt, xt, k) :
138        {U32.xor(x, b) <> R.xor_bytes(xt, List.append(&2, U32, bt, k)) == U32.xor(x, b) <> _ : List<&2, U32>}
139      {==}
140
141law enc_ks:
142  for +fuel: Nat
143  for +xs: List<&2, U32>
144  for +r: Nat
145  for +kb: List<&2, U32>
146  for +c: U32
147  for +nb: List<&2, U32>
148  {R.encrypt_blocks(R.blocks(fuel, xs), r, kb, c, nb) == R.xor_bytes(xs, ks(fuel, r, kb, c, nb)) : List<&2, U32>}
149
150def enc_ks(fuel, xs, r, kb, c, nb):
151  match fuel xs:
152    case 0n Nil{}: {==}
153    case 0n x <> xt: {==}
154    case 1n+p Nil{}: {==}
155    case 1n+p x <> xt:
156      +c1 = U32.add(c, 1)
157      +B = R.block_rounds(r, kb, c, nb)
158      +K = ks(p, r, kb, c1, nb)
159      +X = {x <> xt : List<&2, U32>}
160      +left = List.append(&2, U32, R.xor_bytes(R.prefix(64n, X), B), R.xor_bytes(R.suffix(64n, X), K))
161      Equal.trans(List<&2, U32>,
162        List.append(&2, U32, R.xor_bytes(R.prefix(64n, X), B), R.encrypt_blocks(R.blocks(p, R.suffix(64n, X)), r, kb, c1, nb)),
163        left,
164        R.xor_bytes(X, List.append(&2, U32, B, K)),
165        Equal.cong(List<&2, U32>, List<&2, U32>, l => List.append(&2, U32, R.xor_bytes(R.prefix(64n, X), B), l),
166          R.encrypt_blocks(R.blocks(p, R.suffix(64n, X)), r, kb, c1, nb), R.xor_bytes(R.suffix(64n, X), K), enc_ks(p, R.suffix(64n, X), r, kb, c1, nb)),
167        Equal.sym(List<&2, U32>, R.xor_bytes(X, List.append(&2, U32, B, K)), left,
168          Equal.trans(List<&2, U32>, R.xor_bytes(X, List.append(&2, U32, B, K)),
169            List.append(&2, U32, R.xor_bytes(R.prefix(List.length(&2, U32, B), X), B), R.xor_bytes(R.suffix(List.length(&2, U32, B), X), K)),
170            left,
171            xor_append(B, X, K),
172            Equal.cong(Nat, List<&2, U32>, n => List.append(&2, U32, R.xor_bytes(R.prefix(n, X), B), R.xor_bytes(R.suffix(n, X), K)),
173              List.length(&2, U32, B), 64n, T.block_length(r, kb, c, nb)))))
174
175# ---------------------------------------------------------------- the involution
176
177law encrypt_xor:
178  for +r: Nat
179  for +kb: List<&2, U32>
180  for +c: U32
181  for +nb: List<&2, U32>
182  for +pt: List<&2, U32>
183  {R.encrypt_rounds(r, kb, c, nb, pt) == R.xor_bytes(pt, ks(List.length(&2, U32, pt), r, kb, c, nb)) : List<&2, U32>}
184
185def encrypt_xor(r, kb, c, nb, pt):
186  enc_ks(List.length(&2, U32, pt), pt, r, kb, c, nb)
187
188# The ciphertext is as long as the plaintext.
189law encrypt_length:
190  for +r: Nat
191  for +kb: List<&2, U32>
192  for +c: U32
193  for +nb: List<&2, U32>
194  for +pt: List<&2, U32>
195  {List.length(&2, U32, R.encrypt_rounds(r, kb, c, nb, pt)) == List.length(&2, U32, pt) : Nat}
196
197def encrypt_length(r, kb, c, nb, pt):
198  +K = ks(List.length(&2, U32, pt), r, kb, c, nb)
199  %Equal.sym(List<&2, U32>, R.encrypt_rounds(r, kb, c, nb, pt), R.xor_bytes(pt, K), encrypt_xor(r, kb, c, nb, pt)) :
200    {List.length(&2, U32, _) == List.length(&2, U32, pt) : Nat}
201  xor_length(pt, K, ks_length(List.length(&2, U32, pt), r, kb, c, nb))
202
203law involution:
204  for +r: Nat
205  for +kb: List<&2, U32>
206  for +c: U32
207  for +nb: List<&2, U32>
208  for +pt: List<&2, U32>
209  {R.encrypt_rounds(r, kb, c, nb, R.encrypt_rounds(r, kb, c, nb, pt)) == pt : List<&2, U32>}
210
211def involution(r, kb, c, nb, pt):
212  +ct = R.encrypt_rounds(r, kb, c, nb, pt)
213  +K = ks(List.length(&2, U32, pt), r, kb, c, nb)
214  Equal.trans(List<&2, U32>, R.encrypt_rounds(r, kb, c, nb, ct), R.xor_bytes(ct, ks(List.length(&2, U32, ct), r, kb, c, nb)), pt,
215    encrypt_xor(r, kb, c, nb, ct),
216    Equal.trans(List<&2, U32>, R.xor_bytes(ct, ks(List.length(&2, U32, ct), r, kb, c, nb)), R.xor_bytes(ct, K), pt,
217      Equal.cong(Nat, List<&2, U32>, n => R.xor_bytes(ct, ks(n, r, kb, c, nb)), List.length(&2, U32, ct), List.length(&2, U32, pt), encrypt_length(r, kb, c, nb, pt)),
218      Equal.trans(List<&2, U32>, R.xor_bytes(ct, K), R.xor_bytes(R.xor_bytes(pt, K), K), pt,
219        Equal.cong(List<&2, U32>, List<&2, U32>, l => R.xor_bytes(l, K), ct, R.xor_bytes(pt, K), encrypt_xor(r, kb, c, nb, pt)),
220        xor_twice(pt, K, ks_length(List.length(&2, U32, pt), r, kb, c, nb)))))