1	import Base
2	import ../../../src/crypto/aead.bend as A
3	import ../../../src/crypto/aead/chacha20poly1305.bend as CP
4	import ../../../spec/crypto/chacha.bend as RC
5	import ../../../spec/crypto/chacha20poly1305.bend as R
6	import ../../../spec/crypto/aes/gcm.bend as G
7	
8	# The clauses of the AEAD facade src/crypto/aead.bend (proved in proof.bend,
9	# one case per algorithm). hk / hn: the key and nonce have the algorithm's
10	# lengths.
11	
12	# The tag the specification computes over ciphertext ct: decrypt accepts
13	# ct || t exactly for this t.
14	def expected_tag(alg: A.Alg, +key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +ct: List<&2, U32>) -> List<&2, U32>:
15	  match alg:
16	    case A.CHACHA20_POLY1305{}: R.tag(key, nonce, aad, ct)
17	    case A.XCHACHA20_POLY1305{}: R.tag(RC.xsubkey(key, nonce), RC.xnonce(nonce), aad, ct)
18	    case A.AES_128_GCM{}: G.aes_tag(key, nonce, aad, ct)
19	    case A.AES_256_GCM{}: G.aes_tag(key, nonce, aad, ct)
20	
21	# decrypt applied to what encrypt returned (None stays None).
22	def decrypt_sealed(+alg: A.Alg, +key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
23	  match m:
24	    case None{}: None{}
25	    case Some{c}: A.decrypt(alg, key, nonce, aad, c)
26	
27	# ---- each algorithm is its specification
28	
29	law chacha20poly1305.seal:
30	  for +key: List<&2, U32>
31	  for +nonce: List<&2, U32>
32	  for +aad: List<&2, U32>
33	  for +pt: List<&2, U32>
34	  {A.seal(A.CHACHA20_POLY1305{}, key, nonce, aad, pt) == Some{R.seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
35	
36	law chacha20poly1305.open:
37	  for +key: List<&2, U32>
38	  for +nonce: List<&2, U32>
39	  for +aad: List<&2, U32>
40	  for +data: List<&2, U32>
41	  {A.open(A.CHACHA20_POLY1305{}, key, nonce, aad, data) == R.open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
42	
43	law xchacha20poly1305.seal:
44	  for +key: List<&2, U32>
45	  for +nonce: List<&2, U32>
46	  for +aad: List<&2, U32>
47	  for +pt: List<&2, U32>
48	  {A.seal(A.XCHACHA20_POLY1305{}, key, nonce, aad, pt) == Some{R.xseal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
49	
50	law xchacha20poly1305.open:
51	  for +key: List<&2, U32>
52	  for +nonce: List<&2, U32>
53	  for +aad: List<&2, U32>
54	  for +data: List<&2, U32>
55	  {A.open(A.XCHACHA20_POLY1305{}, key, nonce, aad, data) == R.xopen(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
56	
57	law aes128gcm.seal:
58	  for +key: List<&2, U32>
59	  for +hk: {List.length(&2, U32, key) == 16n : Nat}
60	  for +nonce: List<&2, U32>
61	  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
62	  for +aad: List<&2, U32>
63	  for +pt: List<&2, U32>
64	  {A.seal(A.AES_128_GCM{}, key, nonce, aad, pt) == Some{G.aes_seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
65	
66	law aes128gcm.open:
67	  for +key: List<&2, U32>
68	  for +hk: {List.length(&2, U32, key) == 16n : Nat}
69	  for +nonce: List<&2, U32>
70	  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
71	  for +aad: List<&2, U32>
72	  for +data: List<&2, U32>
73	  {A.open(A.AES_128_GCM{}, key, nonce, aad, data) == G.aes_open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
74	
75	law aes256gcm.seal:
76	  for +key: List<&2, U32>
77	  for +hk: {List.length(&2, U32, key) == 32n : Nat}
78	  for +nonce: List<&2, U32>
79	  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
80	  for +aad: List<&2, U32>
81	  for +pt: List<&2, U32>
82	  {A.seal(A.AES_256_GCM{}, key, nonce, aad, pt) == Some{G.aes_seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
83	
84	law aes256gcm.open:
85	  for +key: List<&2, U32>
86	  for +hk: {List.length(&2, U32, key) == 32n : Nat}
87	  for +nonce: List<&2, U32>
88	  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
89	  for +aad: List<&2, U32>
90	  for +data: List<&2, U32>
91	  {A.open(A.AES_256_GCM{}, key, nonce, aad, data) == G.aes_open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
92	
93	# The per-algorithm checked ChaCha20-Poly1305 API agrees with the facade.
94	law chacha20poly1305.encrypt:
95	  for +key: List<&2, U32>
96	  for +nonce: List<&2, U32>
97	  for +aad: List<&2, U32>
98	  for +pt: List<&2, U32>
99	  {CP.encrypt(key, nonce, aad, pt) == A.encrypt(A.CHACHA20_POLY1305{}, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}
100	
101	law chacha20poly1305.decrypt:
102	  for +key: List<&2, U32>
103	  for +nonce: List<&2, U32>
104	  for +aad: List<&2, U32>
105	  for +data: List<&2, U32>
106	  {CP.decrypt(key, nonce, aad, data) == A.decrypt(A.CHACHA20_POLY1305{}, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
107	
108	law xchacha20poly1305.encrypt:
109	  for +key: List<&2, U32>
110	  for +nonce: List<&2, U32>
111	  for +aad: List<&2, U32>
112	  for +pt: List<&2, U32>
113	  {CP.xencrypt(key, nonce, aad, pt) == A.encrypt(A.XCHACHA20_POLY1305{}, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}
114	
115	law xchacha20poly1305.decrypt:
116	  for +key: List<&2, U32>
117	  for +nonce: List<&2, U32>
118	  for +aad: List<&2, U32>
119	  for +data: List<&2, U32>
120	  {CP.xdecrypt(key, nonce, aad, data) == A.decrypt(A.XCHACHA20_POLY1305{}, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
121	
122	# ---- the checked API
123	
124	law encrypt.valid:
125	  for +alg: A.Alg
126	  for +key: List<&2, U32>
127	  for +nonce: List<&2, U32>
128	  for +aad: List<&2, U32>
129	  for +pt: List<&2, U32>
130	  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
131	  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
132	  {A.encrypt(alg, key, nonce, aad, pt) == A.seal(alg, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}
133	
134	law encrypt.invalid:
135	  for +alg: A.Alg
136	  for +key: List<&2, U32>
137	  for +nonce: List<&2, U32>
138	  for +aad: List<&2, U32>
139	  for +pt: List<&2, U32>
140	  for +h: {A.valid(alg, key, nonce) == False{} : Bool}
141	  {A.encrypt(alg, key, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}
142	
143	law decrypt.valid:
144	  for +alg: A.Alg
145	  for +key: List<&2, U32>
146	  for +nonce: List<&2, U32>
147	  for +aad: List<&2, U32>
148	  for +data: List<&2, U32>
149	  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
150	  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
151	  {A.decrypt(alg, key, nonce, aad, data) == A.open(alg, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
152	
153	law decrypt.invalid:
154	  for +alg: A.Alg
155	  for +key: List<&2, U32>
156	  for +nonce: List<&2, U32>
157	  for +aad: List<&2, U32>
158	  for +data: List<&2, U32>
159	  for +h: {A.valid(alg, key, nonce) == False{} : Bool}
160	  {A.decrypt(alg, key, nonce, aad, data) == None{} : Maybe<&2, List<&2, U32>>}
161	
162	# ---- the AEAD properties
163	
164	# decrypt(encrypt(x)) == Some(x).
165	law roundtrip:
166	  for +alg: A.Alg
167	  for +key: List<&2, U32>
168	  for +nonce: List<&2, U32>
169	  for +aad: List<&2, U32>
170	  for +pt: List<&2, U32>
171	  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
172	  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
173	  {decrypt_sealed(alg, key, nonce, aad, A.encrypt(alg, key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
174	
175	# ciphertext || t is rejected for every 16-byte t other than the tag of the
176	# ciphertext under this key, nonce and aad.
177	law forgery:
178	  for +alg: A.Alg
179	  for +key: List<&2, U32>
180	  for +nonce: List<&2, U32>
181	  for +aad: List<&2, U32>
182	  for +ct: List<&2, U32>
183	  for +t: List<&2, U32>
184	  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
185	  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
186	  for +ht: {List.length(&2, U32, t) == 16n : Nat}
187	  for ne: {t != expected_tag(alg, key, nonce, aad, ct) : List<&2, U32>}
188	  {A.decrypt(alg, key, nonce, aad, List.append(&2, U32, ct, t)) == None{} : Maybe<&2, List<&2, U32>>}
189	
190	# What encrypt returns is a ciphertext followed by its expected tag.
191	law seal_layout:
192	  for +alg: A.Alg
193	  for +key: List<&2, U32>
194	  for +nonce: List<&2, U32>
195	  for +aad: List<&2, U32>
196	  for +pt: List<&2, U32>
197	  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
198	  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
199	  exs ct: List<&2, U32>
200	  {A.encrypt(alg, key, nonce, aad, pt) == Some{List.append(&2, U32, ct, expected_tag(alg, key, nonce, aad, ct))} : Maybe<&2, List<&2, U32>>}
201	
202	# Decryption is sound: whatever decrypt accepts is exactly what encrypt
203	# produces for the returned plaintext (so every accepted input is the honest
204	# ciphertext of its plaintext under this key, nonce and aad).
205	law decrypt_sound:
206	  for +alg: A.Alg
207	  for +key: List<&2, U32>
208	  for +nonce: List<&2, U32>
209	  for +aad: List<&2, U32>
210	  for +data: List<&2, U32>
211	  for +p: List<&2, U32>
212	  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
213	  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
214	  for +h: {A.decrypt(alg, key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>}
215	  {A.encrypt(alg, key, nonce, aad, p) == Some{data} : Maybe<&2, List<&2, U32>>}