proofs/crypto/aead/chacha20poly1305.bend

bend-collections-laws-crypto@1.0.0.0 · 351 lines · 27 definitions

1import 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)
4import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac.bend as PM
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as CH
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/aead/chacha20poly1305.bend as I
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/subtle.bend as S
8import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as RC
9import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as RP
10import bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend as RS
11import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha20poly1305.bend as R
12import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
13import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/stream.bend as T
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/xchacha.bend as X
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/involution.bend as V
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/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
31law 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
36def 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
41law 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
46def mac_data_eq(aad, ct):
47  {==}
48
49law 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
56def 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
63def 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
66law 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
73def 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
80law 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
87def 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
93law 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
101def 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
108law 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
116def 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
119def 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
130law 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
137def open_eq(key, nonce, aad, data):
138  open_len_eq(Nat.is_lt(List.length(&2, U32, data), 16n), key, nonce, aad, data)
139
140law 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
145def 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
150law xnonce_eq:
151  for +nonce: List<&2, U32>
152  {I.xnonce(nonce) == RC.xnonce(nonce) : List<&2, U32>}
153
154def 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
157law 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
164def 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
171law 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
178def 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
187law 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
192def length_append(xs, ys):
193  V.length_append(xs, ys)
194
195law 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
200def 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
206law 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
211def 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.
217law add16_not_lt:
218  for +a: Nat
219  {Nat.is_lt(Nat.add(a, 16n), 16n) == False{} : Bool}
220
221def add16_not_lt(a):
222  %N.add_comm(16n, a) : {Nat.is_lt(_, 16n) == False{} : Bool}
223  N.not_lt_zero(a)
224
225law add16_sub:
226  for +a: Nat
227  {Nat.sub(Nat.add(a, 16n), 16n) == a : Nat}
228
229def 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.
234law 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
243def 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
246def 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
249def 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).
273law 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
280def 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
289law 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
300def 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).
307law 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
317def 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.
324law 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
334def 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
339law 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
346def 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)))