spec/crypto/chacha.bend

bend-collections-laws-crypto@1.0.0.0 · 205 lines · 30 definitions

1import Base
2
3# Executable specification of the ChaCha20 block function and stream cipher
4# (RFC 8439 sections 2.1-2.4) and of HChaCha20 / XChaCha20
5# (draft-irtf-cfrg-xchacha-03 sections 2.2-2.3), transcribed from the
6# documents. Nothing is shared with the implementation (src/crypto/chacha/):
7# the state is the RFC's list of sixteen words, indexed and updated by
8# position, the quarter round is the RFC's sequence of twelve operations,
9# keys and nonces are byte lists read as little-endian words, and the
10# keystream is XORed byte by byte. The shape follows HACL*'s Spec.Chacha20.
11#
12# Bytes are U32 values (each < 256 in the byte convention). A word is read
13# from the low 8 bits of four bytes; the stream XOR works on the whole U32,
14# so encrypting twice is the identity for every list of U32.
15
16# ---------------------------------------------------------------- lists
17
18# Element i of a list, 0 past its end.
19def get(xs: List<&2, U32>, i: Nat) -> U32:
20  match xs i:
21    case Nil{} _: 0
22    case x <> rest 0n: x
23    case x <> rest 1n+p: get(rest, p)
24
25# The list with element i replaced (unchanged past its end).
26def put(xs: List<&2, U32>, i: Nat, y: U32) -> List<&2, U32>:
27  match xs i:
28    case Nil{} _: Nil{}
29    case x <> rest 0n: y <> rest
30    case x <> rest 1n+p: x <> put(rest, p, y)
31
32# ---------------------------------------------------------------- 2.1 quarter round
33
34# x <<< n: rotation of a 32-bit word left by n bits (0 < n < 32).
35def rotl(+x: U32, +n: Nat) -> U32:
36  U32.or(U32.shln(x, n), U32.shrn(x, Nat.sub(32n, n)))
37
38# 2.2: QUARTERROUND(a, b, c, d) applied to the state at those positions:
39#   a += b; d ^= a; d <<<= 16;
40#   c += d; b ^= c; b <<<= 12;
41#   a += b; d ^= a; d <<<= 8;
42#   c += d; b ^= c; b <<<= 7;
43def quarter(+s: List<&2, U32>, +a: Nat, +b: Nat, +c: Nat, +d: Nat) -> List<&2, U32>:
44  +a1 = U32.add(get(s, a), get(s, b))
45  +d1 = rotl(U32.xor(get(s, d), a1), 16n)
46  +c1 = U32.add(get(s, c), d1)
47  +b1 = rotl(U32.xor(get(s, b), c1), 12n)
48  +a2 = U32.add(a1, b1)
49  +d2 = rotl(U32.xor(d1, a2), 8n)
50  +c2 = U32.add(c1, d2)
51  +b2 = rotl(U32.xor(b1, c2), 7n)
52  put(put(put(put(s, a, a2), b, b2), c, c2), d, d2)
53
54# ---------------------------------------------------------------- 2.3 block function
55
56# inner_block: four column rounds, then four diagonal rounds.
57def inner_block(s: List<&2, U32>) -> List<&2, U32>:
58  s1 = quarter(s, 0n, 4n, 8n, 12n)
59  s2 = quarter(s1, 1n, 5n, 9n, 13n)
60  s3 = quarter(s2, 2n, 6n, 10n, 14n)
61  s4 = quarter(s3, 3n, 7n, 11n, 15n)
62  s5 = quarter(s4, 0n, 5n, 10n, 15n)
63  s6 = quarter(s5, 1n, 6n, 11n, 12n)
64  s7 = quarter(s6, 2n, 7n, 8n, 13n)
65  quarter(s7, 3n, 4n, 9n, 14n)
66
67# n applications of inner_block (ChaCha20: n = 10, twenty rounds).
68def inner_blocks(n: Nat, s: List<&2, U32>) -> List<&2, U32>:
69  match n:
70    case 0n: s
71    case 1n+p: inner_blocks(p, inner_block(s))
72
73# A little-endian word from the low 8 bits of four bytes.
74def word(b0: U32, b1: U32, b2: U32, b3: U32) -> U32:
75  U32.or(U32.or(U32.or(U32.and(b0, 255), U32.shln(U32.and(b1, 255), 8n)),
76    U32.shln(U32.and(b2, 255), 16n)), U32.shln(U32.and(b3, 255), 24n))
77
78# The words of a byte list, four bytes each (a partial tail is dropped).
79def words(bytes: List<&2, U32>) -> List<&2, U32>:
80  match bytes:
81    case b0 <> b1 <> b2 <> b3 <> rest: word(b0, b1, b2, b3) <> words(rest)
82    case _: Nil{}
83
84# The four little-endian bytes of a word.
85def octets(+w: U32) -> List<&2, U32>:
86  [U32.and(w, 255), U32.and(U32.shrn(w, 8n), 255),
87   U32.and(U32.shrn(w, 16n), 255), U32.shrn(w, 24n)]
88
89def serialize(ws: List<&2, U32>) -> List<&2, U32>:
90  match ws:
91    case Nil{}: Nil{}
92    case w <> rest: List.append(&2, U32, octets(w), serialize(rest))
93
94# "expa" "nd 3" "2-by" "te k"
95def constants() -> List<&2, U32>:
96  [1634760805, 857760878, 2036477234, 1797285236]
97
98# The initial state: constants, key (eight words), block counter, nonce
99# (three words). Missing key or nonce words read as 0 (the public API
100# rejects other lengths before this is reached).
101def state(+k: List<&2, U32>, counter: U32, +n: List<&2, U32>) -> List<&2, U32>:
102  List.append(&2, U32, constants(),
103    [get(k, 0n), get(k, 1n), get(k, 2n), get(k, 3n), get(k, 4n), get(k, 5n), get(k, 6n), get(k, 7n),
104     counter, get(n, 0n), get(n, 1n), get(n, 2n)])
105
106def add_words(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
107  match xs ys:
108    case x <> xt y <> yt: U32.add(x, y) <> add_words(xt, yt)
109    case _ _: Nil{}
110
111# chacha20_block with n double rounds: working state after n inner blocks,
112# added to the initial state, serialized little-endian (64 bytes).
113def block_body(+n: Nat, +key: List<&2, U32>, counter: U32, +nonce: List<&2, U32>) -> List<&2, U32>:
114  +s = state(words(key), counter, words(nonce))
115  serialize(add_words(s, inner_blocks(n, s)))
116
117# The same, entered through a match on the key's first cell. Both arms are
118# block_body; the match only keeps the proof checker from evaluating the
119# rounds on a symbolic key (it compares types by evaluating them).
120def block_rounds(+n: Nat, key: List<&2, U32>, counter: U32, +nonce: List<&2, U32>) -> List<&2, U32>:
121  match key:
122    case Nil{}: block_body(n, Nil{}, counter, nonce)
123    case b <> rest: block_body(n, b <> rest, counter, nonce)
124
125def block(+key: List<&2, U32>, counter: U32, +nonce: List<&2, U32>) -> List<&2, U32>:
126  block_rounds(10n, key, counter, nonce)
127
128# ---------------------------------------------------------------- 2.4 encryption
129
130# The first n bytes of a list, and the rest.
131def prefix(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
132  match n xs:
133    case 0n _: Nil{}
134    case 1n+p Nil{}: Nil{}
135    case 1n+p x <> rest: x <> prefix(p, rest)
136
137def suffix(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
138  match n xs:
139    case 0n _: xs
140    case 1n+p Nil{}: Nil{}
141    case 1n+p x <> rest: suffix(p, rest)
142
143# The plaintext cut into 64-byte blocks; the last one may be shorter (and
144# there is none for the empty plaintext). fuel bounds the number of blocks
145# (the length of the plaintext is enough).
146def blocks(fuel: Nat, +xs: List<&2, U32>) -> List<&2, List<&2, U32>>:
147  match fuel xs:
148    case 0n _: Nil{}
149    case 1n+p Nil{}: Nil{}
150    case 1n+p x <> rest: prefix(64n, x <> rest) <> blocks(p, suffix(64n, x <> rest))
151
152# Byte-wise XOR of a block with the keystream (as long as the block).
153def xor_bytes(xs: List<&2, U32>, ks: List<&2, U32>) -> List<&2, U32>:
154  match xs ks:
155    case x <> xt k <> kt: U32.xor(x, k) <> xor_bytes(xt, kt)
156    case _ _: Nil{}
157
158# for j = 0 .. : block j is XORed with chacha20_block(key, counter + j, nonce).
159def encrypt_blocks(bs: List<&2, List<&2, U32>>, +n: Nat, +key: List<&2, U32>, +counter: U32, +nonce: List<&2, U32>) -> List<&2, U32>:
160  match bs:
161    case Nil{}: Nil{}
162    case b <> rest:
163      List.append(&2, U32, xor_bytes(b, block_rounds(n, key, counter, nonce)),
164        encrypt_blocks(rest, n, key, U32.add(counter, 1), nonce))
165
166# chacha20_encrypt(key, counter, nonce, plaintext) with n double rounds.
167def encrypt_rounds(+n: Nat, +key: List<&2, U32>, counter: U32, +nonce: List<&2, U32>, +plaintext: List<&2, U32>) -> List<&2, U32>:
168  encrypt_blocks(blocks(List.length(&2, U32, plaintext), plaintext), n, key, counter, nonce)
169
170def encrypt(+key: List<&2, U32>, counter: U32, +nonce: List<&2, U32>, +plaintext: List<&2, U32>) -> List<&2, U32>:
171  encrypt_rounds(10n, key, counter, nonce, plaintext)
172
173# ---------------------------------------------------------------- XChaCha20
174
175# HChaCha20 (draft-irtf-cfrg-xchacha-03 section 2.2): the state is set up as
176# for ChaCha20 with the 16-byte nonce in words 12..15; after twenty rounds
177# (no feed-forward) words 0..3 and 12..15 are the 32-byte subkey.
178def hstate(+k: List<&2, U32>, +n: List<&2, U32>) -> List<&2, U32>:
179  List.append(&2, U32, constants(),
180    [get(k, 0n), get(k, 1n), get(k, 2n), get(k, 3n), get(k, 4n), get(k, 5n), get(k, 6n), get(k, 7n),
181     get(n, 0n), get(n, 1n), get(n, 2n), get(n, 3n)])
182
183def hchacha_body(+n: Nat, +key: List<&2, U32>, +nonce: List<&2, U32>) -> List<&2, U32>:
184  +s = inner_blocks(n, hstate(words(key), words(nonce)))
185  serialize([get(s, 0n), get(s, 1n), get(s, 2n), get(s, 3n), get(s, 12n), get(s, 13n), get(s, 14n), get(s, 15n)])
186
187# Entered through a match on the key, as block_rounds.
188def hchacha_rounds(+n: Nat, key: List<&2, U32>, +nonce: List<&2, U32>) -> List<&2, U32>:
189  match key:
190    case Nil{}: hchacha_body(n, Nil{}, nonce)
191    case b <> rest: hchacha_body(n, b <> rest, nonce)
192
193def hchacha20(+key: List<&2, U32>, +nonce: List<&2, U32>) -> List<&2, U32>:
194  hchacha_rounds(10n, key, nonce)
195
196# Section 2.3: XChaCha20 is ChaCha20 under the HChaCha20 subkey of the
197# first 16 nonce bytes, with the nonce 0x00000000 || nonce[16..24].
198def xsubkey(+key: List<&2, U32>, +nonce: List<&2, U32>) -> List<&2, U32>:
199  hchacha20(key, prefix(16n, nonce))
200
201def xnonce(+nonce: List<&2, U32>) -> List<&2, U32>:
202  List.append(&2, U32, [0, 0, 0, 0], suffix(16n, nonce))
203
204def xencrypt(+key: List<&2, U32>, counter: U32, +nonce: List<&2, U32>, +plaintext: List<&2, U32>) -> List<&2, U32>:
205  encrypt(xsubkey(key, nonce), counter, xnonce(nonce), plaintext)