1 import Base 2 import ../libs/AES256GCM.bend as AES 3 import ../libs/AES256GCMCore.bend as Core 4 import ./AES_ZipLengthProof.bend as ZipLengthProof 5 import ./AES_LengthLimitProof.bend as LengthLimitProof 6 import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32.bend as HubU32 7 8 def bool_mask_xor_inv(+mask: Bool, +x: Bool, +y: Bool) -> 9 {Bool.and(mask, 10 Bool.xor(Bool.and(mask, Bool.xor(x, y)), y)) == 11 Bool.and(mask, x) : Bool}: 12 match mask x y: 13 case False{} False{} False{}: {==} 14 case False{} False{} True{}: {==} 15 case False{} True{} False{}: {==} 16 case False{} True{} True{}: {==} 17 case True{} False{} False{}: {==} 18 case True{} False{} True{}: {==} 19 case True{} True{} False{}: {==} 20 case True{} True{} True{}: {==} 21 22 def word_mask_xor_inv(+n: Nat, +mask: Word(n), +x: Word(n), +y: Word(n)) -> 23 {Word.and(n, mask, 24 Word.xor(n, Word.and(n, mask, Word.xor(n, x, y)), y)) == 25 Word.and(n, mask, x) : Word(n)}: 26 match n mask x y: 27 case 0n WNil{} WNil{} WNil{}: {==} 28 case 1n+p WCon{m, mt} WCon{xb, xt} WCon{yb, yt}: 29 head = bool_mask_xor_inv(m, xb, yb) 30 tail = word_mask_xor_inv(p, mt, xt, yt) 31 Equal.trans(Word(1n+p), 32 Word.and(1n+p, WCon{m, mt}, 33 Word.xor(1n+p, 34 Word.and(1n+p, WCon{m, mt}, 35 Word.xor(1n+p, WCon{xb, xt}, WCon{yb, yt})), 36 WCon{yb, yt})), 37 WCon{Bool.and(m, 38 Bool.xor(Bool.and(m, Bool.xor(xb, yb)), yb)), 39 Word.and(p, mt, 40 Word.xor(p, Word.and(p, mt, 41 Word.xor(p, xt, yt)), yt))}, 42 WCon{Bool.and(m, xb), Word.and(p, mt, xt)}, 43 {==}, 44 Equal.trans(Word(1n+p), 45 WCon{Bool.and(m, 46 Bool.xor(Bool.and(m, Bool.xor(xb, yb)), yb)), 47 Word.and(p, mt, 48 Word.xor(p, Word.and(p, mt, 49 Word.xor(p, xt, yt)), yt))}, 50 WCon{Bool.and(m, xb), 51 Word.and(p, mt, 52 Word.xor(p, Word.and(p, mt, 53 Word.xor(p, xt, yt)), yt))}, 54 WCon{Bool.and(m, xb), Word.and(p, mt, xt)}, 55 Equal.cong(Bool, Word(1n+p), 56 bit => WCon{bit, 57 Word.and(p, mt, 58 Word.xor(p, Word.and(p, mt, 59 Word.xor(p, xt, yt)), yt))}, 60 Bool.and(m, 61 Bool.xor(Bool.and(m, Bool.xor(xb, yb)), yb)), 62 Bool.and(m, xb), head), 63 Equal.cong(Word(p), Word(1n+p), 64 bits => WCon{Bool.and(m, xb), bits}, 65 Word.and(p, mt, 66 Word.xor(p, Word.and(p, mt, 67 Word.xor(p, xt, yt)), yt)), 68 Word.and(p, mt, xt), tail))) 69 70 def word_bits(+value: U32) -> Word(32n): 71 match value: 72 case U32{bits}: bits 73 74 def gcm_mask_xor_inv(+x: U32, +y: U32) -> 75 {Core.gcm_hex_mask( 76 U32.xor(Core.gcm_hex_mask(U32.xor(x, y), 255), y), 255) == 77 Core.gcm_hex_mask(x, 255) : U32}: 78 match x y: 79 case U32{xb} U32{yb}: 80 Equal.cong(Word(32n), U32, bits => U32{bits}, 81 Word.and(32n, word_bits(255), 82 Word.xor(32n, 83 Word.and(32n, word_bits(255), 84 Word.xor(32n, xb, yb)), yb)), 85 Word.and(32n, word_bits(255), xb), 86 word_mask_xor_inv(32n, word_bits(255), xb, yb)) 87 88 def bool_and_comm(+a: Bool, +b: Bool) -> {Bool.and(a, b) == Bool.and(b, a) : Bool}: 89 match a b: 90 case False{} False{}: {==} 91 case False{} True{}: {==} 92 case True{} False{}: {==} 93 case True{} True{}: {==} 94 95 def word_and_comm(+n: Nat, +x: Word(n), +y: Word(n)) -> 96 {Word.and(n, x, y) == Word.and(n, y, x) : Word(n)}: 97 match n x y: 98 case 0n WNil{} WNil{}: {==} 99 case 1n+p WCon{xb, xt} WCon{yb, yt}: 100 head = bool_and_comm(xb, yb) 101 tail = word_and_comm(p, xt, yt) 102 Equal.trans(Word(1n+p), 103 Word.and(1n+p, WCon{xb, xt}, WCon{yb, yt}), 104 WCon{Bool.and(xb, yb), Word.and(p, xt, yt)}, 105 Word.and(1n+p, WCon{yb, yt}, WCon{xb, xt}), 106 {==}, 107 Equal.trans(Word(1n+p), 108 WCon{Bool.and(xb, yb), Word.and(p, xt, yt)}, 109 WCon{Bool.and(yb, xb), Word.and(p, xt, yt)}, 110 WCon{Bool.and(yb, xb), Word.and(p, yt, xt)}, 111 Equal.cong(Bool, Word(1n+p), 112 bit => WCon{bit, Word.and(p, xt, yt)}, 113 Bool.and(xb, yb), Bool.and(yb, xb), head), 114 Equal.cong(Word(p), Word(1n+p), 115 bits => WCon{Bool.and(yb, xb), bits}, 116 Word.and(p, xt, yt), Word.and(p, yt, xt), tail))) 117 118 def byte_mask_identity(+value: U32, 119 below_256: {U32.is_lt(value, 256) == True{} : Bool}) -> 120 {Core.gcm_hex_mask(value, 255) == value : U32}: 121 match value: 122 case U32{bits}: 123 nat_below = Equal.trans(Bool, 124 Nat.is_lt(U32.to_nat(U32{bits}), U32.to_nat(256)), 125 U32.is_lt(U32{bits}, 256), 126 True{}, 127 Equal.sym(Bool, 128 U32.is_lt(U32{bits}, 256), 129 Nat.is_lt(U32.to_nat(U32{bits}), U32.to_nat(256)), 130 HubU32.is_lt_nat(U32{bits}, 256)), 131 below_256) 132 scaled_below = Equal.trans(Bool, 133 Nat.is_lt(U32.to_nat(U32{bits}), U32.to_nat(256)), 134 Nat.is_lt(U32.to_nat(U32{bits}), 256n), 135 True{}, 136 Equal.cong(Nat, Bool, 137 bound => Nat.is_lt(U32.to_nat(U32{bits}), bound), 138 U32.to_nat(256), 256n, {==}), 139 nat_below) 140 masked = HubU32.mask_word(U32{bits}, 255, 8n, 141 {==}, scaled_below) 142 Equal.trans(U32, 143 Core.gcm_hex_mask(U32{bits}, 255), 144 U32.and(255, U32{bits}), 145 U32{bits}, {==}, 146 Equal.trans(U32, 147 U32.and(255, U32{bits}), 148 U32.and(U32{bits}, 255), 149 U32{bits}, 150 Equal.cong(Word(32n), U32, w => U32{w}, 151 Word.and(32n, word_bits(255), bits), 152 Word.and(32n, bits, word_bits(255)), 153 word_and_comm(32n, word_bits(255), bits)), 154 masked)) 155 156 def bool_and_true_left(+a: Bool, +b: Bool, 157 both: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}: 158 match a b: 159 case False{} False{}: 160 Empty.absurd({False{} == True{} : Bool}, 161 ZipLengthProof.false_true(both)) 162 case False{} True{}: 163 Empty.absurd({False{} == True{} : Bool}, 164 ZipLengthProof.false_true(both)) 165 case True{} False{}: {==} 166 case True{} True{}: {==} 167 168 def bool_and_true_right(+a: Bool, +b: Bool, 169 both: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}: 170 match a b: 171 case False{} False{}: 172 Empty.absurd({False{} == True{} : Bool}, 173 ZipLengthProof.false_true(both)) 174 case False{} True{}: {==} 175 case True{} False{}: 176 Empty.absurd({False{} == True{} : Bool}, 177 ZipLengthProof.false_true(both)) 178 case True{} True{}: {==} 179 180 def mask_bytes_identity(+bytes: List<&2, U32>, 181 +valid: {Core.gcm_bytes_valid(bytes) == True{} : Bool}) -> 182 {Core.gcm_mask_bytes(bytes) == bytes : List<&2, U32>}: 183 match bytes: 184 case Nil{}: {==} 185 case byte <> tail: 186 head_valid = bool_and_true_left(U32.is_lt(byte, 256), 187 Core.gcm_bytes_valid(tail), valid) 188 tail_valid = bool_and_true_right(U32.is_lt(byte, 256), 189 Core.gcm_bytes_valid(tail), valid) 190 recursive = mask_bytes_identity(tail, tail_valid) 191 Equal.trans(List<&2, U32>, 192 Core.gcm_mask_bytes(byte <> tail), 193 byte <> Core.gcm_mask_bytes(tail), 194 byte <> tail, 195 Equal.cong(U32, List<&2, U32>, 196 head => head <> Core.gcm_mask_bytes(tail), 197 Core.gcm_hex_mask(byte, 255), byte, 198 byte_mask_identity(byte, head_valid)), 199 Equal.cong(List<&2, U32>, List<&2, U32>, 200 rest => byte <> rest, 201 Core.gcm_mask_bytes(tail), tail, recursive)) 202 203 def predecessor(n: Nat) -> Nat: 204 match n: 205 case 0n: 0n 206 case 1n+p: p 207 208 def zip_xor_involution(+bytes: List<&2, U32>, 209 +stream: List<&2, U32>, 210 same_length: {List.length(&2, U32, bytes) == 211 List.length(&2, U32, stream) : Nat}) -> 212 {Core.gcm_zip_xor(Core.gcm_zip_xor(bytes, stream), stream) == 213 Core.gcm_mask_bytes(bytes) : List<&2, U32>}: 214 match bytes stream: 215 case Nil{} _: 216 +inner = Core.gcm_zip_xor_nil_left(stream) 217 Equal.trans(List<&2, U32>, 218 Core.gcm_zip_xor(Core.gcm_zip_xor(Nil{}, stream), stream), 219 Core.gcm_zip_xor(Nil{}, stream), Nil{}, 220 Equal.cong(List<&2, U32>, List<&2, U32>, 221 xs => Core.gcm_zip_xor(xs, stream), 222 Core.gcm_zip_xor(Nil{}, stream), Nil{}, inner), 223 inner) 224 case _ <> _ Nil{}: 225 unequal = Equal.cong(Nat, Bool, 226 n => Nat.is_eq(n, 0n), 227 List.length(&2, U32, bytes), 228 List.length(&2, U32, Nil{}), same_length) 229 Empty.absurd( 230 {Core.gcm_zip_xor(Core.gcm_zip_xor(bytes, Nil{}), Nil{}) == 231 Core.gcm_mask_bytes(bytes) : List<&2, U32>}, 232 ZipLengthProof.false_true(unequal)) 233 case byte <> tail stream_byte <> stream_tail: 234 tail_length = Equal.cong(Nat, Nat, predecessor, 235 List.length(&2, U32, byte <> tail), 236 List.length(&2, U32, stream_byte <> stream_tail), 237 same_length) 238 recursive = zip_xor_involution(tail, stream_tail, tail_length) 239 Equal.trans(List<&2, U32>, 240 Core.gcm_zip_xor( 241 Core.gcm_zip_xor(byte <> tail, 242 stream_byte <> stream_tail), 243 stream_byte <> stream_tail), 244 Core.gcm_hex_mask(U32.xor( 245 Core.gcm_hex_mask(U32.xor(byte, stream_byte), 255), 246 stream_byte), 255) <> 247 Core.gcm_zip_xor( 248 Core.gcm_zip_xor(tail, stream_tail), stream_tail), 249 Core.gcm_mask_bytes(byte <> tail), 250 {==}, 251 Equal.trans(List<&2, U32>, 252 Core.gcm_hex_mask(U32.xor( 253 Core.gcm_hex_mask(U32.xor(byte, stream_byte), 255), 254 stream_byte), 255) <> 255 Core.gcm_zip_xor( 256 Core.gcm_zip_xor(tail, stream_tail), stream_tail), 257 Core.gcm_hex_mask(byte, 255) <> 258 Core.gcm_zip_xor( 259 Core.gcm_zip_xor(tail, stream_tail), stream_tail), 260 Core.gcm_mask_bytes(byte <> tail), 261 Equal.cong(U32, List<&2, U32>, 262 head => head <> 263 Core.gcm_zip_xor( 264 Core.gcm_zip_xor(tail, stream_tail), stream_tail), 265 Core.gcm_hex_mask(U32.xor( 266 Core.gcm_hex_mask(U32.xor(byte, stream_byte), 255), 267 stream_byte), 255), 268 Core.gcm_hex_mask(byte, 255), 269 gcm_mask_xor_inv(byte, stream_byte)), 270 Equal.cong(List<&2, U32>, List<&2, U32>, 271 rest => Core.gcm_hex_mask(byte, 255) <> rest, 272 Core.gcm_zip_xor( 273 Core.gcm_zip_xor(tail, stream_tail), stream_tail), 274 Core.gcm_mask_bytes(tail), recursive))) 275 276 def ctr_decrypt_ciphertext_roundtrip(+words: List<&2, U32>, 277 +nonce: List<&2, U32>, +plaintext: List<&2, U32>, 278 +valid: {Core.gcm_bytes_valid(plaintext) == True{} : Bool}) -> 279 {Core.gcm_decrypt_expanded(words, nonce, 280 Core.gcm_zip_xor(plaintext, 281 Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext), 282 words, Core.gcm_inc32(Core.gcm_j0(nonce))))) == 283 plaintext : List<&2, U32>}: 284 +start = Core.gcm_inc32(Core.gcm_j0(nonce)) 285 +stream = Core.gcm_ctr_stream_exact( 286 List.length(&2, U32, plaintext), words, start) 287 +same_length = Equal.sym(Nat, 288 List.length(&2, U32, stream), 289 List.length(&2, U32, plaintext), 290 ZipLengthProof.ctr_stream_exact_length( 291 List.length(&2, U32, plaintext), words, start)) 292 cipher_length = ZipLengthProof.zip_length_equal(plaintext, stream, 293 same_length) 294 decrypt_stream = Equal.cong(Nat, List<&2, U32>, 295 fuel => Core.gcm_ctr_stream_exact(fuel, words, start), 296 List.length(&2, U32, 297 Core.gcm_zip_xor(plaintext, stream)), 298 List.length(&2, U32, plaintext), cipher_length) 299 Equal.trans(List<&2, U32>, 300 Core.gcm_decrypt_expanded(words, nonce, 301 Core.gcm_zip_xor(plaintext, stream)), 302 Core.gcm_zip_xor(Core.gcm_zip_xor(plaintext, stream), stream), 303 plaintext, 304 Equal.cong(List<&2, U32>, List<&2, U32>, 305 stream2 => Core.gcm_zip_xor( 306 Core.gcm_zip_xor(plaintext, stream), stream2), 307 Core.gcm_ctr_stream_exact( 308 List.length(&2, U32, 309 Core.gcm_zip_xor(plaintext, stream)), words, start), 310 stream, decrypt_stream), 311 Equal.trans(List<&2, U32>, 312 Core.gcm_zip_xor(Core.gcm_zip_xor(plaintext, stream), stream), 313 Core.gcm_mask_bytes(plaintext), plaintext, 314 zip_xor_involution(plaintext, stream, same_length), 315 mask_bytes_identity(plaintext, valid))) 316 317 def ctr_ciphertext_plaintext_valid(+plaintext: List<&2, U32>, 318 +stream: List<&2, U32>, 319 same_length: {List.length(&2, U32, plaintext) == 320 List.length(&2, U32, stream) : Nat}, 321 +plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}) -> 322 {AES.plaintext_valid(Core.gcm_zip_xor(plaintext, stream)) == 323 True{} : Bool}: 324 +ciphertext = Core.gcm_zip_xor(plaintext, stream) 325 cipher_length = ZipLengthProof.zip_length_equal(plaintext, stream, 326 same_length) 327 output_bytes_ok = AES.core_bytes_valid_proof(ciphertext, 328 Core.gcm_zip_xor_valid(plaintext, stream)) 329 plaintext_limit_ok = bool_and_true_right(AES.bytes_valid(plaintext), 330 AES.bytes_length_limit(plaintext, 4294967264, 15), plaintext_ok) 331 output_limit_eq = LengthLimitProof.bytes_length_limit_same(plaintext, 332 ciphertext, 4294967264, 15, Equal.sym(Nat, 333 List.length(&2, U32, ciphertext), 334 List.length(&2, U32, plaintext), cipher_length)) 335 output_limit_ok = Equal.trans(Bool, 336 AES.bytes_length_limit(ciphertext, 4294967264, 15), 337 AES.bytes_length_limit(plaintext, 4294967264, 15), 338 True{}, Equal.sym(Bool, 339 AES.bytes_length_limit(plaintext, 4294967264, 15), 340 AES.bytes_length_limit(ciphertext, 4294967264, 15), 341 output_limit_eq), plaintext_limit_ok) 342 Equal.trans(Bool, AES.plaintext_valid(ciphertext), 343 Bool.and(AES.bytes_valid(ciphertext), 344 AES.bytes_length_limit(ciphertext, 4294967264, 15)), 345 True{}, {==}, 346 Equal.trans(Bool, 347 Bool.and(AES.bytes_valid(ciphertext), 348 AES.bytes_length_limit(ciphertext, 4294967264, 15)), 349 Bool.and(True{}, 350 AES.bytes_length_limit(ciphertext, 4294967264, 15)), 351 True{}, 352 Equal.cong(Bool, Bool, 353 byte_ok => Bool.and(byte_ok, 354 AES.bytes_length_limit(ciphertext, 4294967264, 15)), 355 AES.bytes_valid(ciphertext), True{}, output_bytes_ok), 356 Equal.trans(Bool, 357 Bool.and(True{}, 358 AES.bytes_length_limit(ciphertext, 4294967264, 15)), 359 AES.bytes_length_limit(ciphertext, 4294967264, 15), 360 True{}, {==}, output_limit_ok)))