1	import Base
2	# (imported first: Bend 2.0.34 overflows its stack checking this module after
3	# proofs/crypto/chacha/core.bend, but not before it)
4	import ../poly1305/mac.bend as PM
5	import ../../../src/crypto/chacha/chacha20.bend as CH
6	import ../../../src/crypto/aead/chacha20poly1305.bend as I
7	import ../../../src/crypto/subtle.bend as S
8	import ../../../spec/crypto/chacha.bend as RC
9	import ../../../spec/crypto/poly1305.bend as RP
10	import ../../../spec/crypto/subtle.bend as RS
11	import ../../../spec/crypto/chacha20poly1305.bend as R
12	import ../../lib/logic.bend as L
13	import ../../lib/nat.bend as N
14	import ../chacha/stream.bend as T
15	import ../chacha/xchacha.bend as X
16	import ../chacha/involution.bend as V
17	import ./subtle_eq.bend as SE
18	
19	# ChaCha20-Poly1305 and XChaCha20-Poly1305 of src/crypto/aead/ against
20	# spec/crypto/chacha20poly1305.bend (for every key, nonce, aad and message
21	# list), and the two properties of the specification: opening a sealed
22	# message gives the plaintext back, and opening ciphertext || t fails for
23	# every 16-byte t other than the tag of the ciphertext. The composition
24	# follows HACL*'s Spec.Chacha20Poly1305 / Hacl.Impl.Chacha20Poly1305 and the
25	# EasyCrypt proof of Almeida et al. 2020 (the AEAD is its two primitives
26	# plus framing), the primitives being proved in proofs/crypto/chacha and
27	# proofs/crypto/poly1305.
28	
29	# ---------------------------------------------------------------- implementation == specification
30	
31	law poly_key_eq:
32	  for +key: List<&2, U32>
33	  for +nonce: List<&2, U32>
34	  {I.poly_key(key, nonce) == R.poly_key(key, nonce) : List<&2, U32>}
35	
36	def poly_key_eq(key, nonce):
37	  Equal.trans(List<&2, U32>, CH.take(32n, CH.block_rounds(10n, key, 0, nonce)), RC.prefix(32n, CH.block_rounds(10n, key, 0, nonce)), RC.prefix(32n, RC.block(key, 0, nonce)),
38	    T.take_eq(32n, CH.block_rounds(10n, key, 0, nonce)),
39	    Equal.cong(List<&2, U32>, List<&2, U32>, l => RC.prefix(32n, l), CH.block_rounds(10n, key, 0, nonce), RC.block(key, 0, nonce), T.block_rounds_correct(10n, key, 0, nonce)))
40	
41	law mac_data_eq:
42	  for +aad: List<&2, U32>
43	  for +ct: List<&2, U32>
44	  {I.mac_data(aad, ct) == R.mac_data(aad, ct) : List<&2, U32>}
45	
46	def mac_data_eq(aad, ct):
47	  {==}
48	
49	law tag_eq:
50	  for +key: List<&2, U32>
51	  for +nonce: List<&2, U32>
52	  for +aad: List<&2, U32>
53	  for +ct: List<&2, U32>
54	  {I.tag(key, nonce, aad, ct) == R.tag(key, nonce, aad, ct) : List<&2, U32>}
55	
56	def tag_eq(key, nonce, aad, ct):
57	  Equal.trans(List<&2, U32>, I.tag(key, nonce, aad, ct), RP.mac(I.poly_key(key, nonce), I.mac_data(aad, ct)), R.tag(key, nonce, aad, ct),
58	    PM.mac_correct(I.poly_key(key, nonce), I.mac_data(aad, ct)),
59	    Equal.trans(List<&2, U32>, RP.mac(I.poly_key(key, nonce), I.mac_data(aad, ct)), RP.mac(R.poly_key(key, nonce), I.mac_data(aad, ct)), R.tag(key, nonce, aad, ct),
60	      Equal.cong(List<&2, U32>, List<&2, U32>, l => RP.mac(l, I.mac_data(aad, ct)), I.poly_key(key, nonce), R.poly_key(key, nonce), poly_key_eq(key, nonce)),
61	      Equal.cong(List<&2, U32>, List<&2, U32>, l => RP.mac(R.poly_key(key, nonce), l), I.mac_data(aad, ct), R.mac_data(aad, ct), mac_data_eq(aad, ct))))
62	
63	def iseal(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +ct: List<&2, U32>) -> List<&2, U32>:
64	  List.append(&2, U32, ct, I.tag(key, nonce, aad, ct))
65	
66	law seal_eq:
67	  for +key: List<&2, U32>
68	  for +nonce: List<&2, U32>
69	  for +aad: List<&2, U32>
70	  for +pt: List<&2, U32>
71	  {I.seal(key, nonce, aad, pt) == R.seal(key, nonce, aad, pt) : List<&2, U32>}
72	
73	def seal_eq(key, nonce, aad, pt):
74	  +ci = CH.encrypt_rounds(10n, key, 1, nonce, pt)
75	  +cr = RC.encrypt(key, 1, nonce, pt)
76	  Equal.trans(List<&2, U32>, iseal(key, nonce, aad, ci), iseal(key, nonce, aad, cr), R.seal(key, nonce, aad, pt),
77	    Equal.cong(List<&2, U32>, List<&2, U32>, l => iseal(key, nonce, aad, l), ci, cr, T.encrypt_correct(10n, key, 1, nonce, pt)),
78	    Equal.cong(List<&2, U32>, List<&2, U32>, l => List.append(&2, U32, cr, l), I.tag(key, nonce, aad, cr), R.tag(key, nonce, aad, cr), tag_eq(key, nonce, aad, cr)))
79	
80	law open_tag_eq:
81	  for +ok: Bool
82	  for +key: List<&2, U32>
83	  for +nonce: List<&2, U32>
84	  for +ct: List<&2, U32>
85	  {I.open_tag(ok, key, nonce, ct) == R.open_tag(ok, key, nonce, ct) : Maybe<&2, List<&2, U32>>}
86	
87	def open_tag_eq(ok, key, nonce, ct):
88	  match ok:
89	    case True{}:
90	      Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, CH.encrypt_rounds(10n, key, 1, nonce, ct), RC.encrypt(key, 1, nonce, ct), T.encrypt_correct(10n, key, 1, nonce, ct))
91	    case False{}: {==}
92	
93	law open_split_eq:
94	  for +key: List<&2, U32>
95	  for +nonce: List<&2, U32>
96	  for +aad: List<&2, U32>
97	  for +ct: List<&2, U32>
98	  for +t: List<&2, U32>
99	  {I.open_split(key, nonce, aad, ct, t) == R.open_split(key, nonce, aad, ct, t) : Maybe<&2, List<&2, U32>>}
100	
101	def open_split_eq(key, nonce, aad, ct, t):
102	  Equal.trans(Maybe<&2, List<&2, U32>>, I.open_tag(S.eq(t, I.tag(key, nonce, aad, ct)), key, nonce, ct), I.open_tag(RS.equal(t, R.tag(key, nonce, aad, ct)), key, nonce, ct), R.open_split(key, nonce, aad, ct, t),
103	    Equal.trans(Maybe<&2, List<&2, U32>>, I.open_tag(S.eq(t, I.tag(key, nonce, aad, ct)), key, nonce, ct), I.open_tag(RS.equal(t, I.tag(key, nonce, aad, ct)), key, nonce, ct), I.open_tag(RS.equal(t, R.tag(key, nonce, aad, ct)), key, nonce, ct),
104	      Equal.cong(Bool, Maybe<&2, List<&2, U32>>, b => I.open_tag(b, key, nonce, ct), S.eq(t, I.tag(key, nonce, aad, ct)), RS.equal(t, I.tag(key, nonce, aad, ct)), SE.eq_value(t, I.tag(key, nonce, aad, ct))),
105	      Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => I.open_tag(RS.equal(t, l), key, nonce, ct), I.tag(key, nonce, aad, ct), R.tag(key, nonce, aad, ct), tag_eq(key, nonce, aad, ct))),
106	    open_tag_eq(RS.equal(t, R.tag(key, nonce, aad, ct)), key, nonce, ct))
107	
108	law open_len_eq:
109	  for +short: Bool
110	  for +key: List<&2, U32>
111	  for +nonce: List<&2, U32>
112	  for +aad: List<&2, U32>
113	  for +data: List<&2, U32>
114	  {I.open_len(short, key, nonce, aad, data) == R.open_len(short, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
115	
116	def ospl(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +ct: List<&2, U32>, +t: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
117	  I.open_split(key, nonce, aad, ct, t)
118	
119	def open_len_eq(short, key, nonce, aad, data):
120	  match short:
121	    case True{}: {==}
122	    case False{}:
123	      +n = Nat.sub(List.length(&2, U32, data), 16n)
124	      Equal.trans(Maybe<&2, List<&2, U32>>, ospl(key, nonce, aad, CH.take(n, data), CH.skip(n, data)), ospl(key, nonce, aad, RC.prefix(n, data), RC.suffix(n, data)), R.open_split(key, nonce, aad, RC.prefix(n, data), RC.suffix(n, data)),
125	        Equal.trans(Maybe<&2, List<&2, U32>>, ospl(key, nonce, aad, CH.take(n, data), CH.skip(n, data)), ospl(key, nonce, aad, RC.prefix(n, data), CH.skip(n, data)), ospl(key, nonce, aad, RC.prefix(n, data), RC.suffix(n, data)),
126	          Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => ospl(key, nonce, aad, l, CH.skip(n, data)), CH.take(n, data), RC.prefix(n, data), T.take_eq(n, data)),
127	          Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => ospl(key, nonce, aad, RC.prefix(n, data), l), CH.skip(n, data), RC.suffix(n, data), T.skip_eq(n, data))),
128	        open_split_eq(key, nonce, aad, RC.prefix(n, data), RC.suffix(n, data)))
129	
130	law open_eq:
131	  for +key: List<&2, U32>
132	  for +nonce: List<&2, U32>
133	  for +aad: List<&2, U32>
134	  for +data: List<&2, U32>
135	  {I.open(key, nonce, aad, data) == R.open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
136	
137	def open_eq(key, nonce, aad, data):
138	  open_len_eq(Nat.is_lt(List.length(&2, U32, data), 16n), key, nonce, aad, data)
139	
140	law xkey_eq:
141	  for +key: List<&2, U32>
142	  for +nonce: List<&2, U32>
143	  {I.xkey(key, nonce) == RC.xsubkey(key, nonce) : List<&2, U32>}
144	
145	def xkey_eq(key, nonce):
146	  Equal.trans(List<&2, U32>, CH.hchacha20_unchecked(key, CH.take(16n, nonce)), RC.hchacha20(key, CH.take(16n, nonce)), RC.hchacha20(key, RC.prefix(16n, nonce)),
147	    X.hchacha20_correct(key, CH.take(16n, nonce)),
148	    Equal.cong(List<&2, U32>, List<&2, U32>, l => RC.hchacha20(key, l), CH.take(16n, nonce), RC.prefix(16n, nonce), T.take_eq(16n, nonce)))
149	
150	law xnonce_eq:
151	  for +nonce: List<&2, U32>
152	  {I.xnonce(nonce) == RC.xnonce(nonce) : List<&2, U32>}
153	
154	def xnonce_eq(nonce):
155	  Equal.cong(List<&2, U32>, List<&2, U32>, l => 0 <> 0 <> 0 <> 0 <> l, CH.skip(16n, nonce), RC.suffix(16n, nonce), T.skip_eq(16n, nonce))
156	
157	law xseal_eq:
158	  for +key: List<&2, U32>
159	  for +nonce: List<&2, U32>
160	  for +aad: List<&2, U32>
161	  for +pt: List<&2, U32>
162	  {I.xseal(key, nonce, aad, pt) == R.xseal(key, nonce, aad, pt) : List<&2, U32>}
163	
164	def xseal_eq(key, nonce, aad, pt):
165	  Equal.trans(List<&2, U32>, I.seal(I.xkey(key, nonce), I.xnonce(nonce), aad, pt), R.seal(I.xkey(key, nonce), I.xnonce(nonce), aad, pt), R.xseal(key, nonce, aad, pt),
166	    seal_eq(I.xkey(key, nonce), I.xnonce(nonce), aad, pt),
167	    Equal.trans(List<&2, U32>, R.seal(I.xkey(key, nonce), I.xnonce(nonce), aad, pt), R.seal(RC.xsubkey(key, nonce), I.xnonce(nonce), aad, pt), R.xseal(key, nonce, aad, pt),
168	      Equal.cong(List<&2, U32>, List<&2, U32>, l => R.seal(l, I.xnonce(nonce), aad, pt), I.xkey(key, nonce), RC.xsubkey(key, nonce), xkey_eq(key, nonce)),
169	      Equal.cong(List<&2, U32>, List<&2, U32>, l => R.seal(RC.xsubkey(key, nonce), l, aad, pt), I.xnonce(nonce), RC.xnonce(nonce), xnonce_eq(nonce))))
170	
171	law xopen_eq:
172	  for +key: List<&2, U32>
173	  for +nonce: List<&2, U32>
174	  for +aad: List<&2, U32>
175	  for +data: List<&2, U32>
176	  {I.xopen(key, nonce, aad, data) == R.xopen(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
177	
178	def xopen_eq(key, nonce, aad, data):
179	  Equal.trans(Maybe<&2, List<&2, U32>>, I.open(I.xkey(key, nonce), I.xnonce(nonce), aad, data), R.open(I.xkey(key, nonce), I.xnonce(nonce), aad, data), R.xopen(key, nonce, aad, data),
180	    open_eq(I.xkey(key, nonce), I.xnonce(nonce), aad, data),
181	    Equal.trans(Maybe<&2, List<&2, U32>>, R.open(I.xkey(key, nonce), I.xnonce(nonce), aad, data), R.open(RC.xsubkey(key, nonce), I.xnonce(nonce), aad, data), R.xopen(key, nonce, aad, data),
182	      Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => R.open(l, I.xnonce(nonce), aad, data), I.xkey(key, nonce), RC.xsubkey(key, nonce), xkey_eq(key, nonce)),
183	      Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => R.open(RC.xsubkey(key, nonce), l, aad, data), I.xnonce(nonce), RC.xnonce(nonce), xnonce_eq(nonce))))
184	
185	# ---------------------------------------------------------------- framing
186	
187	law length_append:
188	  for +xs: List<&2, U32>
189	  for +ys: List<&2, U32>
190	  {List.length(&2, U32, List.append(&2, U32, xs, ys)) == Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}
191	
192	def length_append(xs, ys):
193	  V.length_append(xs, ys)
194	
195	law prefix_append:
196	  for +xs: List<&2, U32>
197	  for +ys: List<&2, U32>
198	  {RC.prefix(List.length(&2, U32, xs), List.append(&2, U32, xs, ys)) == xs : List<&2, U32>}
199	
200	def prefix_append(xs, ys):
201	  match xs:
202	    case Nil{}: {==}
203	    case x <> xt:
204	      Equal.cong(List<&2, U32>, List<&2, U32>, l => x <> l, RC.prefix(List.length(&2, U32, xt), List.append(&2, U32, xt, ys)), xt, prefix_append(xt, ys))
205	
206	law suffix_append:
207	  for +xs: List<&2, U32>
208	  for +ys: List<&2, U32>
209	  {RC.suffix(List.length(&2, U32, xs), List.append(&2, U32, xs, ys)) == ys : List<&2, U32>}
210	
211	def suffix_append(xs, ys):
212	  match xs:
213	    case Nil{}: {==}
214	    case x <> xt: suffix_append(xt, ys)
215	
216	# a + 16 is not below 16, and (a + 16) - 16 == a.
217	law add16_not_lt:
218	  for +a: Nat
219	  {Nat.is_lt(Nat.add(a, 16n), 16n) == False{} : Bool}
220	
221	def add16_not_lt(a):
222	  %N.add_comm(16n, a) : {Nat.is_lt(_, 16n) == False{} : Bool}
223	  N.not_lt_zero(a)
224	
225	law add16_sub:
226	  for +a: Nat
227	  {Nat.sub(Nat.add(a, 16n), 16n) == a : Nat}
228	
229	def add16_sub(a):
230	  %N.add_comm(16n, a) : {Nat.sub(_, 16n) == a : Nat}
231	  N.sub_zero(a)
232	
233	# Opening ct || t with a 16-byte t checks t against the tag of ct.
234	law open_append:
235	  for +key: List<&2, U32>
236	  for +nonce: List<&2, U32>
237	  for +aad: List<&2, U32>
238	  for +ct: List<&2, U32>
239	  for +t: List<&2, U32>
240	  for +ht: {List.length(&2, U32, t) == 16n : Nat}
241	  {R.open(key, nonce, aad, List.append(&2, U32, ct, t)) == R.open_split(key, nonce, aad, ct, t) : Maybe<&2, List<&2, U32>>}
242	
243	def olen(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +d: List<&2, U32>, short: Bool) -> Maybe<&2, List<&2, U32>>:
244	  R.open_len(short, key, nonce, aad, d)
245	
246	def osplit_at(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +d: List<&2, U32>, +n: Nat) -> Maybe<&2, List<&2, U32>>:
247	  R.open_split(key, nonce, aad, RC.prefix(n, d), RC.suffix(n, d))
248	
249	def open_append(key, nonce, aad, ct, t, ht):
250	  +D = List.append(&2, U32, ct, t)
251	  +lc = List.length(&2, U32, ct)
252	  +elen = Equal.trans(Nat, List.length(&2, U32, D), Nat.add(lc, List.length(&2, U32, t)), Nat.add(lc, 16n),
253	    length_append(ct, t),
254	    Equal.cong(Nat, Nat, m => Nat.add(lc, m), List.length(&2, U32, t), 16n, ht))
255	  +eshort = Equal.trans(Bool, Nat.is_lt(List.length(&2, U32, D), 16n), Nat.is_lt(Nat.add(lc, 16n), 16n), False{},
256	    Equal.cong(Nat, Bool, m => Nat.is_lt(m, 16n), List.length(&2, U32, D), Nat.add(lc, 16n), elen),
257	    add16_not_lt(lc))
258	  +esub = Equal.trans(Nat, Nat.sub(List.length(&2, U32, D), 16n), Nat.sub(Nat.add(lc, 16n), 16n), lc,
259	    Equal.cong(Nat, Nat, m => Nat.sub(m, 16n), List.length(&2, U32, D), Nat.add(lc, 16n), elen),
260	    add16_sub(lc))
261	  Equal.trans(Maybe<&2, List<&2, U32>>, olen(key, nonce, aad, D, Nat.is_lt(List.length(&2, U32, D), 16n)), olen(key, nonce, aad, D, False{}), R.open_split(key, nonce, aad, ct, t),
262	    Equal.cong(Bool, Maybe<&2, List<&2, U32>>, b => olen(key, nonce, aad, D, b), Nat.is_lt(List.length(&2, U32, D), 16n), False{}, eshort),
263	    Equal.trans(Maybe<&2, List<&2, U32>>, osplit_at(key, nonce, aad, D, Nat.sub(List.length(&2, U32, D), 16n)), osplit_at(key, nonce, aad, D, lc), R.open_split(key, nonce, aad, ct, t),
264	      Equal.cong(Nat, Maybe<&2, List<&2, U32>>, m => osplit_at(key, nonce, aad, D, m), Nat.sub(List.length(&2, U32, D), 16n), lc, esub),
265	      Equal.trans(Maybe<&2, List<&2, U32>>, R.open_split(key, nonce, aad, RC.prefix(lc, D), RC.suffix(lc, D)), R.open_split(key, nonce, aad, ct, RC.suffix(lc, D)), R.open_split(key, nonce, aad, ct, t),
266	        Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => R.open_split(key, nonce, aad, l, RC.suffix(lc, D)), RC.prefix(lc, D), ct, prefix_append(ct, t)),
267	        Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => R.open_split(key, nonce, aad, ct, l), RC.suffix(lc, D), t, suffix_append(ct, t)))))
268	
269	# ---------------------------------------------------------------- properties of the specification
270	
271	# Opening what was sealed gives the plaintext back (for every key, nonce,
272	# aad and plaintext list).
273	law roundtrip:
274	  for +key: List<&2, U32>
275	  for +nonce: List<&2, U32>
276	  for +aad: List<&2, U32>
277	  for +pt: List<&2, U32>
278	  {R.open(key, nonce, aad, R.seal(key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
279	
280	def roundtrip(key, nonce, aad, pt):
281	  +ct = RC.encrypt(key, 1, nonce, pt)
282	  +t = R.tag(key, nonce, aad, ct)
283	  Equal.trans(Maybe<&2, List<&2, U32>>, R.open(key, nonce, aad, List.append(&2, U32, ct, t)), R.open_split(key, nonce, aad, ct, t), Some{pt},
284	    open_append(key, nonce, aad, ct, t, PM.mac_length(R.poly_key(key, nonce), R.mac_data(aad, ct))),
285	    Equal.trans(Maybe<&2, List<&2, U32>>, R.open_tag(RS.equal(t, t), key, nonce, ct), R.open_tag(True{}, key, nonce, ct), Some{pt},
286	      Equal.cong(Bool, Maybe<&2, List<&2, U32>>, b => R.open_tag(b, key, nonce, ct), RS.equal(t, t), True{}, SE.equal_refl(t)),
287	      Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, RC.encrypt(key, 1, nonce, ct), pt, V.involution(10n, key, 1, nonce, pt))))
288	
289	law open_tag_false:
290	  for +key: List<&2, U32>
291	  for +nonce: List<&2, U32>
292	  for +aad: List<&2, U32>
293	  for +ct: List<&2, U32>
294	  for +t: List<&2, U32>
295	  for ne: {t != R.tag(key, nonce, aad, ct) : List<&2, U32>}
296	  for +b: Bool
297	  for +hb: {RS.equal(t, R.tag(key, nonce, aad, ct)) == b : Bool}
298	  {R.open_tag(b, key, nonce, ct) == None{} : Maybe<&2, List<&2, U32>>}
299	
300	def open_tag_false(key, nonce, aad, ct, t, ne, b, hb):
301	  match b:
302	    case True{}: Empty.absurd({R.open_tag(True{}, key, nonce, ct) == None{} : Maybe<&2, List<&2, U32>>}, ne(SE.equal_sound(t, R.tag(key, nonce, aad, ct), hb)))
303	    case False{}: {==}
304	
305	# Opening ciphertext || t fails for every 16-byte t that is not the tag of
306	# the ciphertext (under the key, nonce and aad given).
307	law forgery:
308	  for +key: List<&2, U32>
309	  for +nonce: List<&2, U32>
310	  for +aad: List<&2, U32>
311	  for +ct: List<&2, U32>
312	  for +t: List<&2, U32>
313	  for +ht: {List.length(&2, U32, t) == 16n : Nat}
314	  for ne: {t != R.tag(key, nonce, aad, ct) : List<&2, U32>}
315	  {R.open(key, nonce, aad, List.append(&2, U32, ct, t)) == None{} : Maybe<&2, List<&2, U32>>}
316	
317	def forgery(key, nonce, aad, ct, t, ht, ne):
318	  Equal.trans(Maybe<&2, List<&2, U32>>, R.open(key, nonce, aad, List.append(&2, U32, ct, t)), R.open_split(key, nonce, aad, ct, t), None{},
319	    open_append(key, nonce, aad, ct, t, ht),
320	    open_tag_false(key, nonce, aad, ct, t, ne, RS.equal(t, R.tag(key, nonce, aad, ct)), {==}))
321	
322	# The implementation's tag is the specification's, so a t other than the
323	# implementation's tag is rejected by the implementation.
324	law iforgery:
325	  for +key: List<&2, U32>
326	  for +nonce: List<&2, U32>
327	  for +aad: List<&2, U32>
328	  for +ct: List<&2, U32>
329	  for +t: List<&2, U32>
330	  for +ht: {List.length(&2, U32, t) == 16n : Nat}
331	  for ne: {t != I.tag(key, nonce, aad, ct) : List<&2, U32>}
332	  {I.open(key, nonce, aad, List.append(&2, U32, ct, t)) == None{} : Maybe<&2, List<&2, U32>>}
333	
334	def iforgery(key, nonce, aad, ct, t, ht, ne):
335	  Equal.trans(Maybe<&2, List<&2, U32>>, I.open(key, nonce, aad, List.append(&2, U32, ct, t)), R.open(key, nonce, aad, List.append(&2, U32, ct, t)), None{},
336	    open_eq(key, nonce, aad, List.append(&2, U32, ct, t)),
337	    forgery(key, nonce, aad, ct, t, ht, e => ne(Equal.trans(List<&2, U32>, t, R.tag(key, nonce, aad, ct), I.tag(key, nonce, aad, ct), e, Equal.sym(List<&2, U32>, I.tag(key, nonce, aad, ct), R.tag(key, nonce, aad, ct), tag_eq(key, nonce, aad, ct))))))
338	
339	law iroundtrip:
340	  for +key: List<&2, U32>
341	  for +nonce: List<&2, U32>
342	  for +aad: List<&2, U32>
343	  for +pt: List<&2, U32>
344	  {I.open(key, nonce, aad, I.seal(key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
345	
346	def iroundtrip(key, nonce, aad, pt):
347	  Equal.trans(Maybe<&2, List<&2, U32>>, I.open(key, nonce, aad, I.seal(key, nonce, aad, pt)), R.open(key, nonce, aad, I.seal(key, nonce, aad, pt)), Some{pt},
348	    open_eq(key, nonce, aad, I.seal(key, nonce, aad, pt)),
349	    Equal.trans(Maybe<&2, List<&2, U32>>, R.open(key, nonce, aad, I.seal(key, nonce, aad, pt)), R.open(key, nonce, aad, R.seal(key, nonce, aad, pt)), Some{pt},
350	      Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => R.open(key, nonce, aad, l), I.seal(key, nonce, aad, pt), R.seal(key, nonce, aad, pt), seal_eq(key, nonce, aad, pt)),
351	      roundtrip(key, nonce, aad, pt)))