src/crypto/aead/chacha20poly1305.bend

bend-collections-laws-crypto@1.0.0.0 · 108 lines · 22 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as CH
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend as P
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/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.
22def 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
25def 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.
29def 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
34def 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
38def 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).
42def 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.
46def 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
50def 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
55def 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
58def 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.
66def 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].
71def xkey(key: List<&2, U32>, nonce: List<&2, U32>) -> List<&2, U32>:
72  CH.hchacha20_unchecked(key, CH.take(16n, nonce))
73
74def xnonce(nonce: List<&2, U32>) -> List<&2, U32>:
75  0 <> 0 <> 0 <> 0 <> CH.skip(16n, nonce)
76
77def 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
80def 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
85def 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
88def 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
93def 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
98def 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
101def 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
104def 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
107def 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))