1 import Base 2 import ./AES256GCMCore.bend as Core 3 4 # AES-256-GCM with validated inputs and canonical envelope serialization. 5 # Bytes use U32 storage, with validation certificates excluding values above 255. 6 def bytes_valid(bytes: List<&2, U32>) -> Bool: 7 match bytes: 8 case Nil{}: True{} 9 case head <> tail: 10 U32.is_lt(head, 256) && bytes_valid(tail) 11 12 def core_bytes_valid_eq(+bytes: List<&2, U32>) -> 13 {bytes_valid(bytes) == Core.gcm_bytes_valid(bytes) : Bool}: 14 match bytes: 15 case Nil{}: {==} 16 case head <> tail: 17 recursive = core_bytes_valid_eq(tail) 18 Equal.cong(Bool, Bool, 19 valid => Bool.and(U32.is_lt(head, 256), valid), 20 bytes_valid(tail), Core.gcm_bytes_valid(tail), recursive) 21 22 def core_bytes_valid_proof(bytes: List<&2, U32>, 23 valid: {Core.gcm_bytes_valid(bytes) == True{} : Bool}) -> 24 {bytes_valid(bytes) == True{} : Bool}: 25 Equal.trans(Bool, bytes_valid(bytes), Core.gcm_bytes_valid(bytes), True{}, 26 core_bytes_valid_eq(bytes), valid) 27 28 # Count at most the supported byte bound with two wrapping words. This avoids 29 # constructing or dividing enormous Peano Nat bounds for symbolic lists. 30 31 def length_pair_high(low: U32, high_cmp: Cmp, max_low: U32) -> Bool: 32 match high_cmp: 33 case LT{}: True{} 34 case EQ{}: U32.is_le(low, max_low) 35 case GT{}: False{} 36 37 def length_pair_within(low: U32, high: U32, max_low: U32, max_high: U32) -> Bool: 38 length_pair_high(low, U32.cmp(high, max_high), max_low) 39 40 def bytes_length_limit.go(fuel: Nat, bytes: List<&2, U32>, 41 low: U32, +high: U32, +max_low: U32, +max_high: U32, 42 within: Bool) -> Bool: 43 match fuel bytes within: 44 case 0n Nil{} _: within 45 case 0n _ <> _ _: False{} 46 case 1n+p Nil{} _: False{} 47 case 1n+p _ <> _ False{}: False{} 48 case 1n+p _ <> tail True{}: 49 +next_low = U32.add(low, 1) 50 +next_high = Bool.pick(U32, U32.is_eq(next_low, 0), U32.add(high, 1), high) 51 bytes_length_limit.go(p, tail, next_low, next_high, 52 max_low, max_high, 53 length_pair_within(next_low, next_high, max_low, max_high)) 54 55 def bytes_length_limit(+bytes: List<&2, U32>, max_low: U32, max_high: U32) -> Bool: 56 bytes_length_limit.go(List.length(&2, U32, bytes), bytes, 57 0, 0, max_low, max_high, True{}) 58 59 # GCM limits are expressed in bytes after requiring byte-aligned input. 60 def plaintext_valid(+bytes: List<&2, U32>) -> Bool: 61 bytes_valid(bytes) && bytes_length_limit(bytes, 4294967264, 15) 62 63 def aad_valid(+bytes: List<&2, U32>) -> Bool: 64 bytes_valid(bytes) && bytes_length_limit(bytes, 4294967295, 536870911) 65 66 type SecretKey is Data: 67 SecretKey{ 68 bytes: List<&2, U32>, 69 -size: {List.length(&2, U32, bytes) == 32n : Nat}, 70 -valid: {bytes_valid(bytes) == True{} : Bool} 71 } 72 73 type Nonce is Data: 74 Nonce{ 75 bytes: List<&2, U32>, 76 size: {List.length(&2, U32, bytes) == 12n : Nat}, 77 valid: {bytes_valid(bytes) == True{} : Bool} 78 } 79 80 type Tag is Data: 81 Tag{ 82 bytes: List<&2, U32>, 83 size: {List.length(&2, U32, bytes) == 16n : Nat}, 84 valid: {bytes_valid(bytes) == True{} : Bool} 85 } 86 87 type Envelope is Data: 88 Envelope{ 89 nonce: Nonce, 90 ciphertext: List<&2, U32>, 91 tag: Tag, 92 valid: {bytes_valid(ciphertext) == True{} : Bool} 93 } 94 95 type Error is Data: 96 InvalidKey{} 97 InvalidNonce{} 98 InvalidBytes{} 99 InvalidEnvelope{} 100 AuthenticationFailed{} 101 102 # Constructors validate raw input; SecretKey/Nonce/Tag certificates enforce sizes. 103 law key: 104 for bytes: List<&2, U32> 105 Result<&2, &2, Error, SecretKey> 106 107 law nonce: 108 for bytes: List<&2, U32> 109 Result<&2, &2, Error, Nonce> 110 111 # Deterministic primitive: the caller supplies a nonce unique for this key. 112 # The eventual effectful wrapper must generate nonces using an OS CSPRNG. 113 law encrypt: 114 for key: SecretKey 115 for nonce: Nonce 116 for aad: List<&2, U32> 117 for plaintext: List<&2, U32> 118 Result<&2, &2, Error, Envelope> 119 120 # Fail contains only an Error, never unauthenticated or partial plaintext. 121 law decrypt: 122 for key: SecretKey 123 for aad: List<&2, U32> 124 for envelope: Envelope 125 Result<&2, &2, Error, List<&2, U32>> 126 127 # Canonical envelope: v1.... 128 # The nonce has 24 hex characters, the tag 32, ciphertext an even number (or 0). 129 # AAD is external and must be supplied unchanged when decrypting. 130 law encode: 131 for envelope: Envelope 132 String 133 134 law parse: 135 for text: String 136 Result<&2, &2, Error, Envelope> 137 138 # Read-only projections needed to state the contract. 139 def nonce_bytes(nonce: Nonce) -> List<&2, U32>: 140 match nonce: 141 case Nonce{bytes, size, valid}: bytes 142 143 def tag_bytes(tag: Tag) -> List<&2, U32>: 144 match tag: 145 case Tag{bytes, size, valid}: bytes 146 147 def tag_bytes_size(tag: Tag) -> 148 {List.length(&2, U32, tag_bytes(tag)) == 16n : Nat}: 149 match tag: 150 case Tag{bytes, size, valid}: size 151 152 def tag_bytes_valid(tag: Tag) -> 153 {bytes_valid(tag_bytes(tag)) == True{} : Bool}: 154 match tag: 155 case Tag{bytes, size, valid}: valid 156 157 def ciphertext(envelope: Envelope) -> List<&2, U32>: 158 match envelope: 159 case Envelope{nonce, ciphertext, tag, valid}: ciphertext 160 161 def envelope_ciphertext_valid(envelope: Envelope) -> 162 {bytes_valid(ciphertext(envelope)) == True{} : Bool}: 163 match envelope: 164 case Envelope{nonce, ciphertext, tag, valid}: valid 165 166 def envelope_nonce(envelope: Envelope) -> Nonce: 167 match envelope: 168 case Envelope{nonce, ciphertext, tag, valid}: nonce 169 170 def envelope_tag(envelope: Envelope) -> Tag: 171 match envelope: 172 case Envelope{nonce, ciphertext, tag, valid}: tag 173 174 # Canonical lowercase hexadecimal envelope serialization. 175 def hex_digit_kind(+n: U32, decimal: Bool) -> Char: 176 match decimal: 177 case True{}: Chr{U32.add(48, n)} 178 case False{}: Chr{U32.add(87, n)} 179 180 # The mask-first implementation keeps zero mask bits visibly false to Bend's 181 # checker, which supports the nibble range proofs used by the codec. 182 def hex_word_and(n: Nat, mask: Word(n), +value: Word(n)) -> Word(n): 183 match n: 184 case 0n: WNil{} 185 case 1n+p: 186 match mask: 187 case WCon{False{}, mask_tail}: 188 match value: 189 case WCon{_, value_tail}: 190 WCon{False{}, hex_word_and(p, mask_tail, value_tail)} 191 case WCon{True{}, mask_tail}: 192 match value: 193 case WCon{bit, value_tail}: 194 WCon{bit, hex_word_and(p, mask_tail, value_tail)} 195 196 def hex_mask(value: U32, mask: U32) -> U32: 197 match value mask: 198 case U32{value_word} U32{mask_word}: 199 U32{hex_word_and(32n, mask_word, value_word)} 200 201 def hex_digit.nibble(+n: U32) -> Char: 202 match n: 203 case 0: Chr{48} 204 case 1: Chr{49} 205 case 2: Chr{50} 206 case 3: Chr{51} 207 case 4: Chr{52} 208 case 5: Chr{53} 209 case 6: Chr{54} 210 case 7: Chr{55} 211 case 8: Chr{56} 212 case 9: Chr{57} 213 case 10: Chr{97} 214 case 11: Chr{98} 215 case 12: Chr{99} 216 case 13: Chr{100} 217 case 14: Chr{101} 218 case 15: Chr{102} 219 case _: hex_digit_kind(n, U32.is_lt(n, 10)) 220 221 def hex_digit(+n: U32) -> Char: 222 hex_digit.nibble(hex_mask(n, 15)) 223 224 def hex_bytes(+bytes: List<&2, U32>) -> String: 225 match bytes: 226 case Nil{}: "" 227 case +byte <> tail: 228 +normalized = hex_mask(byte, 255) 229 SCon{hex_digit(U32.shrn(normalized, 4n)), 230 SCon{hex_digit(normalized), hex_bytes(tail)}} 231 232 # Serialize validated fixed-size fields through a fixed-size byte view. This 233 # makes the wire length structural even when the constructor certificate is 234 # erased from runtime storage. 235 def fixed_bytes(n: Nat, bytes: List<&2, U32>) -> List<&2, U32>: 236 match n: 237 case 0n: Nil{} 238 case 1n+p: 239 match bytes: 240 case Nil{}: 0 <> fixed_bytes(p, Nil{}) 241 case byte <> tail: byte <> fixed_bytes(p, tail) 242 243 def encode_impl(envelope: Envelope) -> String: 244 match envelope: 245 case Envelope{nonce, ciphertext, tag, valid}: 246 match nonce: 247 case Nonce{nonce_bytes, size, valid}: 248 "v1." ++ hex_bytes(fixed_bytes(12n, nonce_bytes)) ++ "." ++ 249 hex_bytes(fixed_bytes(16n, tag_bytes(tag))) ++ "." ++ 250 hex_bytes(ciphertext) 251 252 # Match the ASCII code point directly so each accepted nibble normalizes to a literal. 253 def hex_nibble(+code: U32) -> Maybe<&2, U32>: 254 match code: 255 case 48: Some{0} 256 case 49: Some{1} 257 case 50: Some{2} 258 case 51: Some{3} 259 case 52: Some{4} 260 case 53: Some{5} 261 case 54: Some{6} 262 case 55: Some{7} 263 case 56: Some{8} 264 case 57: Some{9} 265 case 97: Some{10} 266 case 98: Some{11} 267 case 99: Some{12} 268 case 100: Some{13} 269 case 101: Some{14} 270 case 102: Some{15} 271 case _: None{} 272 273 def hex_join(high: U32, low: U32) -> U32: 274 match high low: 275 case U32{WCon{h0, WCon{h1, WCon{h2, WCon{h3, _}}}}} 276 U32{WCon{l0, WCon{l1, WCon{l2, WCon{l3, _}}}}}: 277 U32{WCon{l0, WCon{l1, WCon{l2, WCon{l3, 278 WCon{h0, WCon{h1, WCon{h2, WCon{h3, Word.zero(24n)}}}}}}}}} 279 280 def hex_pair.combine(high: Maybe<&2, U32>, low: Maybe<&2, U32>) -> Maybe<&2, U32>: 281 match high low: 282 case None{} _: None{} 283 case Some{high} None{}: None{} 284 case Some{high} Some{low}: Some{hex_join(high, low)} 285 286 def hex_pair(first: Char, second: Char) -> Maybe<&2, U32>: 287 hex_pair.combine(hex_nibble(Char.to_u32(first)), 288 hex_nibble(Char.to_u32(second))) 289 290 def hex_pairs(chars: List<&2, Char>) -> List<&2, Maybe<&2, U32>>: 291 match chars: 292 case Nil{}: Nil{} 293 case first <> Nil{}: [None{}] 294 case first <> second <> tail: 295 hex_pair(first, second) <> hex_pairs(tail) 296 297 def collect_hex.cons(pair: Maybe<&2, U32>, result: Maybe<&2, List<&2, U32>>) -> 298 Maybe<&2, List<&2, U32>>: 299 match pair result: 300 case None{} _: None{} 301 case Some{_} None{}: None{} 302 case Some{byte} Some{bytes}: Some{byte <> bytes} 303 304 def collect_hex(pairs: List<&2, Maybe<&2, U32>>) -> Maybe<&2, List<&2, U32>>: 305 match pairs: 306 case Nil{}: Some{Nil{}} 307 case pair <> tail: collect_hex.cons(pair, collect_hex(tail)) 308 309 def decode_hex(text: String) -> Maybe<&2, List<&2, U32>>: 310 collect_hex(hex_pairs(String.to_list(text))) 311 312 def aes_nat_eq_step(+a: Nat, +b: Nat, 313 result: Maybe<&0, {a == b : Nat}>) -> Maybe<&0, {1n+a == 1n+b : Nat}>: 314 match result: 315 case None{}: None{} 316 case Some{proof}: Some{Equal.cong(Nat, Nat, n => 1n+n, a, b, proof)} 317 318 def aes_nat_eq_proof(+a: Nat, +b: Nat) -> Maybe<&0, {a == b : Nat}>: 319 match a b: 320 case 0n 0n: Some{{==}} 321 case 0n 1n+p: None{} 322 case 1n+p 0n: None{} 323 case 1n+pa 1n+pb: aes_nat_eq_step(pa, pb, aes_nat_eq_proof(pa, pb)) 324 325 def aes_bool_true_proof(+x: U32, b: Bool, 326 link: {b == U32.is_lt(x, 256) : Bool}) -> Maybe<&0, {U32.is_lt(x, 256) == True{} : Bool}>: 327 match b: 328 case False{}: None{} 329 case True{}: 330 Some{Equal.trans(Bool, U32.is_lt(x, 256), b, True{}, 331 Equal.sym(Bool, b, U32.is_lt(x, 256), link), {==})} 332 333 def aes_bytes_valid_cons_proof(x: U32, tail: List<&2, U32>, 334 head_proof: Maybe<&0, {U32.is_lt(x, 256) == True{} : Bool}>, 335 tail_proof: Maybe<&0, {bytes_valid(tail) == True{} : Bool}>) -> 336 Maybe<&0, {bytes_valid(x <> tail) == True{} : Bool}>: 337 match head_proof tail_proof: 338 case None{} _: None{} 339 case _ None{}: None{} 340 case Some{hp} Some{tp}: 341 Some{Equal.trans(Bool, Bool.and(U32.is_lt(x, 256), bytes_valid(tail)), 342 Bool.and(True{}, bytes_valid(tail)), True{}, 343 Equal.cong(Bool, Bool, b => Bool.and(b, bytes_valid(tail)), 344 U32.is_lt(x, 256), True{}, hp), 345 Equal.trans(Bool, Bool.and(True{}, bytes_valid(tail)), 346 bytes_valid(tail), True{}, {==}, tp))} 347 348 def aes_bytes_valid_from_bool(+bytes: List<&2, U32>, b: Bool, 349 link: {b == bytes_valid(bytes) : Bool}) -> 350 Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>: 351 match b: 352 case False{}: None{} 353 case True{}: 354 Some{Equal.sym(Bool, True{}, bytes_valid(bytes), link)} 355 356 def aes_bytes_valid_proof(+bytes: List<&2, U32>) -> 357 Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>: 358 aes_bytes_valid_from_bool(bytes, bytes_valid(bytes), {==}) 359 360 def key_checked(bytes: List<&2, U32>, -size: {List.length(&2, U32, bytes) == 32n : Nat}, 361 -valid: {bytes_valid(bytes) == True{} : Bool}) -> Result<&2, &2, Error, SecretKey>: 362 Done{SecretKey{bytes, size, valid}} 363 364 def key_from_proofs(+bytes: List<&2, U32>, 365 size: Maybe<&0, {List.length(&2, U32, bytes) == 32n : Nat}>, 366 valid: Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>) -> Result<&2, &2, Error, SecretKey>: 367 match size valid: 368 case Some{size} Some{valid}: Done{SecretKey{bytes, size, valid}} 369 case _ _: Fail{InvalidKey{}} 370 371 def key_impl(+bytes: List<&2, U32>) -> Result<&2, &2, Error, SecretKey>: 372 key_from_proofs(bytes, aes_nat_eq_proof(List.length(&2, U32, bytes), 32n), 373 aes_bytes_valid_proof(bytes)) 374 375 def nonce_checked(bytes: List<&2, U32>, size: {List.length(&2, U32, bytes) == 12n : Nat}, 376 valid: {bytes_valid(bytes) == True{} : Bool}) -> Result<&2, &2, Error, Nonce>: 377 Done{Nonce{bytes, size, valid}} 378 379 def nonce_from_proofs(+bytes: List<&2, U32>, 380 size: Maybe<&0, {List.length(&2, U32, bytes) == 12n : Nat}>, 381 valid: Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>) -> Result<&2, &2, Error, Nonce>: 382 match size valid: 383 case Some{size} Some{valid}: Done{Nonce{bytes, size, valid}} 384 case _ _: Fail{InvalidNonce{}} 385 386 def nonce_impl(+bytes: List<&2, U32>) -> Result<&2, &2, Error, Nonce>: 387 nonce_from_proofs(bytes, aes_nat_eq_proof(List.length(&2, U32, bytes), 12n), 388 aes_bytes_valid_proof(bytes)) 389 390 def secret_key_bytes(key: SecretKey) -> List<&2, U32>: 391 match key: 392 case SecretKey{bytes, size, valid}: bytes 393 394 def raw_nonce_bytes(nonce: Nonce) -> List<&2, U32>: 395 match nonce: 396 case Nonce{bytes, size, valid}: bytes 397 398 def tag_from_proofs(bytes: List<&2, U32>, 399 size: Maybe<&0, {List.length(&2, U32, bytes) == 16n : Nat}>, 400 valid: Maybe<&0, {bytes_valid(bytes) == True{} : Bool}>) -> Maybe<&2, Tag>: 401 match size valid: 402 case Some{size} Some{valid}: Some{Tag{bytes, size, valid}} 403 case _ _: None{} 404 405 def envelope_from_proofs(nonce: Nonce, +ciphertext: List<&2, U32>, tag: Tag, 406 valid: Maybe<&0, {bytes_valid(ciphertext) == True{} : Bool}>) -> Maybe<&2, Envelope>: 407 match valid: 408 case Some{valid}: Some{Envelope{nonce, ciphertext, tag, valid}} 409 case None{}: None{} 410 411 def envelope_from_tag_proof(nonce: Nonce, +ciphertext: List<&2, U32>, tag_bytes: List<&2, U32>, 412 tag: Maybe<&2, Tag>, valid: Maybe<&0, {bytes_valid(ciphertext) == True{} : Bool}>) -> Maybe<&2, Envelope>: 413 match tag: 414 case None{}: None{} 415 case Some{tag}: envelope_from_proofs(nonce, ciphertext, tag, valid) 416 417 def envelope_from_gcm(nonce: Nonce, output: Core.GcmOutput) -> Maybe<&2, Envelope>: 418 match output: 419 case Core.GcmOutput{+ciphertext, ciphertext_valid, 420 +tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad, 421 tag_matches}: 422 Some{Envelope{nonce, ciphertext, 423 Tag{tag_bytes, tag_size, core_bytes_valid_proof(tag_bytes, tag_valid)}, 424 core_bytes_valid_proof(ciphertext, ciphertext_valid)}} 425 426 def envelope_from_gcm_checked(nonce: Nonce, output: Core.GcmOutput) -> Envelope: 427 match output: 428 case Core.GcmOutput{+ciphertext, ciphertext_valid, 429 +tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad, 430 tag_matches}: 431 Envelope{nonce, ciphertext, 432 Tag{tag_bytes, tag_size, core_bytes_valid_proof(tag_bytes, tag_valid)}, 433 core_bytes_valid_proof(ciphertext, ciphertext_valid)} 434 435 def encrypt_output(nonce: Nonce, maybe_envelope: Maybe<&2, Envelope>) -> Result<&2, &2, Error, Envelope>: 436 match maybe_envelope: 437 case Some{envelope}: Done{envelope} 438 case None{}: Fail{InvalidBytes{}} 439 440 def encrypt_output_from_gcm(+nonce: Nonce, output: Core.GcmOutput) -> 441 Result<&2, &2, Error, Envelope>: 442 Done{envelope_from_gcm_checked(nonce, output)} 443 444 def encrypt_valid_output(key: SecretKey, +nonce: Nonce, 445 aad: List<&2, U32>, plaintext: List<&2, U32>) -> 446 Core.GcmOutput: 447 Core.gcm_encrypt_raw(secret_key_bytes(key), raw_nonce_bytes(nonce), aad, plaintext) 448 449 def encrypt_valid(key: SecretKey, +nonce: Nonce, aad: List<&2, U32>, 450 plaintext: List<&2, U32>) -> Result<&2, &2, Error, Envelope>: 451 encrypt_output_from_gcm(nonce, 452 encrypt_valid_output(key, nonce, aad, plaintext)) 453 454 def encrypt_checked(key: SecretKey, nonce: Nonce, aad: List<&2, U32>, 455 plaintext: List<&2, U32>, aad_ok: Bool, plaintext_ok: Bool) -> Result<&2, &2, Error, Envelope>: 456 match aad_ok plaintext_ok: 457 case True{} True{}: encrypt_valid(key, nonce, aad, plaintext) 458 case _ _: Fail{InvalidBytes{}} 459 460 def encrypt_impl(key: SecretKey, nonce: Nonce, +aad: List<&2, U32>, 461 +plaintext: List<&2, U32>) -> Result<&2, &2, Error, Envelope>: 462 encrypt_checked(key, nonce, aad, plaintext, aad_valid(aad), plaintext_valid(plaintext)) 463 464 def bytes_difference.go(a: List<&2, U32>, b: List<&2, U32>, +difference: U32) -> U32: 465 match a b: 466 case Nil{} Nil{}: difference 467 case x <> xs y <> ys: 468 bytes_difference.go(xs, ys, U32.or(difference, U32.xor(x, y))) 469 case _ _: 1 470 471 def bytes_equal_full_scan(a: List<&2, U32>, b: List<&2, U32>) -> Bool: 472 U32.is_eq(bytes_difference.go(a, b, 0), 0) 473 474 def decrypt_payload(words: List<&2, U32>, envelope: Envelope) -> Result<&2, &2, Error, List<&2, U32>>: 475 match envelope: 476 case Envelope{nonce, ciphertext, tag, valid}: 477 Done{Core.gcm_decrypt_expanded(words, raw_nonce_bytes(nonce), ciphertext)} 478 479 def decrypt_auth_result(words: List<&2, U32>, envelope: Envelope, authenticated: Bool) -> Result<&2, &2, Error, List<&2, U32>>: 480 match authenticated: 481 case False{}: Fail{AuthenticationFailed{}} 482 case True{}: decrypt_payload(words, envelope) 483 484 def decrypt_authenticated_tag(+words: List<&2, U32>, 485 +nonce: List<&2, U32>, +aad: List<&2, U32>, 486 +ciphertext: List<&2, U32>, +envelope: Envelope, tag: Tag) -> 487 Result<&2, &2, Error, List<&2, U32>>: 488 match tag: 489 case Tag{tag_bytes, size, valid}: 490 authenticated = bytes_equal_full_scan(tag_bytes, 491 Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, 492 ciphertext))) 493 decrypt_auth_result(words, envelope, authenticated) 494 495 def decrypt_authenticated(key: SecretKey, +aad: List<&2, U32>, +envelope: Envelope) -> Result<&2, &2, Error, List<&2, U32>>: 496 match key envelope: 497 case SecretKey{+key_bytes, _, _} Envelope{nonce, ciphertext, +tag, _}: 498 +words = Core.aes256_expand(key_bytes) 499 decrypt_authenticated_tag(words, raw_nonce_bytes(nonce), aad, 500 ciphertext, envelope, tag) 501 502 def decrypt_checked(+key: SecretKey, aad: List<&2, U32>, +envelope: Envelope, 503 aad_ok: Bool, ciphertext_ok: Bool) -> Result<&2, &2, Error, List<&2, U32>>: 504 match aad_ok ciphertext_ok: 505 case False{} _: Fail{InvalidBytes{}} 506 case True{} False{}: Fail{InvalidBytes{}} 507 case True{} True{}: decrypt_authenticated(key, aad, envelope) 508 509 def decrypt_impl(key: SecretKey, +aad: List<&2, U32>, +envelope: Envelope) -> Result<&2, &2, Error, List<&2, U32>>: 510 decrypt_checked(key, aad, envelope, aad_valid(aad), plaintext_valid(ciphertext(envelope))) 511 512 def parse_decoded(+nonce_bytes: List<&2, U32>, +tag_bytes: List<&2, U32>, +ciphertext: List<&2, U32>, 513 nonce_size: Maybe<&0, {List.length(&2, U32, nonce_bytes) == 12n : Nat}>, 514 tag_size: Maybe<&0, {List.length(&2, U32, tag_bytes) == 16n : Nat}>, 515 nonce_valid: Maybe<&0, {bytes_valid(nonce_bytes) == True{} : Bool}>, 516 tag_valid: Maybe<&0, {bytes_valid(tag_bytes) == True{} : Bool}>, 517 ciphertext_valid: Maybe<&0, {bytes_valid(ciphertext) == True{} : Bool}>) -> Result<&2, &2, Error, Envelope>: 518 match nonce_size tag_size nonce_valid tag_valid ciphertext_valid: 519 case Some{ns} Some{ts} Some{nv} Some{tv} Some{cv}: 520 Done{Envelope{Nonce{nonce_bytes, ns, nv}, ciphertext, Tag{tag_bytes, ts, tv}, cv}} 521 case _ _ _ _ _: Fail{InvalidEnvelope{}} 522 523 def parse_decoded_hex(nonce: Maybe<&2, List<&2, U32>>, tag: Maybe<&2, List<&2, U32>>, 524 ciphertext: Maybe<&2, List<&2, U32>>) -> Result<&2, &2, Error, Envelope>: 525 match nonce tag ciphertext: 526 case Some{+n} Some{+t} Some{+c}: 527 parse_decoded(n, t, c, aes_nat_eq_proof(List.length(&2, U32, n), 12n), 528 aes_nat_eq_proof(List.length(&2, U32, t), 16n), aes_bytes_valid_proof(n), 529 aes_bytes_valid_proof(t), aes_bytes_valid_proof(c)) 530 case _ _ _: Fail{InvalidEnvelope{}} 531 532 def parse_version_fields(fields: List<&2, String>) -> Result<&2, &2, Error, Envelope>: 533 match fields: 534 case version <> nonce_text <> tag_text <> ciphertext_text <> Nil{}: 535 parse_decoded_hex(decode_hex(nonce_text), decode_hex(tag_text), decode_hex(ciphertext_text)) 536 case _: Fail{InvalidEnvelope{}} 537 538 def parse_version(fields: List<&2, String>, valid_version: Bool) -> Result<&2, &2, Error, Envelope>: 539 match valid_version: 540 case False{}: Fail{InvalidEnvelope{}} 541 case True{}: parse_version_fields(fields) 542 543 def parse_string_cmp_is_eq(result: ((String & String) & Cmp)) -> Bool: 544 match result: 545 case ((_, _), EQ{}): True{} 546 case ((_, _), _): False{} 547 548 def parse_fields(fields: List<&2, String>) -> Result<&2, &2, Error, Envelope>: 549 match fields: 550 case +version <> rest: 551 parse_version(fields, parse_string_cmp_is_eq(String.cmp(version, "v1"))) 552 case Nil{}: Fail{InvalidEnvelope{}} 553 554 def parse_canonical_decision(text: String, envelope: Envelope, 555 canonical: Bool) -> Result<&2, &2, Error, Envelope>: 556 match canonical: 557 case True{}: Done{envelope} 558 case False{}: Fail{InvalidEnvelope{}} 559 560 def parse_canonical(+text: String, 561 result: Result<&2, &2, Error, Envelope>) -> 562 Result<&2, &2, Error, Envelope>: 563 match result: 564 case Fail{error}: Fail{error} 565 case Done{+envelope}: 566 parse_canonical_decision(text, envelope, 567 String.eq(encode_impl(envelope), text)) 568 569 def parse_impl(+text: String) -> Result<&2, &2, Error, Envelope>: 570 parse_canonical(text, parse_fields(String.split(text, '.'))) 571 572 def key(bytes): 573 key_impl(bytes) 574 575 def nonce(bytes): 576 nonce_impl(bytes) 577 578 def encrypt(key, nonce, aad, plaintext): 579 encrypt_impl(key, nonce, aad, plaintext) 580 581 def decrypt(key, aad, envelope): 582 decrypt_impl(key, aad, envelope) 583 584 def encode(envelope): 585 encode_impl(envelope) 586 587 def parse(text): 588 parse_impl(text)