1	import Base
2	import ../../../spec/crypto/chacha.bend as RC
3	import ../../../spec/crypto/chacha20poly1305.bend as R
4	import ../../../spec/crypto/subtle.bend as RS
5	import ../../../spec/crypto/aes/gcm.bend as G
6	import ../../lib/logic.bend as L
7	import ../chacha/involution.bend as V
8	import ../aes/aead.bend as AD
9	import ./subtle_eq.bend as SE
10	
11	# Decryption is sound: whatever the specification opens to a plaintext p is
12	# exactly the sealing of p (same key, nonce and aad). So no input other than
13	# the honest ciphertext of p ever decrypts to p: an accepted ciphertext
14	# carries the tag of its body, and the body is the encryption of p (the
15	# stream is an involution). Stated for the ChaCha20-Poly1305 specification
16	# (spec/crypto/chacha20poly1305.bend) and the GCM specification
17	# (spec/crypto/aes/gcm.bend); the facade clause decrypt_sound follows.
18	
19	# ---------------------------------------------------------------- Maybe
20	
21	law none_some:
22	  for +p: List<&2, U32>
23	  for +h: {None{} == Some{p} : Maybe<&2, List<&2, U32>>}
24	  Empty
25	
26	def none_some(p, h):
27	  L.false_true(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, m => Maybe.is_some(&2, List<&2, U32>, m), None{}, Some{p}, h))
28	
29	law some_inj:
30	  for +x: List<&2, U32>
31	  for +p: List<&2, U32>
32	  for +h: {Some{x} == Some{p} : Maybe<&2, List<&2, U32>>}
33	  {x == p : List<&2, U32>}
34	
35	def some_inj(x, p, h):
36	  Equal.cong(Maybe<&2, List<&2, U32>>, List<&2, U32>, m => Maybe.default(&2, List<&2, U32>, m, Nil{}), Some{x}, Some{p}, h)
37	
38	# ---------------------------------------------------------------- splits
39	
40	law prefix_suffix:
41	  for +n: Nat
42	  for +xs: List<&2, U32>
43	  {List.append(&2, U32, RC.prefix(n, xs), RC.suffix(n, xs)) == xs : List<&2, U32>}
44	
45	def prefix_suffix(n, xs):
46	  match n xs:
47	    case 0n _: {==}
48	    case 1n+k Nil{}: {==}
49	    case 1n+k x <> rest:
50	      Equal.cong(List<&2, U32>, List<&2, U32>, l => x <> l, List.append(&2, U32, RC.prefix(k, rest), RC.suffix(k, rest)), rest, prefix_suffix(k, rest))
51	
52	law take_drop:
53	  for +xs: List<&2, U32>
54	  for +n: Nat
55	  {List.append(&2, U32, List.take(&2, U32, xs, n), List.drop(&2, U32, xs, n)) == xs : List<&2, U32>}
56	
57	def take_drop(xs, n):
58	  match xs n:
59	    case Nil{} _: {==}
60	    case x <> rest 0n: {==}
61	    case x <> rest 1n+k:
62	      Equal.cong(List<&2, U32>, List<&2, U32>, l => x <> l, List.append(&2, U32, List.take(&2, U32, rest, k), List.drop(&2, U32, rest, k)), rest, take_drop(rest, k))
63	
64	# ---------------------------------------------------------------- ChaCha20-Poly1305
65	
66	def csa(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +c: List<&2, U32>) -> List<&2, U32>:
67	  List.append(&2, U32, c, R.tag(key, nonce, aad, c))
68	
69	law c_tag:
70	  for +ok: Bool
71	  for +key: List<&2, U32>
72	  for +nonce: List<&2, U32>
73	  for +aad: List<&2, U32>
74	  for +ct: List<&2, U32>
75	  for +t: List<&2, U32>
76	  for +p: List<&2, U32>
77	  for +hok: {RS.equal(t, R.tag(key, nonce, aad, ct)) == ok : Bool}
78	  for +h: {R.open_tag(ok, key, nonce, ct) == Some{p} : Maybe<&2, List<&2, U32>>}
79	  {R.seal(key, nonce, aad, p) == List.append(&2, U32, ct, t) : List<&2, U32>}
80	
81	def c_tag(ok, key, nonce, aad, ct, t, p, hok, h):
82	  match ok:
83	    case False{}: Empty.absurd({R.seal(key, nonce, aad, p) == List.append(&2, U32, ct, t) : List<&2, U32>}, none_some(p, h))
84	    case True{}:
85	      +e = RC.encrypt(key, 1, nonce, ct)
86	      +ep = some_inj(e, p, h)
87	      +et = SE.equal_sound(t, R.tag(key, nonce, aad, ct), hok)
88	      Equal.trans(List<&2, U32>, R.seal(key, nonce, aad, p), csa(key, nonce, aad, RC.encrypt(key, 1, nonce, e)), List.append(&2, U32, ct, t),
89	        Equal.trans(List<&2, U32>, R.seal(key, nonce, aad, p), R.seal(key, nonce, aad, e), csa(key, nonce, aad, RC.encrypt(key, 1, nonce, e)),
90	          Equal.cong(List<&2, U32>, List<&2, U32>, q => R.seal(key, nonce, aad, q), p, e, Equal.sym(List<&2, U32>, e, p, ep)),
91	          {==}),
92	        Equal.trans(List<&2, U32>, csa(key, nonce, aad, RC.encrypt(key, 1, nonce, e)), csa(key, nonce, aad, ct), List.append(&2, U32, ct, t),
93	          Equal.cong(List<&2, U32>, List<&2, U32>, q => csa(key, nonce, aad, q), RC.encrypt(key, 1, nonce, e), ct, V.involution(10n, key, 1, nonce, ct)),
94	          Equal.cong(List<&2, U32>, List<&2, U32>, q => List.append(&2, U32, ct, q), R.tag(key, nonce, aad, ct), t, Equal.sym(List<&2, U32>, t, R.tag(key, nonce, aad, ct), et))))
95	
96	law c_len:
97	  for +short: Bool
98	  for +key: List<&2, U32>
99	  for +nonce: List<&2, U32>
100	  for +aad: List<&2, U32>
101	  for +data: List<&2, U32>
102	  for +p: List<&2, U32>
103	  for +h: {R.open_len(short, key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>}
104	  {R.seal(key, nonce, aad, p) == data : List<&2, U32>}
105	
106	def c_len(short, key, nonce, aad, data, p, h):
107	  match short:
108	    case True{}: Empty.absurd({R.seal(key, nonce, aad, p) == data : List<&2, U32>}, none_some(p, h))
109	    case False{}:
110	      +n = Nat.sub(List.length(&2, U32, data), 16n)
111	      +ct = RC.prefix(n, data)
112	      +t = RC.suffix(n, data)
113	      Equal.trans(List<&2, U32>, R.seal(key, nonce, aad, p), List.append(&2, U32, ct, t), data,
114	        c_tag(RS.equal(t, R.tag(key, nonce, aad, ct)), key, nonce, aad, ct, t, p, {==}, h),
115	        prefix_suffix(n, data))
116	
117	# Whatever opens to p is the sealing of p.
118	law chacha_sound:
119	  for +key: List<&2, U32>
120	  for +nonce: List<&2, U32>
121	  for +aad: List<&2, U32>
122	  for +data: List<&2, U32>
123	  for +p: List<&2, U32>
124	  for +h: {R.open(key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>}
125	  {R.seal(key, nonce, aad, p) == data : List<&2, U32>}
126	
127	def chacha_sound(key, nonce, aad, data, p, h):
128	  c_len(Nat.is_lt(List.length(&2, U32, data), 16n), key, nonce, aad, data, p, h)
129	
130	# ---------------------------------------------------------------- GCM
131	
132	def gsa(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, +c: List<&2, U32>) -> List<&2, U32>:
133	  List.append(&2, U32, c, G.tag(nk, nr, key, iv, aad, c))
134	
135	law g_tag:
136	  for +ok: Bool
137	  for +nk: Nat
138	  for +nr: Nat
139	  for +key: List<&2, U32>
140	  for +iv: List<&2, U32>
141	  for +aad: List<&2, U32>
142	  for +c: List<&2, U32>
143	  for +t: List<&2, U32>
144	  for +p: List<&2, U32>
145	  for +hok: {RS.equal(t, G.tag(nk, nr, key, iv, aad, c)) == ok : Bool}
146	  for +h: {G.accept(ok, G.gctr(nk, nr, key, c, G.inc32(G.j0(iv)))) == Some{p} : Maybe<&2, List<&2, U32>>}
147	  {G.seal(nk, nr, key, iv, aad, p) == List.append(&2, U32, c, t) : List<&2, U32>}
148	
149	def g_tag(ok, nk, nr, key, iv, aad, c, t, p, hok, h):
150	  match ok:
151	    case False{}: Empty.absurd({G.seal(nk, nr, key, iv, aad, p) == List.append(&2, U32, c, t) : List<&2, U32>}, none_some(p, h))
152	    case True{}:
153	      +cb = G.inc32(G.j0(iv))
154	      +e = G.gctr(nk, nr, key, c, cb)
155	      +ep = some_inj(e, p, h)
156	      +et = SE.equal_sound(t, G.tag(nk, nr, key, iv, aad, c), hok)
157	      Equal.trans(List<&2, U32>, G.seal(nk, nr, key, iv, aad, p), gsa(nk, nr, key, iv, aad, G.gctr(nk, nr, key, e, cb)), List.append(&2, U32, c, t),
158	        Equal.trans(List<&2, U32>, G.seal(nk, nr, key, iv, aad, p), G.seal(nk, nr, key, iv, aad, e), gsa(nk, nr, key, iv, aad, G.gctr(nk, nr, key, e, cb)),
159	          Equal.cong(List<&2, U32>, List<&2, U32>, q => G.seal(nk, nr, key, iv, aad, q), p, e, Equal.sym(List<&2, U32>, e, p, ep)),
160	          {==}),
161	        Equal.trans(List<&2, U32>, gsa(nk, nr, key, iv, aad, G.gctr(nk, nr, key, e, cb)), gsa(nk, nr, key, iv, aad, c), List.append(&2, U32, c, t),
162	          Equal.cong(List<&2, U32>, List<&2, U32>, q => gsa(nk, nr, key, iv, aad, q), G.gctr(nk, nr, key, e, cb), c, AD.gctr_inv(nk, nr, key, c, cb)),
163	          Equal.cong(List<&2, U32>, List<&2, U32>, q => List.append(&2, U32, c, q), G.tag(nk, nr, key, iv, aad, c), t, Equal.sym(List<&2, U32>, t, G.tag(nk, nr, key, iv, aad, c), et))))
164	
165	law g_len:
166	  for +short: Bool
167	  for +nk: Nat
168	  for +nr: Nat
169	  for +key: List<&2, U32>
170	  for +iv: List<&2, U32>
171	  for +aad: List<&2, U32>
172	  for +input: List<&2, U32>
173	  for +p: List<&2, U32>
174	  for +h: {G.open_split(nk, nr, key, iv, aad, input, List.length(&2, U32, input), short) == Some{p} : Maybe<&2, List<&2, U32>>}
175	  {G.seal(nk, nr, key, iv, aad, p) == input : List<&2, U32>}
176	
177	def g_len(short, nk, nr, key, iv, aad, input, p, h):
178	  match short:
179	    case True{}: Empty.absurd({G.seal(nk, nr, key, iv, aad, p) == input : List<&2, U32>}, none_some(p, h))
180	    case False{}:
181	      +n = Nat.sub(List.length(&2, U32, input), 16n)
182	      +c = List.take(&2, U32, input, n)
183	      +t = List.drop(&2, U32, input, n)
184	      Equal.trans(List<&2, U32>, G.seal(nk, nr, key, iv, aad, p), List.append(&2, U32, c, t), input,
185	        g_tag(RS.equal(t, G.tag(nk, nr, key, iv, aad, c)), nk, nr, key, iv, aad, c, t, p, {==}, h),
186	        take_drop(input, n))
187	
188	law gcm_sound:
189	  for +nk: Nat
190	  for +nr: Nat
191	  for +key: List<&2, U32>
192	  for +iv: List<&2, U32>
193	  for +aad: List<&2, U32>
194	  for +input: List<&2, U32>
195	  for +p: List<&2, U32>
196	  for +h: {G.open(nk, nr, key, iv, aad, input) == Some{p} : Maybe<&2, List<&2, U32>>}
197	  {G.seal(nk, nr, key, iv, aad, p) == input : List<&2, U32>}
198	
199	def gcm_sound(nk, nr, key, iv, aad, input, p, h):
200	  g_len(Nat.is_lt(List.length(&2, U32, input), 16n), nk, nr, key, iv, aad, input, p, h)