proofs/crypto/chacha/laws.bend

bend-collections-laws-crypto@1.0.0.0 · 154 lines · 18 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as I
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R
4
5# The ChaCha20 / HChaCha20 / XChaCha20 clauses of src/crypto/chacha/ against
6# spec/crypto/chacha.bend (RFC 8439 sections 2.3-2.4,
7# draft-irtf-cfrg-xchacha-03 sections 2.2-2.3). Proved in proof.bend, for
8# every key, nonce, counter and byte list (lists of any length and any U32
9# values). r is the number of double rounds: every clause stated with r holds
10# for ChaCha20 (10), ChaCha12 (6) and ChaCha8 (4) alike.
11
12# ---- the functions against the specification
13
14# chacha20_block with r double rounds.
15law block_rounds:
16  for +r: Nat
17  for +key: List<&2, U32>
18  for +counter: U32
19  for +nonce: List<&2, U32>
20  {I.block_rounds(r, key, counter, nonce) == R.block_rounds(r, key, counter, nonce) : List<&2, U32>}
21
22# chacha20_encrypt with r double rounds.
23law encrypt_rounds:
24  for +r: Nat
25  for +key: List<&2, U32>
26  for +counter: U32
27  for +nonce: List<&2, U32>
28  for +plaintext: List<&2, U32>
29  {I.encrypt_rounds(r, key, counter, nonce, plaintext) == R.encrypt_rounds(r, key, counter, nonce, plaintext) : List<&2, U32>}
30
31# HChaCha20 with r double rounds, and at twenty rounds.
32law hchacha_rounds:
33  for +r: Nat
34  for +key: List<&2, U32>
35  for +nonce: List<&2, U32>
36  {I.hchacha_rounds(r, key, nonce) == R.hchacha_rounds(r, key, nonce) : List<&2, U32>}
37
38law hchacha20:
39  for +key: List<&2, U32>
40  for +nonce: List<&2, U32>
41  {I.hchacha20_unchecked(key, nonce) == R.hchacha20(key, nonce) : List<&2, U32>}
42
43# XChaCha20.
44law xencrypt:
45  for +key: List<&2, U32>
46  for +counter: U32
47  for +nonce: List<&2, U32>
48  for +plaintext: List<&2, U32>
49  {I.xencrypt_unchecked(key, counter, nonce, plaintext) == R.xencrypt(key, counter, nonce, plaintext) : List<&2, U32>}
50
51# ---- the checked API: Some(the specification) on the RFC lengths, None otherwise
52
53law chacha20_block.valid:
54  for +key: List<&2, U32>
55  for +counter: U32
56  for +nonce: List<&2, U32>
57  for +hk: {List.length(&2, U32, key) == 32n : Nat}
58  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
59  {I.chacha20_block(key, counter, nonce) == Some{R.block(key, counter, nonce)} : Maybe<&2, List<&2, U32>>}
60
61law chacha20_block.invalid:
62  for +key: List<&2, U32>
63  for +counter: U32
64  for +nonce: List<&2, U32>
65  for +h: {Bool.and(Nat.is_eq(List.length(&2, U32, key), 32n), Nat.is_eq(List.length(&2, U32, nonce), 12n)) == False{} : Bool}
66  {I.chacha20_block(key, counter, nonce) == None{} : Maybe<&2, List<&2, U32>>}
67
68law chacha20.valid:
69  for +key: List<&2, U32>
70  for +counter: U32
71  for +nonce: List<&2, U32>
72  for +plaintext: List<&2, U32>
73  for +hk: {List.length(&2, U32, key) == 32n : Nat}
74  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
75  {I.chacha20(key, counter, nonce, plaintext) == Some{R.encrypt(key, counter, nonce, plaintext)} : Maybe<&2, List<&2, U32>>}
76
77law chacha20.invalid:
78  for +key: List<&2, U32>
79  for +counter: U32
80  for +nonce: List<&2, U32>
81  for +plaintext: List<&2, U32>
82  for +h: {Bool.and(Nat.is_eq(List.length(&2, U32, key), 32n), Nat.is_eq(List.length(&2, U32, nonce), 12n)) == False{} : Bool}
83  {I.chacha20(key, counter, nonce, plaintext) == None{} : Maybe<&2, List<&2, U32>>}
84
85law hchacha20.valid:
86  for +key: List<&2, U32>
87  for +nonce: List<&2, U32>
88  for +hk: {List.length(&2, U32, key) == 32n : Nat}
89  for +hn: {List.length(&2, U32, nonce) == 16n : Nat}
90  {I.hchacha20(key, nonce) == Some{R.hchacha20(key, nonce)} : Maybe<&2, List<&2, U32>>}
91
92law hchacha20.invalid:
93  for +key: List<&2, U32>
94  for +nonce: List<&2, U32>
95  for +h: {Bool.and(Nat.is_eq(List.length(&2, U32, key), 32n), Nat.is_eq(List.length(&2, U32, nonce), 16n)) == False{} : Bool}
96  {I.hchacha20(key, nonce) == None{} : Maybe<&2, List<&2, U32>>}
97
98law xchacha20.valid:
99  for +key: List<&2, U32>
100  for +counter: U32
101  for +nonce: List<&2, U32>
102  for +plaintext: List<&2, U32>
103  for +hk: {List.length(&2, U32, key) == 32n : Nat}
104  for +hn: {List.length(&2, U32, nonce) == 24n : Nat}
105  {I.xchacha20(key, counter, nonce, plaintext) == Some{R.xencrypt(key, counter, nonce, plaintext)} : Maybe<&2, List<&2, U32>>}
106
107law xchacha20.invalid:
108  for +key: List<&2, U32>
109  for +counter: U32
110  for +nonce: List<&2, U32>
111  for +plaintext: List<&2, U32>
112  for +h: {Bool.and(Nat.is_eq(List.length(&2, U32, key), 32n), Nat.is_eq(List.length(&2, U32, nonce), 24n)) == False{} : Bool}
113  {I.xchacha20(key, counter, nonce, plaintext) == None{} : Maybe<&2, List<&2, U32>>}
114
115# ---- properties
116
117# Decryption is encryption: applying the cipher twice is the identity.
118law involution:
119  for +r: Nat
120  for +key: List<&2, U32>
121  for +counter: U32
122  for +nonce: List<&2, U32>
123  for +plaintext: List<&2, U32>
124  {I.encrypt_rounds(r, key, counter, nonce, I.encrypt_rounds(r, key, counter, nonce, plaintext)) == plaintext : List<&2, U32>}
125
126law xinvolution:
127  for +key: List<&2, U32>
128  for +counter: U32
129  for +nonce: List<&2, U32>
130  for +plaintext: List<&2, U32>
131  {I.xencrypt_unchecked(key, counter, nonce, I.xencrypt_unchecked(key, counter, nonce, plaintext)) == plaintext : List<&2, U32>}
132
133# The ciphertext is as long as the plaintext.
134law encrypt_length:
135  for +r: Nat
136  for +key: List<&2, U32>
137  for +counter: U32
138  for +nonce: List<&2, U32>
139  for +plaintext: List<&2, U32>
140  {List.length(&2, U32, I.encrypt_rounds(r, key, counter, nonce, plaintext)) == List.length(&2, U32, plaintext) : Nat}
141
142# The block function's output has 64 bytes, HChaCha20's 32.
143law block_length:
144  for +r: Nat
145  for +key: List<&2, U32>
146  for +counter: U32
147  for +nonce: List<&2, U32>
148  {List.length(&2, U32, R.block_rounds(r, key, counter, nonce)) == 64n : Nat}
149
150law hchacha_length:
151  for +r: Nat
152  for +key: List<&2, U32>
153  for +nonce: List<&2, U32>
154  {List.length(&2, U32, R.hchacha_rounds(r, key, nonce)) == 32n : Nat}