1 import Base 2 import ../chacha/chacha20.bend as CH 3 import ../poly1305/poly1305.bend as P 4 import ../subtle.bend as S 5 6 # ChaCha20-Poly1305 (RFC 8439 section 2.8) and XChaCha20-Poly1305 7 # (draft-irtf-cfrg-xchacha-03), over byte lists (U32 values < 256). 8 # 9 # encrypt(key, nonce, aad, plaintext) -> Some(ciphertext || tag) 10 # decrypt(key, nonce, aad, ciphertext || tag) -> Some(plaintext) 11 # 12 # Keys have 32 bytes, nonces 12 (ChaCha20-Poly1305) or 24 (XChaCha20- 13 # Poly1305), tags 16. Both functions return None for other key or nonce 14 # lengths; decrypt returns None for inputs shorter than a tag and whenever 15 # the tag differs from the one computed over aad and ciphertext (compared 16 # with the constant-time Subtle.eq, before any plaintext is produced). 17 # Bend has no timing model: constant time is a property of the code's shape 18 # (no branch or index on secret bytes; only the final accept/reject), not a 19 # proved fact. 20 21 # poly1305_key_gen: the first 32 bytes of the block with counter 0. 22 def poly_key(key: List<&2, U32>, nonce: List<&2, U32>) -> List<&2, U32>: 23 CH.take(32n, CH.block_rounds(10n, key, 0, nonce)) 24 25 def pad16(+xs: List<&2, U32>) -> List<&2, U32>: 26 List.replicate(U32, Nat.mod(Nat.sub(16n, Nat.mod(List.length(&2, U32, xs), 16n)), 16n), 0) 27 28 # The eight little-endian bytes of a length. 29 def le8(n: Nat, +x: Nat) -> List<&2, U32>: 30 match n: 31 case 0n: Nil{} 32 case 1n+k: U32.from_nat(Nat.mod(x, 256n)) <> le8(k, Nat.div(x, 256n)) 33 34 def mac_data(+aad: List<&2, U32>, +ct: List<&2, U32>) -> List<&2, U32>: 35 List.append(&2, U32, aad, List.append(&2, U32, pad16(aad), List.append(&2, U32, ct, 36 List.append(&2, U32, pad16(ct), List.append(&2, U32, le8(8n, List.length(&2, U32, aad)), le8(8n, List.length(&2, U32, ct))))))) 37 38 def tag(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +ct: List<&2, U32>) -> List<&2, U32>: 39 P.mac(poly_key(key, nonce), mac_data(aad, ct)) 40 41 # chacha20_encrypt(key, 1, nonce, plaintext). 42 def encrypt_ct(key: List<&2, U32>, nonce: List<&2, U32>, +pt: List<&2, U32>) -> List<&2, U32>: 43 CH.encrypt_rounds(10n, key, 1, nonce, pt) 44 45 # ciphertext || tag, without length checks. 46 def seal(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +pt: List<&2, U32>) -> List<&2, U32>: 47 +ct = encrypt_ct(key, nonce, pt) 48 List.append(&2, U32, ct, tag(key, nonce, aad, ct)) 49 50 def open_tag(ok: Bool, +key: List<&2, U32>, +nonce: List<&2, U32>, +ct: List<&2, U32>) -> Maybe<&2, List<&2, U32>>: 51 match ok: 52 case True{}: Some{CH.encrypt_rounds(10n, key, 1, nonce, ct)} 53 case False{}: None{} 54 55 def open_split(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +ct: List<&2, U32>, +t: List<&2, U32>) -> Maybe<&2, List<&2, U32>>: 56 open_tag(S.eq(t, tag(key, nonce, aad, ct)), key, nonce, ct) 57 58 def open_len(short: Bool, +key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +data: List<&2, U32>) -> Maybe<&2, List<&2, U32>>: 59 match short: 60 case True{}: None{} 61 case False{}: 62 +n = Nat.sub(List.length(&2, U32, data), 16n) 63 open_split(key, nonce, aad, CH.take(n, data), CH.skip(n, data)) 64 65 # The plaintext of ciphertext || tag, without key/nonce length checks. 66 def open(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +data: List<&2, U32>) -> Maybe<&2, List<&2, U32>>: 67 open_len(Nat.is_lt(List.length(&2, U32, data), 16n), key, nonce, aad, data) 68 69 # XChaCha20-Poly1305: the HChaCha20 subkey of nonce[0..16] and the nonce 70 # 0x00000000 || nonce[16..24]. 71 def xkey(key: List<&2, U32>, nonce: List<&2, U32>) -> List<&2, U32>: 72 CH.hchacha20_unchecked(key, CH.take(16n, nonce)) 73 74 def xnonce(nonce: List<&2, U32>) -> List<&2, U32>: 75 0 <> 0 <> 0 <> 0 <> CH.skip(16n, nonce) 76 77 def xseal(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +pt: List<&2, U32>) -> List<&2, U32>: 78 seal(xkey(key, nonce), xnonce(nonce), aad, pt) 79 80 def xopen(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +data: List<&2, U32>) -> Maybe<&2, List<&2, U32>>: 81 open(xkey(key, nonce), xnonce(nonce), aad, data) 82 83 # ---------------------------------------------------------------- checked API 84 85 def lengths_ok(+key: List<&2, U32>, +nonce: List<&2, U32>, n: Nat) -> Bool: 86 Bool.and(Nat.is_eq(List.length(&2, U32, key), 32n), Nat.is_eq(List.length(&2, U32, nonce), n)) 87 88 def when(ok: Bool, x: List<&2, U32>) -> Maybe<&2, List<&2, U32>>: 89 match ok: 90 case True{}: Some{x} 91 case False{}: None{} 92 93 def when_open(ok: Bool, r: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>: 94 match ok: 95 case True{}: r 96 case False{}: None{} 97 98 def encrypt(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +pt: List<&2, U32>) -> Maybe<&2, List<&2, U32>>: 99 when(lengths_ok(key, nonce, 12n), seal(key, nonce, aad, pt)) 100 101 def decrypt(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +data: List<&2, U32>) -> Maybe<&2, List<&2, U32>>: 102 when_open(lengths_ok(key, nonce, 12n), open(key, nonce, aad, data)) 103 104 def xencrypt(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +pt: List<&2, U32>) -> Maybe<&2, List<&2, U32>>: 105 when(lengths_ok(key, nonce, 24n), xseal(key, nonce, aad, pt)) 106 107 def xdecrypt(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +data: List<&2, U32>) -> Maybe<&2, List<&2, U32>>: 108 when_open(lengths_ok(key, nonce, 24n), xopen(key, nonce, aad, data))