proofs/crypto/aead/sound.bend

bend-collections-laws-crypto@1.0.0.0 · 200 lines · 12 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as RC
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha20poly1305.bend as R
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend as RS
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/involution.bend as V
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend as AD
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/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
21law none_some:
22  for +p: List<&2, U32>
23  for +h: {None{} == Some{p} : Maybe<&2, List<&2, U32>>}
24  Empty
25
26def 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
29law 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
35def 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
40law 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
45def 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
52law 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
57def 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
66def 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
69law 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
81def 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
96law 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
106def 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.
118law 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
127def 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
132def 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
135law 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
149def 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
165law 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
177def 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
188law 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
199def 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)