proofs/crypto/aead/proof.bend

bend-collections-laws-crypto@1.0.0.0 · 352 lines · 17 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/aead.bend as A
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/aead/chacha20poly1305.bend as CP
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/aesgcm.bend as GCM
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as RC
6import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha20poly1305.bend as R
7import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S
8import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend as Laws
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend as C
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/api.bend as AE
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/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
23def 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
26def Laws.chacha20poly1305.open(key, nonce, aad, data):
27  C.open_eq(key, nonce, aad, data)
28
29def 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
32def Laws.xchacha20poly1305.open(key, nonce, aad, data):
33  C.xopen_eq(key, nonce, aad, data)
34
35def Laws.aes128gcm.seal(key, hk, nonce, hn, aad, pt):
36  AE.aes128_encrypt_l(key, hk, nonce, hn, aad, pt)
37
38def Laws.aes128gcm.open(key, hk, nonce, hn, aad, data):
39  AE.aes128_decrypt_l(key, hk, nonce, hn, aad, data)
40
41def Laws.aes256gcm.seal(key, hk, nonce, hn, aad, pt):
42  AE.aes256_encrypt_l(key, hk, nonce, hn, aad, pt)
43
44def Laws.aes256gcm.open(key, hk, nonce, hn, aad, data):
45  AE.aes256_decrypt_l(key, hk, nonce, hn, aad, data)
46
47law 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
52def when_same(ok, x):
53  match ok:
54    case True{}: {==}
55    case False{}: {==}
56
57law 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
62def when_open_same(ok, r):
63  match ok:
64    case True{}: {==}
65    case False{}: {==}
66
67def Laws.chacha20poly1305.encrypt(key, nonce, aad, pt):
68  when_same(CP.lengths_ok(key, nonce, 12n), CP.seal(key, nonce, aad, pt))
69
70def Laws.chacha20poly1305.decrypt(key, nonce, aad, data):
71  when_open_same(CP.lengths_ok(key, nonce, 12n), CP.open(key, nonce, aad, data))
72
73def Laws.xchacha20poly1305.encrypt(key, nonce, aad, pt):
74  when_same(CP.lengths_ok(key, nonce, 24n), CP.xseal(key, nonce, aad, pt))
75
76def 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
81law 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
89def 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
98law 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
108def 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
113def Laws.encrypt.valid(alg, key, nonce, aad, pt, hk, hn):
114  encrypt_valid(alg, key, nonce, aad, pt, hk, hn)
115
116def 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
121law 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
131def 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
136def Laws.decrypt.valid(alg, key, nonce, aad, data, hk, hn):
137  decrypt_valid(alg, key, nonce, aad, data, hk, hn)
138
139def 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).
147def 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
152law 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
162def 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
167law 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
174def os128(key, nonce, aad, m):
175  match m:
176    case None{}: {==}
177    case Some{c}: {==}
178
179law 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
186def os256(key, nonce, aad, m):
187  match m:
188    case None{}: {==}
189    case Some{c}: {==}
190
191law 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
201def 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
214def 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
225law 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
238def 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
251def 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
258def sapp(+ct: List<&2, U32>, +t: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
259  Some{List.append(&2, U32, ct, t)}
260
261law 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
268def 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
272law 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
279def 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
289def 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
292def 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
309def smaybe(+x: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
310  Some{x}
311
312law 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
324def 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
347def 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))