1	import Base
2	import ../../../src/crypto/chacha/chacha20.bend as I
3	import ../../../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.
15	law 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.
23	law 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.
32	law 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	
38	law 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.
44	law 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	
53	law 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	
61	law 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	
68	law 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	
77	law 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	
85	law 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	
92	law 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	
98	law 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	
107	law 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.
118	law 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	
126	law 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.
134	law 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.
143	law 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	
150	law 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}