1	import Base
2	import ../../../src/crypto/aead.bend as A
3	import ../../../src/crypto/aead/chacha20poly1305.bend as CP
4	import ../../../src/crypto/aesgcm.bend as GCM
5	import ../../../spec/crypto/chacha.bend as RC
6	import ../../../spec/crypto/chacha20poly1305.bend as R
7	import ../../../spec/crypto/aes/aes.bend as S
8	import ../../../spec/crypto/aes/gcm.bend as G
9	import ../../lib/nat.bend as N
10	import ./laws.bend as Laws
11	import ./chacha20poly1305.bend as C
12	import ../aes/api.bend as AE
13	import ./sound.bend as SD
14	
15	# Entry point: `bend proofs/crypto/aead/proof.bend` checks the clauses of
16	# laws.bend. Each algorithm-generic clause is proved by one case per
17	# constructor of A.Alg: ChaCha20-Poly1305 and XChaCha20-Poly1305 through
18	# chacha20poly1305.bend, AES-GCM through aes.bend (the AES-GCM API lemmas of
19	# proofs/crypto/aes).
20	
21	# ---- each algorithm is its specification
22	
23	def Laws.chacha20poly1305.seal(key, nonce, aad, pt):
24	  Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, CP.seal(key, nonce, aad, pt), R.seal(key, nonce, aad, pt), C.seal_eq(key, nonce, aad, pt))
25	
26	def Laws.chacha20poly1305.open(key, nonce, aad, data):
27	  C.open_eq(key, nonce, aad, data)
28	
29	def Laws.xchacha20poly1305.seal(key, nonce, aad, pt):
30	  Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, CP.xseal(key, nonce, aad, pt), R.xseal(key, nonce, aad, pt), C.xseal_eq(key, nonce, aad, pt))
31	
32	def Laws.xchacha20poly1305.open(key, nonce, aad, data):
33	  C.xopen_eq(key, nonce, aad, data)
34	
35	def Laws.aes128gcm.seal(key, hk, nonce, hn, aad, pt):
36	  AE.aes128_encrypt_l(key, hk, nonce, hn, aad, pt)
37	
38	def Laws.aes128gcm.open(key, hk, nonce, hn, aad, data):
39	  AE.aes128_decrypt_l(key, hk, nonce, hn, aad, data)
40	
41	def Laws.aes256gcm.seal(key, hk, nonce, hn, aad, pt):
42	  AE.aes256_encrypt_l(key, hk, nonce, hn, aad, pt)
43	
44	def Laws.aes256gcm.open(key, hk, nonce, hn, aad, data):
45	  AE.aes256_decrypt_l(key, hk, nonce, hn, aad, data)
46	
47	law when_same:
48	  for +ok: Bool
49	  for +x: List<&2, U32>
50	  {CP.when(ok, x) == A.when_open(ok, Some{x}) : Maybe<&2, List<&2, U32>>}
51	
52	def when_same(ok, x):
53	  match ok:
54	    case True{}: {==}
55	    case False{}: {==}
56	
57	law when_open_same:
58	  for +ok: Bool
59	  for +r: Maybe<&2, List<&2, U32>>
60	  {CP.when_open(ok, r) == A.when_open(ok, r) : Maybe<&2, List<&2, U32>>}
61	
62	def when_open_same(ok, r):
63	  match ok:
64	    case True{}: {==}
65	    case False{}: {==}
66	
67	def Laws.chacha20poly1305.encrypt(key, nonce, aad, pt):
68	  when_same(CP.lengths_ok(key, nonce, 12n), CP.seal(key, nonce, aad, pt))
69	
70	def Laws.chacha20poly1305.decrypt(key, nonce, aad, data):
71	  when_open_same(CP.lengths_ok(key, nonce, 12n), CP.open(key, nonce, aad, data))
72	
73	def Laws.xchacha20poly1305.encrypt(key, nonce, aad, pt):
74	  when_same(CP.lengths_ok(key, nonce, 24n), CP.xseal(key, nonce, aad, pt))
75	
76	def Laws.xchacha20poly1305.decrypt(key, nonce, aad, data):
77	  when_open_same(CP.lengths_ok(key, nonce, 24n), CP.xopen(key, nonce, aad, data))
78	
79	# ---- the checked API
80	
81	law valid_true:
82	  for +alg: A.Alg
83	  for +key: List<&2, U32>
84	  for +nonce: List<&2, U32>
85	  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
86	  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
87	  {A.valid(alg, key, nonce) == True{} : Bool}
88	
89	def valid_true(alg, key, nonce, hk, hn):
90	  %Equal.sym(Nat, List.length(&2, U32, key), A.key_size(alg), hk) :
91	    {Bool.and(Nat.is_eq(_, A.key_size(alg)), Nat.is_eq(List.length(&2, U32, nonce), A.nonce_size(alg))) == True{} : Bool}
92	  %Equal.sym(Nat, List.length(&2, U32, nonce), A.nonce_size(alg), hn) :
93	    {Bool.and(Nat.is_eq(A.key_size(alg), A.key_size(alg)), Nat.is_eq(_, A.nonce_size(alg))) == True{} : Bool}
94	  %Equal.sym(Bool, Nat.is_eq(A.key_size(alg), A.key_size(alg)), True{}, N.is_eq_refl(A.key_size(alg))) :
95	    {Bool.and(_, Nat.is_eq(A.nonce_size(alg), A.nonce_size(alg))) == True{} : Bool}
96	  N.is_eq_refl(A.nonce_size(alg))
97	
98	law encrypt_valid:
99	  for +alg: A.Alg
100	  for +key: List<&2, U32>
101	  for +nonce: List<&2, U32>
102	  for +aad: List<&2, U32>
103	  for +pt: List<&2, U32>
104	  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
105	  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
106	  {A.encrypt(alg, key, nonce, aad, pt) == A.seal(alg, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}
107	
108	def encrypt_valid(alg, key, nonce, aad, pt, hk, hn):
109	  %Equal.sym(Bool, A.valid(alg, key, nonce), True{}, valid_true(alg, key, nonce, hk, hn)) :
110	    {A.when_open(_, A.seal(alg, key, nonce, aad, pt)) == A.seal(alg, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}
111	  {==}
112	
113	def Laws.encrypt.valid(alg, key, nonce, aad, pt, hk, hn):
114	  encrypt_valid(alg, key, nonce, aad, pt, hk, hn)
115	
116	def Laws.encrypt.invalid(alg, key, nonce, aad, pt, h):
117	  %Equal.sym(Bool, A.valid(alg, key, nonce), False{}, h) :
118	    {A.when_open(_, A.seal(alg, key, nonce, aad, pt)) == None{} : Maybe<&2, List<&2, U32>>}
119	  {==}
120	
121	law decrypt_valid:
122	  for +alg: A.Alg
123	  for +key: List<&2, U32>
124	  for +nonce: List<&2, U32>
125	  for +aad: List<&2, U32>
126	  for +data: List<&2, U32>
127	  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
128	  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
129	  {A.decrypt(alg, key, nonce, aad, data) == A.open(alg, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
130	
131	def decrypt_valid(alg, key, nonce, aad, data, hk, hn):
132	  %Equal.sym(Bool, A.valid(alg, key, nonce), True{}, valid_true(alg, key, nonce, hk, hn)) :
133	    {A.when_open(_, A.open(alg, key, nonce, aad, data)) == A.open(alg, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
134	  {==}
135	
136	def Laws.decrypt.valid(alg, key, nonce, aad, data, hk, hn):
137	  decrypt_valid(alg, key, nonce, aad, data, hk, hn)
138	
139	def Laws.decrypt.invalid(alg, key, nonce, aad, data, h):
140	  %Equal.sym(Bool, A.valid(alg, key, nonce), False{}, h) :
141	    {A.when_open(_, A.open(alg, key, nonce, aad, data)) == None{} : Maybe<&2, List<&2, U32>>}
142	  {==}
143	
144	# ---- round trip
145	
146	# decrypt after encrypt is open after seal (on valid lengths).
147	def open_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>>:
148	  match m:
149	    case None{}: None{}
150	    case Some{c}: A.open(alg, key, nonce, aad, c)
151	
152	law ds_open:
153	  for +alg: A.Alg
154	  for +key: List<&2, U32>
155	  for +nonce: List<&2, U32>
156	  for +aad: List<&2, U32>
157	  for +m: Maybe<&2, List<&2, U32>>
158	  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
159	  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
160	  {Laws.decrypt_sealed(alg, key, nonce, aad, m) == open_sealed(alg, key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}
161	
162	def ds_open(alg, key, nonce, aad, m, hk, hn):
163	  match m:
164	    case None{}: {==}
165	    case Some{c}: decrypt_valid(alg, key, nonce, aad, c, hk, hn)
166	
167	law os128:
168	  for +key: List<&2, U32>
169	  for +nonce: List<&2, U32>
170	  for +aad: List<&2, U32>
171	  for +m: Maybe<&2, List<&2, U32>>
172	  {open_sealed(A.AES_128_GCM{}, key, nonce, aad, m) == AE.open128(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}
173	
174	def os128(key, nonce, aad, m):
175	  match m:
176	    case None{}: {==}
177	    case Some{c}: {==}
178	
179	law os256:
180	  for +key: List<&2, U32>
181	  for +nonce: List<&2, U32>
182	  for +aad: List<&2, U32>
183	  for +m: Maybe<&2, List<&2, U32>>
184	  {open_sealed(A.AES_256_GCM{}, key, nonce, aad, m) == AE.open256(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}
185	
186	def os256(key, nonce, aad, m):
187	  match m:
188	    case None{}: {==}
189	    case Some{c}: {==}
190	
191	law open_seal:
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	  {open_sealed(alg, key, nonce, aad, A.seal(alg, key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
200	
201	def open_seal(alg, key, nonce, aad, pt, hk, hn):
202	  match alg:
203	    case A.CHACHA20_POLY1305{}: C.iroundtrip(key, nonce, aad, pt)
204	    case A.XCHACHA20_POLY1305{}: C.iroundtrip(CP.xkey(key, nonce), CP.xnonce(nonce), aad, pt)
205	    case A.AES_128_GCM{}:
206	      Equal.trans(Maybe<&2, List<&2, U32>>, open_sealed(A.AES_128_GCM{}, key, nonce, aad, GCM.aes128_gcm_encrypt(key, nonce, aad, pt)), AE.open128(key, nonce, aad, GCM.aes128_gcm_encrypt(key, nonce, aad, pt)), Some{pt},
207	        os128(key, nonce, aad, GCM.aes128_gcm_encrypt(key, nonce, aad, pt)),
208	        AE.aes128_roundtrip_l(key, hk, nonce, hn, aad, pt))
209	    case A.AES_256_GCM{}:
210	      Equal.trans(Maybe<&2, List<&2, U32>>, open_sealed(A.AES_256_GCM{}, key, nonce, aad, GCM.aes256_gcm_encrypt(key, nonce, aad, pt)), AE.open256(key, nonce, aad, GCM.aes256_gcm_encrypt(key, nonce, aad, pt)), Some{pt},
211	        os256(key, nonce, aad, GCM.aes256_gcm_encrypt(key, nonce, aad, pt)),
212	        AE.aes256_roundtrip_l(key, hk, nonce, hn, aad, pt))
213	
214	def Laws.roundtrip(alg, key, nonce, aad, pt, hk, hn):
215	  +E = A.encrypt(alg, key, nonce, aad, pt)
216	  +SE = A.seal(alg, key, nonce, aad, pt)
217	  Equal.trans(Maybe<&2, List<&2, U32>>, Laws.decrypt_sealed(alg, key, nonce, aad, E), open_sealed(alg, key, nonce, aad, E), Some{pt},
218	    ds_open(alg, key, nonce, aad, E, hk, hn),
219	    Equal.trans(Maybe<&2, List<&2, U32>>, open_sealed(alg, key, nonce, aad, E), open_sealed(alg, key, nonce, aad, SE), Some{pt},
220	      Equal.cong(Maybe<&2, List<&2, U32>>, Maybe<&2, List<&2, U32>>, m => open_sealed(alg, key, nonce, aad, m), E, SE, encrypt_valid(alg, key, nonce, aad, pt, hk, hn)),
221	      open_seal(alg, key, nonce, aad, pt, hk, hn)))
222	
223	# ---- forgery
224	
225	law open_forged:
226	  for +alg: A.Alg
227	  for +key: List<&2, U32>
228	  for +nonce: List<&2, U32>
229	  for +aad: List<&2, U32>
230	  for +ct: List<&2, U32>
231	  for +t: List<&2, U32>
232	  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
233	  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
234	  for +ht: {List.length(&2, U32, t) == 16n : Nat}
235	  for ne: {t != Laws.expected_tag(alg, key, nonce, aad, ct) : List<&2, U32>}
236	  {A.open(alg, key, nonce, aad, List.append(&2, U32, ct, t)) == None{} : Maybe<&2, List<&2, U32>>}
237	
238	def open_forged(alg, key, nonce, aad, ct, t, hk, hn, ht, ne):
239	  match alg:
240	    case A.CHACHA20_POLY1305{}:
241	      Equal.trans(Maybe<&2, List<&2, U32>>, CP.open(key, nonce, aad, List.append(&2, U32, ct, t)), R.open(key, nonce, aad, List.append(&2, U32, ct, t)), None{},
242	        C.open_eq(key, nonce, aad, List.append(&2, U32, ct, t)),
243	        C.forgery(key, nonce, aad, ct, t, ht, ne))
244	    case A.XCHACHA20_POLY1305{}:
245	      Equal.trans(Maybe<&2, List<&2, U32>>, CP.xopen(key, nonce, aad, List.append(&2, U32, ct, t)), R.xopen(key, nonce, aad, List.append(&2, U32, ct, t)), None{},
246	        C.xopen_eq(key, nonce, aad, List.append(&2, U32, ct, t)),
247	        C.forgery(RC.xsubkey(key, nonce), RC.xnonce(nonce), aad, ct, t, ht, ne))
248	    case A.AES_128_GCM{}: AE.aes128_forgery_l(key, hk, nonce, hn, aad, ct, t, ht, ne)
249	    case A.AES_256_GCM{}: AE.aes256_forgery_l(key, hk, nonce, hn, aad, ct, t, ht, ne)
250	
251	def Laws.forgery(alg, key, nonce, aad, ct, t, hk, hn, ht, ne):
252	  Equal.trans(Maybe<&2, List<&2, U32>>, A.decrypt(alg, key, nonce, aad, List.append(&2, U32, ct, t)), A.open(alg, key, nonce, aad, List.append(&2, U32, ct, t)), None{},
253	    decrypt_valid(alg, key, nonce, aad, List.append(&2, U32, ct, t), hk, hn),
254	    open_forged(alg, key, nonce, aad, ct, t, hk, hn, ht, ne))
255	
256	# ---- layout
257	
258	def sapp(+ct: List<&2, U32>, +t: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
259	  Some{List.append(&2, U32, ct, t)}
260	
261	law layout_cp:
262	  for +key: List<&2, U32>
263	  for +nonce: List<&2, U32>
264	  for +aad: List<&2, U32>
265	  for +pt: List<&2, U32>
266	  {A.seal(A.CHACHA20_POLY1305{}, key, nonce, aad, pt) == sapp(CP.encrypt_ct(key, nonce, pt), R.tag(key, nonce, aad, CP.encrypt_ct(key, nonce, pt))) : Maybe<&2, List<&2, U32>>}
267	
268	def layout_cp(key, nonce, aad, pt):
269	  +ct = CP.encrypt_ct(key, nonce, pt)
270	  Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => sapp(ct, l), CP.tag(key, nonce, aad, ct), R.tag(key, nonce, aad, ct), C.tag_eq(key, nonce, aad, ct))
271	
272	law layout_x:
273	  for +key: List<&2, U32>
274	  for +nonce: List<&2, U32>
275	  for +aad: List<&2, U32>
276	  for +pt: List<&2, U32>
277	  {A.seal(A.XCHACHA20_POLY1305{}, key, nonce, aad, pt) == sapp(CP.encrypt_ct(CP.xkey(key, nonce), CP.xnonce(nonce), pt), R.tag(RC.xsubkey(key, nonce), RC.xnonce(nonce), aad, CP.encrypt_ct(CP.xkey(key, nonce), CP.xnonce(nonce), pt))) : Maybe<&2, List<&2, U32>>}
278	
279	def layout_x(key, nonce, aad, pt):
280	  +k = CP.xkey(key, nonce)
281	  +n = CP.xnonce(nonce)
282	  +ct = CP.encrypt_ct(k, n, pt)
283	  Equal.trans(Maybe<&2, List<&2, U32>>, sapp(ct, CP.tag(k, n, aad, ct)), sapp(ct, R.tag(k, n, aad, ct)), sapp(ct, R.tag(RC.xsubkey(key, nonce), RC.xnonce(nonce), aad, ct)),
284	    Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => sapp(ct, l), CP.tag(k, n, aad, ct), R.tag(k, n, aad, ct), C.tag_eq(k, n, aad, ct)),
285	    Equal.trans(Maybe<&2, List<&2, U32>>, sapp(ct, R.tag(k, n, aad, ct)), sapp(ct, R.tag(RC.xsubkey(key, nonce), n, aad, ct)), sapp(ct, R.tag(RC.xsubkey(key, nonce), RC.xnonce(nonce), aad, ct)),
286	      Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => sapp(ct, R.tag(l, n, aad, ct)), k, RC.xsubkey(key, nonce), C.xkey_eq(key, nonce)),
287	      Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => sapp(ct, R.tag(RC.xsubkey(key, nonce), l, aad, ct)), n, RC.xnonce(nonce), C.xnonce_eq(nonce))))
288	
289	def gct(+key: List<&2, U32>, +nonce: List<&2, U32>, +pt: List<&2, U32>) -> List<&2, U32>:
290	  G.gctr(S.nk(key), S.nr(key), key, pt, G.inc32(G.j0(nonce)))
291	
292	def Laws.seal_layout(alg, key, nonce, aad, pt, hk, hn):
293	  match alg:
294	    case A.CHACHA20_POLY1305{}:
295	      (CP.encrypt_ct(key, nonce, pt), Equal.trans(Maybe<&2, List<&2, U32>>, A.encrypt(A.CHACHA20_POLY1305{}, key, nonce, aad, pt), A.seal(A.CHACHA20_POLY1305{}, key, nonce, aad, pt), sapp(CP.encrypt_ct(key, nonce, pt), R.tag(key, nonce, aad, CP.encrypt_ct(key, nonce, pt))),
296	        encrypt_valid(A.CHACHA20_POLY1305{}, key, nonce, aad, pt, hk, hn), layout_cp(key, nonce, aad, pt)))
297	    case A.XCHACHA20_POLY1305{}:
298	      (CP.encrypt_ct(CP.xkey(key, nonce), CP.xnonce(nonce), pt), Equal.trans(Maybe<&2, List<&2, U32>>, A.encrypt(A.XCHACHA20_POLY1305{}, key, nonce, aad, pt), A.seal(A.XCHACHA20_POLY1305{}, key, nonce, aad, pt), sapp(CP.encrypt_ct(CP.xkey(key, nonce), CP.xnonce(nonce), pt), R.tag(RC.xsubkey(key, nonce), RC.xnonce(nonce), aad, CP.encrypt_ct(CP.xkey(key, nonce), CP.xnonce(nonce), pt))),
299	        encrypt_valid(A.XCHACHA20_POLY1305{}, key, nonce, aad, pt, hk, hn), layout_x(key, nonce, aad, pt)))
300	    case A.AES_128_GCM{}:
301	      (gct(key, nonce, pt), Equal.trans(Maybe<&2, List<&2, U32>>, A.encrypt(A.AES_128_GCM{}, key, nonce, aad, pt), A.seal(A.AES_128_GCM{}, key, nonce, aad, pt), Some{G.aes_seal(key, nonce, aad, pt)},
302	        encrypt_valid(A.AES_128_GCM{}, key, nonce, aad, pt, hk, hn), AE.aes128_encrypt_l(key, hk, nonce, hn, aad, pt)))
303	    case A.AES_256_GCM{}:
304	      (gct(key, nonce, pt), Equal.trans(Maybe<&2, List<&2, U32>>, A.encrypt(A.AES_256_GCM{}, key, nonce, aad, pt), A.seal(A.AES_256_GCM{}, key, nonce, aad, pt), Some{G.aes_seal(key, nonce, aad, pt)},
305	        encrypt_valid(A.AES_256_GCM{}, key, nonce, aad, pt, hk, hn), AE.aes256_encrypt_l(key, hk, nonce, hn, aad, pt)))
306	
307	# ---- soundness of decryption
308	
309	def smaybe(+x: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
310	  Some{x}
311	
312	law open_sound:
313	  for +alg: A.Alg
314	  for +key: List<&2, U32>
315	  for +nonce: List<&2, U32>
316	  for +aad: List<&2, U32>
317	  for +data: List<&2, U32>
318	  for +p: List<&2, U32>
319	  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
320	  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
321	  for +h: {A.open(alg, key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>}
322	  {A.seal(alg, key, nonce, aad, p) == Some{data} : Maybe<&2, List<&2, U32>>}
323	
324	def open_sound(alg, key, nonce, aad, data, p, hk, hn, h):
325	  match alg:
326	    case A.CHACHA20_POLY1305{}:
327	      +hs = Equal.trans(Maybe<&2, List<&2, U32>>, R.open(key, nonce, aad, data), CP.open(key, nonce, aad, data), Some{p}, Equal.sym(Maybe<&2, List<&2, U32>>, CP.open(key, nonce, aad, data), R.open(key, nonce, aad, data), C.open_eq(key, nonce, aad, data)), h)
328	      Equal.trans(Maybe<&2, List<&2, U32>>, smaybe(CP.seal(key, nonce, aad, p)), smaybe(R.seal(key, nonce, aad, p)), Some{data},
329	        Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => smaybe(l), CP.seal(key, nonce, aad, p), R.seal(key, nonce, aad, p), C.seal_eq(key, nonce, aad, p)),
330	        Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => smaybe(l), R.seal(key, nonce, aad, p), data, SD.chacha_sound(key, nonce, aad, data, p, hs)))
331	    case A.XCHACHA20_POLY1305{}:
332	      +hs = Equal.trans(Maybe<&2, List<&2, U32>>, R.xopen(key, nonce, aad, data), CP.xopen(key, nonce, aad, data), Some{p}, Equal.sym(Maybe<&2, List<&2, U32>>, CP.xopen(key, nonce, aad, data), R.xopen(key, nonce, aad, data), C.xopen_eq(key, nonce, aad, data)), h)
333	      Equal.trans(Maybe<&2, List<&2, U32>>, smaybe(CP.xseal(key, nonce, aad, p)), smaybe(R.xseal(key, nonce, aad, p)), Some{data},
334	        Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => smaybe(l), CP.xseal(key, nonce, aad, p), R.xseal(key, nonce, aad, p), C.xseal_eq(key, nonce, aad, p)),
335	        Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => smaybe(l), R.xseal(key, nonce, aad, p), data, SD.chacha_sound(RC.xsubkey(key, nonce), RC.xnonce(nonce), aad, data, p, hs)))
336	    case A.AES_128_GCM{}:
337	      +hs = Equal.trans(Maybe<&2, List<&2, U32>>, G.aes_open(key, nonce, aad, data), GCM.aes128_gcm_decrypt(key, nonce, aad, data), Some{p}, Equal.sym(Maybe<&2, List<&2, U32>>, GCM.aes128_gcm_decrypt(key, nonce, aad, data), G.aes_open(key, nonce, aad, data), AE.aes128_decrypt_l(key, hk, nonce, hn, aad, data)), h)
338	      Equal.trans(Maybe<&2, List<&2, U32>>, GCM.aes128_gcm_encrypt(key, nonce, aad, p), smaybe(G.aes_seal(key, nonce, aad, p)), Some{data},
339	        AE.aes128_encrypt_l(key, hk, nonce, hn, aad, p),
340	        Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => smaybe(l), G.aes_seal(key, nonce, aad, p), data, SD.gcm_sound(S.nk(key), S.nr(key), key, nonce, aad, data, p, hs)))
341	    case A.AES_256_GCM{}:
342	      +hs = Equal.trans(Maybe<&2, List<&2, U32>>, G.aes_open(key, nonce, aad, data), GCM.aes256_gcm_decrypt(key, nonce, aad, data), Some{p}, Equal.sym(Maybe<&2, List<&2, U32>>, GCM.aes256_gcm_decrypt(key, nonce, aad, data), G.aes_open(key, nonce, aad, data), AE.aes256_decrypt_l(key, hk, nonce, hn, aad, data)), h)
343	      Equal.trans(Maybe<&2, List<&2, U32>>, GCM.aes256_gcm_encrypt(key, nonce, aad, p), smaybe(G.aes_seal(key, nonce, aad, p)), Some{data},
344	        AE.aes256_encrypt_l(key, hk, nonce, hn, aad, p),
345	        Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => smaybe(l), G.aes_seal(key, nonce, aad, p), data, SD.gcm_sound(S.nk(key), S.nr(key), key, nonce, aad, data, p, hs)))
346	
347	def Laws.decrypt_sound(alg, key, nonce, aad, data, p, hk, hn, h):
348	  +ho = Equal.trans(Maybe<&2, List<&2, U32>>, A.open(alg, key, nonce, aad, data), A.decrypt(alg, key, nonce, aad, data), Some{p},
349	    Equal.sym(Maybe<&2, List<&2, U32>>, A.decrypt(alg, key, nonce, aad, data), A.open(alg, key, nonce, aad, data), decrypt_valid(alg, key, nonce, aad, data, hk, hn)), h)
350	  Equal.trans(Maybe<&2, List<&2, U32>>, A.encrypt(alg, key, nonce, aad, p), A.seal(alg, key, nonce, aad, p), Some{data},
351	    encrypt_valid(alg, key, nonce, aad, p, hk, hn),
352	    open_sound(alg, key, nonce, aad, data, p, hk, hn, ho))