1 import Base 2 import ../../../spec/crypto/chacha.bend as R 3 import ../../lib/logic.bend as L 4 import ../../lib/nat.bend as N 5 import ./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 16 law 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 22 def 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 34 law u32_xor_inv: 35 for +a: U32 36 for +b: U32 37 {U32.xor(U32.xor(a, b), b) == a : U32} 38 39 def 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 46 law 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 51 def 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 57 law 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 64 def 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 69 law 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 75 def 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 82 law 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 88 def 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. 102 def 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 107 law 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 115 def 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 126 law 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 132 def 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 141 law 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 150 def 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 177 law 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 185 def 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. 189 law 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 197 def 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 203 law 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 211 def 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)))))