1 import 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. 19 def 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). 26 def 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). 35 def 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; 43 def 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. 57 def 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). 68 def 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. 74 def 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). 79 def 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. 85 def 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 89 def 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" 95 def 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). 101 def 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 106 def 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). 113 def 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). 120 def 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 125 def 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. 131 def 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 137 def 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). 146 def 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). 153 def 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). 159 def 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. 167 def 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 170 def 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. 178 def 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 183 def 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. 188 def 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 193 def 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]. 198 def xsubkey(+key: List<&2, U32>, +nonce: List<&2, U32>) -> List<&2, U32>: 199 hchacha20(key, prefix(16n, nonce)) 200 201 def xnonce(+nonce: List<&2, U32>) -> List<&2, U32>: 202 List.append(&2, U32, [0, 0, 0, 0], suffix(16n, nonce)) 203 204 def 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)