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_CoreTagProof.bend as CoreTagProof 6 import ./AES_MaskedXorProof.bend as MaskedXorProof 7 import ./AES_LengthLimitProof.bend as LengthLimitProof 8 import ./AES_TagCompareProof.bend as TagCompareProof 9 10 type TagContext is Data: 11 TagContext{ 12 words: List<&2, U32>, 13 nonce: List<&2, U32>, 14 aad: List<&2, U32>, 15 ciphertext: List<&2, U32> 16 } 17 18 def result_ciphertext(fallback: List<&2, U32>, 19 result: Result<&2, &2, AES.Error, AES.Envelope>) -> List<&2, U32>: 20 match result: 21 case Fail{error}: fallback 22 case Done{envelope}: AES.ciphertext(envelope) 23 24 def output_tag_context(output: Core.GcmOutput) -> TagContext: 25 match output: 26 case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes, 27 tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}: 28 TagContext{tag_words, tag_nonce, tag_aad, ciphertext} 29 30 def tag_for_context(context: TagContext) -> List<&2, U32>: 31 match context: 32 case TagContext{words, nonce, aad, ciphertext}: 33 Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, 34 ciphertext)) 35 36 def output_tag_matches_context(+output: Core.GcmOutput) -> 37 {CoreTagProof.output_tag(output) == 38 tag_for_context(output_tag_context(output)) : List<&2, U32>}: 39 match output: 40 case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes, 41 tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}: 42 tag_matches 43 44 def raw_output_tag_canonical(+key: List<&2, U32>, 45 +nonce: List<&2, U32>, +aad: List<&2, U32>, 46 +plaintext: List<&2, U32>) -> 47 {CoreTagProof.output_tag(Core.gcm_encrypt_raw(key, nonce, aad, 48 plaintext)) == Core.gcm_tag_bytes(Core.gcm_tag_output( 49 Core.aes256_expand(key), nonce, aad, 50 CoreTagProof.output_ciphertext(Core.gcm_encrypt_raw(key, nonce, 51 aad, plaintext)))) : List<&2, U32>}: 52 +output = Core.gcm_encrypt_raw(key, nonce, aad, plaintext) 53 +context = output_tag_context(output) 54 +expected_context = {TagContext{Core.aes256_expand(key), nonce, aad, 55 CoreTagProof.output_ciphertext(output)} : TagContext} 56 context_eq: {context == expected_context : TagContext} = {==} 57 Equal.trans(List<&2, U32>, CoreTagProof.output_tag(output), 58 tag_for_context(context), tag_for_context(expected_context), 59 output_tag_matches_context(output), 60 Equal.cong(TagContext, List<&2, U32>, tag_for_context, 61 context, expected_context, context_eq)) 62 63 def result_tag_bytes(fallback: List<&2, U32>, 64 result: Result<&2, &2, AES.Error, AES.Envelope>) -> List<&2, U32>: 65 match result: 66 case Fail{error}: fallback 67 case Done{envelope}: AES.tag_bytes(AES.envelope_tag(envelope)) 68 69 def valid_output_ciphertext_length(+key: AES.SecretKey, 70 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>) -> 71 {List.length(&2, U32, 72 AES.ciphertext(AES.envelope_from_gcm_checked(nonce, 73 AES.encrypt_valid_output(key, nonce, aad, plaintext)))) == 74 List.length(&2, U32, plaintext) : Nat}: 75 ZipLengthProof.ctr_encrypt_ciphertext_length( 76 Core.aes256_expand(AES.secret_key_bytes(key)), 77 AES.raw_nonce_bytes(nonce), plaintext) 78 79 def encrypt_checked_with_flags(+key: AES.SecretKey, +nonce: AES.Nonce, 80 +aad: List<&2, U32>, +plaintext: List<&2, U32>, 81 +aad_flag: Bool, +plaintext_flag: Bool, 82 aad_ok: {AES.aad_valid(aad) == aad_flag : Bool}, 83 plaintext_ok: {AES.plaintext_valid(plaintext) == plaintext_flag : Bool}, 84 +envelope: AES.Envelope, 85 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 86 Result<&2, &2, AES.Error, AES.Envelope>}) -> 87 {AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag, 88 plaintext_flag) == Done{envelope} : 89 Result<&2, &2, AES.Error, AES.Envelope>}: 90 changed_flags = Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>, 91 AES.encrypt(key, nonce, aad, plaintext), 92 AES.encrypt_checked(key, nonce, aad, plaintext, 93 AES.aad_valid(aad), AES.plaintext_valid(plaintext)), 94 AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag, 95 plaintext_flag), {==}, 96 Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>, 97 AES.encrypt_checked(key, nonce, aad, plaintext, 98 AES.aad_valid(aad), AES.plaintext_valid(plaintext)), 99 AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag, 100 AES.plaintext_valid(plaintext)), 101 AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag, 102 plaintext_flag), 103 Equal.cong(Bool, Result<&2, &2, AES.Error, AES.Envelope>, 104 flag => AES.encrypt_checked(key, nonce, aad, plaintext, 105 flag, AES.plaintext_valid(plaintext)), 106 AES.aad_valid(aad), aad_flag, aad_ok), 107 Equal.cong(Bool, Result<&2, &2, AES.Error, AES.Envelope>, 108 flag => AES.encrypt_checked(key, nonce, aad, plaintext, 109 aad_flag, flag), 110 AES.plaintext_valid(plaintext), plaintext_flag, 111 plaintext_ok))) 112 Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>, 113 AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag, 114 plaintext_flag), 115 AES.encrypt(key, nonce, aad, plaintext), 116 Done{envelope}, 117 Equal.sym(Result<&2, &2, AES.Error, AES.Envelope>, 118 AES.encrypt(key, nonce, aad, plaintext), 119 AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag, 120 plaintext_flag), changed_flags), 121 encrypted) 122 123 def successful_encrypt_aad_valid(+key: AES.SecretKey, 124 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>, 125 +aad_flag: Bool, +plaintext_flag: Bool, 126 aad_ok: {AES.aad_valid(aad) == aad_flag : Bool}, 127 plaintext_ok: {AES.plaintext_valid(plaintext) == plaintext_flag : Bool}, 128 +envelope: AES.Envelope, 129 encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 130 Result<&2, &2, AES.Error, AES.Envelope>}) -> 131 {aad_flag == True{} : Bool}: 132 match aad_flag: 133 case True{}: {==} 134 case False{}: 135 checked = encrypt_checked_with_flags(key, nonce, aad, plaintext, 136 aad_flag, plaintext_flag, aad_ok, plaintext_ok, envelope, 137 encrypted) 138 Equal.trans(Bool, False{}, 139 Result.is_done(&2, &2, AES.Error, AES.Envelope, 140 AES.encrypt_checked(key, nonce, aad, plaintext, 141 aad_flag, plaintext_flag)), 142 True{}, {==}, 143 Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, Bool, 144 result => Result.is_done(&2, &2, AES.Error, AES.Envelope, 145 result), 146 AES.encrypt_checked(key, nonce, aad, plaintext, 147 aad_flag, plaintext_flag), Done{envelope}, checked)) 148 149 def successful_encrypt_plaintext_valid(+key: AES.SecretKey, 150 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>, 151 +aad_flag: Bool, +plaintext_flag: Bool, 152 aad_ok: {AES.aad_valid(aad) == aad_flag : Bool}, 153 plaintext_ok: {AES.plaintext_valid(plaintext) == plaintext_flag : Bool}, 154 +envelope: AES.Envelope, 155 encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 156 Result<&2, &2, AES.Error, AES.Envelope>}) -> 157 {plaintext_flag == True{} : Bool}: 158 match aad_flag plaintext_flag: 159 case True{} True{}: {==} 160 case True{} False{}: 161 checked = encrypt_checked_with_flags(key, nonce, aad, plaintext, 162 aad_flag, plaintext_flag, aad_ok, plaintext_ok, envelope, 163 encrypted) 164 Equal.trans(Bool, False{}, 165 Result.is_done(&2, &2, AES.Error, AES.Envelope, 166 AES.encrypt_checked(key, nonce, aad, plaintext, 167 aad_flag, plaintext_flag)), 168 True{}, {==}, 169 Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, Bool, 170 result => Result.is_done(&2, &2, AES.Error, AES.Envelope, 171 result), 172 AES.encrypt_checked(key, nonce, aad, plaintext, 173 aad_flag, plaintext_flag), Done{envelope}, checked)) 174 case False{} _: 175 checked = encrypt_checked_with_flags(key, nonce, aad, plaintext, 176 aad_flag, plaintext_flag, aad_ok, plaintext_ok, envelope, 177 encrypted) 178 Empty.absurd({plaintext_flag == True{} : Bool}, 179 ZipLengthProof.false_true(Equal.trans(Bool, False{}, 180 Result.is_done(&2, &2, AES.Error, AES.Envelope, 181 AES.encrypt_checked(key, nonce, aad, plaintext, 182 aad_flag, plaintext_flag)), 183 True{}, {==}, 184 Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, Bool, 185 result => Result.is_done(&2, &2, AES.Error, AES.Envelope, 186 result), 187 AES.encrypt_checked(key, nonce, aad, plaintext, 188 aad_flag, plaintext_flag), Done{envelope}, checked)))) 189 190 def result_ciphertext_length( 191 result: Result<&2, &2, AES.Error, AES.Envelope>) -> Nat: 192 match result: 193 case Fail{error}: 0n 194 case Done{envelope}: 195 List.length(&2, U32, AES.ciphertext(envelope)) 196 197 def successful_encrypt_preserves_length(+key: AES.SecretKey, 198 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>, 199 +envelope: AES.Envelope, 200 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 201 Result<&2, &2, AES.Error, AES.Envelope>}) -> 202 {List.length(&2, U32, AES.ciphertext(envelope)) == 203 List.length(&2, U32, plaintext) : Nat}: 204 +aad_flag = AES.aad_valid(aad) 205 +plaintext_flag = AES.plaintext_valid(plaintext) 206 aad_is_true = successful_encrypt_aad_valid(key, nonce, aad, plaintext, 207 aad_flag, plaintext_flag, {==}, {==}, envelope, encrypted) 208 plaintext_is_true = successful_encrypt_plaintext_valid(key, nonce, 209 aad, plaintext, aad_flag, plaintext_flag, {==}, {==}, 210 envelope, encrypted) 211 checked = encrypt_checked_with_flags(key, nonce, aad, plaintext, 212 True{}, True{}, aad_is_true, plaintext_is_true, envelope, encrypted) 213 output_length = valid_output_ciphertext_length(key, nonce, aad, plaintext) 214 Equal.trans(Nat, 215 List.length(&2, U32, AES.ciphertext(envelope)), 216 result_ciphertext_length( 217 AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{})), 218 List.length(&2, U32, plaintext), 219 Equal.sym(Nat, 220 result_ciphertext_length( 221 AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{})), 222 result_ciphertext_length(Done{envelope}), 223 Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, Nat, 224 result => result_ciphertext_length(result), 225 AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{}), 226 Done{envelope}, checked)), 227 output_length) 228 229 def successful_encrypt_ciphertext_matches_gcm(+key: AES.SecretKey, 230 +nonce: AES.Nonce, +aad: List<&2, U32>, 231 +plaintext: List<&2, U32>, +envelope: AES.Envelope, 232 aad_valid: {AES.aad_valid(aad) == True{} : Bool}, 233 plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool}, 234 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 235 Result<&2, &2, AES.Error, AES.Envelope>}) -> 236 {AES.ciphertext(envelope) == 237 CoreTagProof.output_ciphertext(AES.encrypt_valid_output(key, nonce, 238 aad, plaintext)) : List<&2, U32>}: 239 checked = encrypt_checked_with_flags(key, nonce, aad, plaintext, 240 True{}, True{}, aad_valid, plaintext_valid, envelope, encrypted) 241 +output = AES.encrypt_valid_output(key, nonce, aad, plaintext) 242 constructed_matches = Equal.cong( 243 Result<&2, &2, AES.Error, AES.Envelope>, List<&2, U32>, 244 result => result_ciphertext(AES.ciphertext(envelope), result), 245 AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{}), 246 Done{envelope}, checked) 247 Equal.trans(List<&2, U32>, 248 AES.ciphertext(envelope), 249 AES.ciphertext(AES.envelope_from_gcm_checked(nonce, output)), 250 CoreTagProof.output_ciphertext(output), 251 Equal.sym(List<&2, U32>, 252 AES.ciphertext(AES.envelope_from_gcm_checked(nonce, output)), 253 AES.ciphertext(envelope), constructed_matches), 254 CoreTagProof.envelope_gcm_ciphertext(nonce, output)) 255 256 def successful_encrypt_tag_matches_gcm(+key: AES.SecretKey, 257 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>, 258 +envelope: AES.Envelope, 259 aad_ok: {AES.aad_valid(aad) == True{} : Bool}, 260 plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}, 261 encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 262 Result<&2, &2, AES.Error, AES.Envelope>}) -> 263 {AES.tag_bytes(AES.envelope_tag(envelope)) == 264 CoreTagProof.output_tag(AES.encrypt_valid_output(key, nonce, aad, 265 plaintext)) : List<&2, U32>}: 266 checked = encrypt_checked_with_flags(key, nonce, aad, plaintext, 267 True{}, True{}, aad_ok, plaintext_ok, envelope, encrypted) 268 +output = AES.encrypt_valid_output(key, nonce, aad, plaintext) 269 constructed_matches = Equal.cong( 270 Result<&2, &2, AES.Error, AES.Envelope>, List<&2, U32>, 271 result => result_tag_bytes([], result), 272 AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{}), 273 Done{envelope}, checked) 274 Equal.trans(List<&2, U32>, AES.tag_bytes(AES.envelope_tag(envelope)), 275 AES.tag_bytes(AES.envelope_tag(AES.envelope_from_gcm_checked(nonce, 276 output))), CoreTagProof.output_tag(output), 277 Equal.sym(List<&2, U32>, 278 AES.tag_bytes(AES.envelope_tag(AES.envelope_from_gcm_checked( 279 nonce, output))), AES.tag_bytes(AES.envelope_tag(envelope)), 280 constructed_matches), CoreTagProof.envelope_gcm_tag(nonce, output)) 281 282 def successful_encrypt_tag_canonical(+key: AES.SecretKey, 283 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>, 284 +envelope: AES.Envelope, 285 +aad_ok: {AES.aad_valid(aad) == True{} : Bool}, 286 +plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}, 287 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 288 Result<&2, &2, AES.Error, AES.Envelope>}) -> 289 {AES.tag_bytes(AES.envelope_tag(envelope)) == Core.gcm_tag_bytes( 290 Core.gcm_tag_output(Core.aes256_expand(AES.secret_key_bytes(key)), 291 AES.raw_nonce_bytes(nonce), aad, AES.ciphertext(envelope))) : 292 List<&2, U32>}: 293 +output = AES.encrypt_valid_output(key, nonce, aad, plaintext) 294 tag_matches = successful_encrypt_tag_matches_gcm(key, nonce, aad, 295 plaintext, envelope, aad_ok, plaintext_ok, encrypted) 296 ciphertext_matches = successful_encrypt_ciphertext_matches_gcm(key, 297 nonce, aad, plaintext, envelope, aad_ok, plaintext_ok, encrypted) 298 raw_canonical = raw_output_tag_canonical(AES.secret_key_bytes(key), 299 AES.raw_nonce_bytes(nonce), aad, plaintext) 300 current_ciphertext = Equal.cong(List<&2, U32>, List<&2, U32>, 301 value => Core.gcm_tag_bytes(Core.gcm_tag_output( 302 Core.aes256_expand(AES.secret_key_bytes(key)), 303 AES.raw_nonce_bytes(nonce), aad, value)), 304 CoreTagProof.output_ciphertext(output), AES.ciphertext(envelope), 305 Equal.sym(List<&2, U32>, AES.ciphertext(envelope), 306 CoreTagProof.output_ciphertext(output), ciphertext_matches)) 307 Equal.trans(List<&2, U32>, AES.tag_bytes(AES.envelope_tag(envelope)), 308 CoreTagProof.output_tag(output), 309 Core.gcm_tag_bytes(Core.gcm_tag_output( 310 Core.aes256_expand(AES.secret_key_bytes(key)), 311 AES.raw_nonce_bytes(nonce), aad, AES.ciphertext(envelope))), 312 tag_matches, 313 Equal.trans(List<&2, U32>, CoreTagProof.output_tag(output), 314 Core.gcm_tag_bytes(Core.gcm_tag_output( 315 Core.aes256_expand(AES.secret_key_bytes(key)), 316 AES.raw_nonce_bytes(nonce), aad, 317 CoreTagProof.output_ciphertext(output))), 318 Core.gcm_tag_bytes(Core.gcm_tag_output( 319 Core.aes256_expand(AES.secret_key_bytes(key)), 320 AES.raw_nonce_bytes(nonce), aad, AES.ciphertext(envelope))), 321 raw_canonical, current_ciphertext)) 322 323 def successful_encrypt_ciphertext_matches_ctr(+key: AES.SecretKey, 324 +nonce: AES.Nonce, +aad: List<&2, U32>, 325 +plaintext: List<&2, U32>, +envelope: AES.Envelope, 326 aad_valid: {AES.aad_valid(aad) == True{} : Bool}, 327 plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool}, 328 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 329 Result<&2, &2, AES.Error, AES.Envelope>}) -> 330 {AES.ciphertext(envelope) == 331 Core.gcm_zip_xor(plaintext, 332 Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext), 333 Core.aes256_expand(AES.secret_key_bytes(key)), 334 Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(nonce))))) : 335 List<&2, U32>}: 336 Equal.trans(List<&2, U32>, 337 AES.ciphertext(envelope), 338 CoreTagProof.output_ciphertext(AES.encrypt_valid_output(key, nonce, 339 aad, plaintext)), 340 Core.gcm_zip_xor(plaintext, 341 Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext), 342 Core.aes256_expand(AES.secret_key_bytes(key)), 343 Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(nonce))))), 344 successful_encrypt_ciphertext_matches_gcm(key, nonce, aad, 345 plaintext, envelope, aad_valid, plaintext_valid, encrypted), 346 CoreTagProof.raw_encrypt_output_ciphertext( 347 AES.secret_key_bytes(key), AES.raw_nonce_bytes(nonce), aad, 348 plaintext)) 349 350 def successful_encrypt_ciphertext_valid(+key: AES.SecretKey, 351 +nonce: AES.Nonce, +aad: List<&2, U32>, 352 +plaintext: List<&2, U32>, +envelope: AES.Envelope, 353 aad_valid: {AES.aad_valid(aad) == True{} : Bool}, 354 plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool}, 355 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 356 Result<&2, &2, AES.Error, AES.Envelope>}) -> 357 {AES.plaintext_valid(AES.ciphertext(envelope)) == True{} : Bool}: 358 length_eq = successful_encrypt_preserves_length(key, nonce, aad, 359 plaintext, envelope, encrypted) 360 LengthLimitProof.plaintext_valid_same_length( 361 AES.ciphertext(envelope), plaintext, 362 AES.envelope_ciphertext_valid(envelope), plaintext_valid, length_eq) 363 364 def successful_encrypt_ctr_decrypts(+key: AES.SecretKey, 365 +nonce: AES.Nonce, +aad: List<&2, U32>, 366 +plaintext: List<&2, U32>, +envelope: AES.Envelope, 367 aad_valid: {AES.aad_valid(aad) == True{} : Bool}, 368 +plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool}, 369 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 370 Result<&2, &2, AES.Error, AES.Envelope>}) -> 371 {Core.gcm_decrypt_raw(AES.secret_key_bytes(key), 372 AES.raw_nonce_bytes(nonce), AES.ciphertext(envelope)) == 373 plaintext : List<&2, U32>}: 374 +words = Core.aes256_expand(AES.secret_key_bytes(key)) 375 aes_bytes_valid = MaskedXorProof.bool_and_true_left( 376 AES.bytes_valid(plaintext), 377 AES.bytes_length_limit(plaintext, 4294967264, 15), plaintext_valid) 378 core_bytes_valid = Equal.trans(Bool, 379 Core.gcm_bytes_valid(plaintext), AES.bytes_valid(plaintext), True{}, 380 Equal.sym(Bool, AES.bytes_valid(plaintext), 381 Core.gcm_bytes_valid(plaintext), 382 AES.core_bytes_valid_eq(plaintext)), aes_bytes_valid) 383 cipher = successful_encrypt_ciphertext_matches_ctr(key, nonce, aad, 384 plaintext, envelope, aad_valid, plaintext_valid, encrypted) 385 Equal.trans(List<&2, U32>, 386 Core.gcm_decrypt_raw(AES.secret_key_bytes(key), 387 AES.raw_nonce_bytes(nonce), AES.ciphertext(envelope)), 388 Core.gcm_decrypt_raw(AES.secret_key_bytes(key), 389 AES.raw_nonce_bytes(nonce), 390 Core.gcm_zip_xor(plaintext, 391 Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext), 392 words, Core.gcm_inc32(Core.gcm_j0( 393 AES.raw_nonce_bytes(nonce)))))), 394 plaintext, 395 Equal.cong(List<&2, U32>, List<&2, U32>, 396 ciphertext => Core.gcm_decrypt_raw(AES.secret_key_bytes(key), 397 AES.raw_nonce_bytes(nonce), ciphertext), 398 AES.ciphertext(envelope), 399 Core.gcm_zip_xor(plaintext, 400 Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext), 401 words, Core.gcm_inc32(Core.gcm_j0( 402 AES.raw_nonce_bytes(nonce))))), cipher), 403 MaskedXorProof.ctr_decrypt_ciphertext_roundtrip(words, 404 AES.raw_nonce_bytes(nonce), plaintext, core_bytes_valid)) 405 406 def result_nonce(fallback: AES.Nonce, 407 result: Result<&2, &2, AES.Error, AES.Envelope>) -> AES.Nonce: 408 match result: 409 case Fail{error}: fallback 410 case Done{envelope}: AES.envelope_nonce(envelope) 411 412 def output_nonce(+nonce: AES.Nonce, +output: Core.GcmOutput) -> 413 {result_nonce(nonce, AES.encrypt_output_from_gcm(nonce, output)) == 414 nonce : AES.Nonce}: 415 match output: 416 case Core.GcmOutput{+ciphertext, ciphertext_valid, 417 tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad, 418 tag_matches}: 419 {==} 420 421 def valid_nonce(key: AES.SecretKey, +nonce: AES.Nonce, 422 aad: List<&2, U32>, plaintext: List<&2, U32>) -> 423 {result_nonce(nonce, AES.encrypt_valid(key, nonce, aad, plaintext)) == 424 nonce : AES.Nonce}: 425 output_nonce(nonce, 426 AES.encrypt_valid_output(key, nonce, aad, plaintext)) 427 428 def checked_nonce(key: AES.SecretKey, +nonce: AES.Nonce, 429 +aad: List<&2, U32>, +plaintext: List<&2, U32>, 430 aad_ok: Bool, plaintext_ok: Bool) -> 431 {result_nonce(nonce, AES.encrypt_checked(key, nonce, aad, plaintext, 432 aad_ok, plaintext_ok)) == nonce : AES.Nonce}: 433 match aad_ok plaintext_ok: 434 case True{} True{}: valid_nonce(key, nonce, aad, plaintext) 435 case False{} _: {==} 436 case True{} False{}: {==} 437 438 def encrypt_nonce(key: AES.SecretKey, +nonce: AES.Nonce, 439 +aad: List<&2, U32>, +plaintext: List<&2, U32>) -> 440 {result_nonce(nonce, AES.encrypt(key, nonce, aad, plaintext)) == 441 nonce : AES.Nonce}: 442 checked_nonce(key, nonce, aad, plaintext, 443 AES.aad_valid(aad), AES.plaintext_valid(plaintext)) 444 445 def preserves_nonce(+key: AES.SecretKey, +nonce: AES.Nonce, 446 +aad: List<&2, U32>, +plaintext: List<&2, U32>, 447 +envelope: AES.Envelope, 448 encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 449 Result<&2, &2, AES.Error, AES.Envelope>}) -> 450 {AES.envelope_nonce(envelope) == nonce : AES.Nonce}: 451 Equal.trans(AES.Nonce, 452 result_nonce(nonce, Done{envelope}), 453 result_nonce(nonce, AES.encrypt(key, nonce, aad, plaintext)), 454 nonce, 455 Equal.sym(AES.Nonce, 456 result_nonce(nonce, AES.encrypt(key, nonce, aad, plaintext)), 457 result_nonce(nonce, Done{envelope}), 458 Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, AES.Nonce, 459 result => result_nonce(nonce, result), 460 AES.encrypt(key, nonce, aad, plaintext), Done{envelope}, 461 encrypted)), 462 encrypt_nonce(key, nonce, aad, plaintext)) 463 464 def successful_encrypt_envelope_tag_canonical(+key: AES.SecretKey, 465 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>, 466 +envelope: AES.Envelope, 467 aad_ok: {AES.aad_valid(aad) == True{} : Bool}, 468 plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}, 469 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 470 Result<&2, &2, AES.Error, AES.Envelope>}) -> 471 {AES.tag_bytes(AES.envelope_tag(envelope)) == Core.gcm_tag_bytes( 472 Core.gcm_tag_output(Core.aes256_expand(AES.secret_key_bytes(key)), 473 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), aad, 474 AES.ciphertext(envelope))) : List<&2, U32>}: 475 canonical = successful_encrypt_tag_canonical(key, nonce, aad, plaintext, 476 envelope, aad_ok, plaintext_ok, encrypted) 477 nonce_matches = Equal.cong(AES.Nonce, List<&2, U32>, 478 AES.raw_nonce_bytes, AES.envelope_nonce(envelope), nonce, 479 preserves_nonce(key, nonce, aad, plaintext, envelope, encrypted)) 480 nonce_rewrite = Equal.cong(List<&2, U32>, List<&2, U32>, 481 value => Core.gcm_tag_bytes(Core.gcm_tag_output( 482 Core.aes256_expand(AES.secret_key_bytes(key)), value, aad, 483 AES.ciphertext(envelope))), AES.raw_nonce_bytes(nonce), 484 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), 485 Equal.sym(List<&2, U32>, 486 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), 487 AES.raw_nonce_bytes(nonce), nonce_matches)) 488 Equal.trans(List<&2, U32>, AES.tag_bytes(AES.envelope_tag(envelope)), 489 Core.gcm_tag_bytes(Core.gcm_tag_output( 490 Core.aes256_expand(AES.secret_key_bytes(key)), 491 AES.raw_nonce_bytes(nonce), aad, AES.ciphertext(envelope))), 492 Core.gcm_tag_bytes(Core.gcm_tag_output( 493 Core.aes256_expand(AES.secret_key_bytes(key)), 494 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), aad, 495 AES.ciphertext(envelope))), canonical, nonce_rewrite) 496 497 def decrypt_auth_tag_canonical(+words: List<&2, U32>, 498 +nonce: List<&2, U32>, +aad: List<&2, U32>, 499 +ciphertext: List<&2, U32>, +envelope: AES.Envelope, +tag: AES.Tag, 500 canonical: {AES.tag_bytes(tag) == Core.gcm_tag_bytes( 501 Core.gcm_tag_output(words, nonce, aad, ciphertext)) : List<&2, U32>}) -> 502 {AES.decrypt_authenticated_tag(words, nonce, aad, ciphertext, envelope, 503 tag) == AES.decrypt_auth_result(words, envelope, True{}) : 504 Result<&2, &2, AES.Error, List<&2, U32>>}: 505 match tag: 506 case AES.Tag{bytes, size, valid}: 507 Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>, 508 ok => AES.decrypt_auth_result(words, envelope, ok), 509 AES.bytes_equal_full_scan(bytes, Core.gcm_tag_bytes( 510 Core.gcm_tag_output(words, nonce, aad, ciphertext))), 511 True{}, TagCompareProof.equal_of_equal(bytes, 512 Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, 513 aad, ciphertext)), canonical)) 514 515 def successful_encrypt_decrypt_authenticated(+key: AES.SecretKey, 516 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>, 517 +envelope: AES.Envelope, 518 +aad_ok: {AES.aad_valid(aad) == True{} : Bool}, 519 +plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}, 520 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 521 Result<&2, &2, AES.Error, AES.Envelope>}) -> 522 {AES.decrypt_authenticated(key, aad, envelope) == Done{plaintext} : 523 Result<&2, &2, AES.Error, List<&2, U32>>}: 524 match key envelope: 525 case AES.SecretKey{+key_bytes, _, _} 526 AES.Envelope{envelope_nonce, ciphertext, tag, _}: 527 +words = Core.aes256_expand(key_bytes) 528 +nonce_bytes = AES.raw_nonce_bytes(envelope_nonce) 529 canonical = successful_encrypt_envelope_tag_canonical(key, 530 nonce, aad, plaintext, envelope, aad_ok, plaintext_ok, 531 encrypted) 532 authenticated = decrypt_auth_tag_canonical(words, nonce_bytes, 533 aad, ciphertext, envelope, tag, canonical) 534 nonce_matches = Equal.cong(AES.Nonce, List<&2, U32>, 535 AES.raw_nonce_bytes, envelope_nonce, nonce, 536 preserves_nonce(key, nonce, aad, plaintext, envelope, 537 encrypted)) 538 ctr_roundtrip = successful_encrypt_ctr_decrypts(key, nonce, aad, 539 plaintext, envelope, aad_ok, plaintext_ok, encrypted) 540 expanded_nonce = Equal.cong(List<&2, U32>, List<&2, U32>, 541 value => Core.gcm_decrypt_expanded(words, value, ciphertext), 542 nonce_bytes, AES.raw_nonce_bytes(nonce), nonce_matches) 543 expanded_to_raw = Equal.trans(List<&2, U32>, 544 Core.gcm_decrypt_expanded(words, nonce_bytes, ciphertext), 545 Core.gcm_decrypt_expanded(words, AES.raw_nonce_bytes(nonce), 546 ciphertext), 547 Core.gcm_decrypt_raw(AES.secret_key_bytes(key), 548 AES.raw_nonce_bytes(nonce), ciphertext), 549 expanded_nonce, {==}) 550 expanded_roundtrip = Equal.trans(List<&2, U32>, 551 Core.gcm_decrypt_expanded(words, nonce_bytes, ciphertext), 552 Core.gcm_decrypt_raw(AES.secret_key_bytes(key), 553 AES.raw_nonce_bytes(nonce), ciphertext), plaintext, 554 expanded_to_raw, ctr_roundtrip) 555 payload = Equal.cong(List<&2, U32>, 556 Result<&2, &2, AES.Error, List<&2, U32>>, 557 value => Done{value}, 558 Core.gcm_decrypt_expanded(words, nonce_bytes, ciphertext), 559 plaintext, expanded_roundtrip) 560 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>, 561 AES.decrypt_authenticated(key, aad, envelope), 562 AES.decrypt_auth_result(words, envelope, True{}), 563 Done{plaintext}, authenticated, payload) 564 565 def successful_encrypt_decrypt_roundtrip(+key: AES.SecretKey, 566 +nonce: AES.Nonce, +aad: List<&2, U32>, 567 +plaintext: List<&2, U32>, +envelope: AES.Envelope, 568 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} : 569 Result<&2, &2, AES.Error, AES.Envelope>}) -> 570 {AES.decrypt(key, aad, envelope) == Done{plaintext} : 571 Result<&2, &2, AES.Error, List<&2, U32>>}: 572 +aad_ok = successful_encrypt_aad_valid(key, nonce, aad, plaintext, 573 AES.aad_valid(aad), AES.plaintext_valid(plaintext), {==}, {==}, 574 envelope, encrypted) 575 +plaintext_ok = successful_encrypt_plaintext_valid(key, nonce, aad, 576 plaintext, AES.aad_valid(aad), AES.plaintext_valid(plaintext), 577 {==}, {==}, envelope, encrypted) 578 ciphertext_ok = successful_encrypt_ciphertext_valid(key, nonce, aad, 579 plaintext, envelope, aad_ok, plaintext_ok, encrypted) 580 authenticated = successful_encrypt_decrypt_authenticated(key, nonce, 581 aad, plaintext, envelope, aad_ok, plaintext_ok, encrypted) 582 aad_checked = Equal.cong(Bool, 583 Result<&2, &2, AES.Error, List<&2, U32>>, 584 flag => AES.decrypt_checked(key, aad, envelope, flag, 585 AES.plaintext_valid(AES.ciphertext(envelope))), 586 AES.aad_valid(aad), True{}, aad_ok) 587 ciphertext_checked = Equal.cong(Bool, 588 Result<&2, &2, AES.Error, List<&2, U32>>, 589 flag => AES.decrypt_checked(key, aad, envelope, True{}, flag), 590 AES.plaintext_valid(AES.ciphertext(envelope)), True{}, ciphertext_ok) 591 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>, 592 AES.decrypt(key, aad, envelope), 593 AES.decrypt_checked(key, aad, envelope, True{}, True{}), 594 Done{plaintext}, 595 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>, 596 AES.decrypt(key, aad, envelope), 597 AES.decrypt_checked(key, aad, envelope, 598 AES.aad_valid(aad), 599 AES.plaintext_valid(AES.ciphertext(envelope))), 600 AES.decrypt_checked(key, aad, envelope, True{}, True{}), 601 {==}, 602 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>, 603 AES.decrypt_checked(key, aad, envelope, 604 AES.aad_valid(aad), 605 AES.plaintext_valid(AES.ciphertext(envelope))), 606 AES.decrypt_checked(key, aad, envelope, True{}, 607 AES.plaintext_valid(AES.ciphertext(envelope))), 608 AES.decrypt_checked(key, aad, envelope, True{}, True{}), 609 aad_checked, ciphertext_checked)), 610 authenticated) 611 612 def output_is_done(+nonce: AES.Nonce, +output: Core.GcmOutput) -> 613 {Result.is_done(&2, &2, AES.Error, AES.Envelope, 614 AES.encrypt_output_from_gcm(nonce, output)) == True{} : Bool}: 615 {==} 616 617 def valid_is_done(key: AES.SecretKey, +nonce: AES.Nonce, 618 aad: List<&2, U32>, plaintext: List<&2, U32>) -> 619 {Result.is_done(&2, &2, AES.Error, AES.Envelope, 620 AES.encrypt_valid(key, nonce, aad, plaintext)) == True{} : Bool}: 621 output_is_done(nonce, 622 AES.encrypt_valid_output(key, nonce, aad, plaintext)) 623 624 def valid_input_is_done(+key: AES.SecretKey, +nonce: AES.Nonce, 625 +aad: List<&2, U32>, +plaintext: List<&2, U32>, 626 aad_ok: {AES.aad_valid(aad) == True{} : Bool}, 627 plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}) -> 628 {Result.is_done(&2, &2, AES.Error, AES.Envelope, 629 AES.encrypt(key, nonce, aad, plaintext)) == True{} : Bool}: 630 Equal.trans(Bool, 631 Result.is_done(&2, &2, AES.Error, AES.Envelope, 632 AES.encrypt(key, nonce, aad, plaintext)), 633 Result.is_done(&2, &2, AES.Error, AES.Envelope, 634 AES.encrypt_checked(key, nonce, aad, plaintext, 635 True{}, AES.plaintext_valid(plaintext))), 636 True{}, 637 Equal.cong(Bool, Bool, 638 b => Result.is_done(&2, &2, AES.Error, AES.Envelope, 639 AES.encrypt_checked(key, nonce, aad, plaintext, 640 b, AES.plaintext_valid(plaintext))), 641 AES.aad_valid(aad), True{}, aad_ok), 642 Equal.trans(Bool, 643 Result.is_done(&2, &2, AES.Error, AES.Envelope, 644 AES.encrypt_checked(key, nonce, aad, plaintext, 645 True{}, AES.plaintext_valid(plaintext))), 646 Result.is_done(&2, &2, AES.Error, AES.Envelope, 647 AES.encrypt_valid(key, nonce, aad, plaintext)), 648 True{}, 649 Equal.cong(Bool, Bool, 650 b => Result.is_done(&2, &2, AES.Error, AES.Envelope, 651 AES.encrypt_checked(key, nonce, aad, plaintext, 652 True{}, b)), 653 AES.plaintext_valid(plaintext), True{}, plaintext_ok), 654 valid_is_done(key, nonce, aad, plaintext)))