proof/AES_NistObservationProof.bend
qasim-bend-kit@0.1.0.2 · 258 lines · 22 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/LAWS.bend as L
3import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
4import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
5
6def ciphertext(output: Core.GcmCiphertext) -> List<&2, U32>:
7 match output:
8 case Core.GcmCiphertext{bytes, valid}: bytes
9
10def schedule_input_matches(+key: AES.SecretKey, +bytes: List<&2, U32>, +words: List<&2, U32>,
11 input_matches: {AES.secret_key_bytes(key) == bytes : List<&2, U32>},
12 computed: {Core.aes256_expand(bytes) == words : List<&2, U32>}) ->
13 {Core.aes256_expand(AES.secret_key_bytes(key)) == words : List<&2, U32>}:
14 Equal.trans(List<&2, U32>, Core.aes256_expand(AES.secret_key_bytes(key)), Core.aes256_expand(bytes), words,
15 Equal.cong(List<&2, U32>, List<&2, U32>, value => Core.aes256_expand(value),
16 AES.secret_key_bytes(key), bytes, input_matches), computed)
17
18def stream_parameters(+size: Nat, +words: List<&2, U32>, +start: List<&2, U32>,
19 +known_size: Nat, +known_start: List<&2, U32>, +stream: List<&2, U32>,
20 count: {size == known_size : Nat}, counter: {start == known_start : List<&2, U32>},
21 computed: {Core.gcm_ctr_stream_exact.go(known_size, words, known_start, Nil{}) == stream : List<&2, U32>}) ->
22 {Core.gcm_ctr_stream_exact(size, words, start) == stream : List<&2, U32>}:
23 Equal.trans(List<&2, U32>, Core.gcm_ctr_stream_exact(size, words, start),
24 Core.gcm_ctr_stream_exact.go(known_size, words, start, Nil{}), stream,
25 Equal.cong(Nat, List<&2, U32>, n => Core.gcm_ctr_stream_exact.go(n, words, start, Nil{}), size, known_size, count),
26 Equal.trans(List<&2, U32>, Core.gcm_ctr_stream_exact.go(known_size, words, start, Nil{}),
27 Core.gcm_ctr_stream_exact.go(known_size, words, known_start, Nil{}), stream,
28 Equal.cong(List<&2, U32>, List<&2, U32>, value => Core.gcm_ctr_stream_exact.go(known_size, words, value, Nil{}),
29 start, known_start, counter), computed))
30
31def ciphertext_shape(+words: List<&2, U32>, +nonce: List<&2, U32>, +input: List<&2, U32>) ->
32 {ciphertext(Core.gcm_ctr_encrypt(words, nonce, input)) == Core.gcm_decrypt_expanded(words, nonce, input) : List<&2, U32>}:
33 {==}
34
35def xor_from_stream(+words: List<&2, U32>, +nonce: List<&2, U32>, +input: List<&2, U32>, +stream: List<&2, U32>,
36 computed: {Core.gcm_ctr_stream_exact(List.length(&2, U32, input), words, Core.gcm_inc32(Core.gcm_j0(nonce))) == stream : List<&2, U32>}) ->
37 {Core.gcm_decrypt_expanded(words, nonce, input) == Core.gcm_zip_xor(input, stream) : List<&2, U32>}:
38 Equal.cong(List<&2, U32>, List<&2, U32>, value => Core.gcm_zip_xor(input, value),
39 Core.gcm_ctr_stream_exact(List.length(&2, U32, input), words, Core.gcm_inc32(Core.gcm_j0(nonce))), stream, computed)
40
41def finish_cipher(+words: List<&2, U32>, +nonce: List<&2, U32>, +input: List<&2, U32>, +stream: List<&2, U32>, +output: List<&2, U32>,
42 computed: {Core.gcm_ctr_stream_exact(List.length(&2, U32, input), words, Core.gcm_inc32(Core.gcm_j0(nonce))) == stream : List<&2, U32>},
43 xor_matches: {Core.gcm_zip_xor(input, stream) == output : List<&2, U32>}) ->
44 {ciphertext(Core.gcm_ctr_encrypt(words, nonce, input)) == output : List<&2, U32>}:
45 Equal.trans(List<&2, U32>, ciphertext(Core.gcm_ctr_encrypt(words, nonce, input)),
46 Core.gcm_decrypt_expanded(words, nonce, input), output, ciphertext_shape(words, nonce, input),
47 Equal.trans(List<&2, U32>, Core.gcm_decrypt_expanded(words, nonce, input),
48 Core.gcm_zip_xor(input, stream), output, xor_from_stream(words, nonce, input, stream, computed), xor_matches))
49
50def parts(+words: List<&2, U32>, +nonce: AES.Nonce,
51 +aad: List<&2, U32>, +bytes: List<&2, U32>) -> List<&2, U32>:
52 List.append(&2, U32, AES.raw_nonce_bytes(nonce),
53 List.append(&2, U32, bytes,
54 Core.gcm_tag_bytes(Core.gcm_tag_output(words,
55 AES.raw_nonce_bytes(nonce), aad, bytes))))
56
57def expanded(+words: List<&2, U32>, +nonce: AES.Nonce,
58 +aad: List<&2, U32>, +plaintext: List<&2, U32>) -> List<&2, U32>:
59 parts(words, nonce, aad,
60 ciphertext(Core.gcm_ctr_encrypt(words, AES.raw_nonce_bytes(nonce), plaintext)))
61
62def from_ciphertext(+words: List<&2, U32>, +nonce: AES.Nonce,
63 +aad: List<&2, U32>, +output: Core.GcmCiphertext) ->
64 {L.aes256gcm_nist_encrypt_observation(AES.encrypt_output_from_gcm(nonce,
65 Core.gcm_output_from_ciphertext(words, AES.raw_nonce_bytes(nonce), aad, output))) ==
66 parts(words, nonce, aad, ciphertext(output)) : List<&2, U32>}:
67 match nonce output:
68 case AES.Nonce{nonce_bytes, nonce_size, nonce_valid} Core.GcmCiphertext{bytes, valid}: {==}
69
70def valid_encrypt(+key: AES.SecretKey, +nonce: AES.Nonce,
71 +aad: List<&2, U32>, +plaintext: List<&2, U32>) ->
72 {L.aes256gcm_nist_encrypt_observation(AES.encrypt_valid(key, nonce, aad, plaintext)) ==
73 expanded(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad, plaintext) : List<&2, U32>}:
74 from_ciphertext(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad,
75 Core.gcm_ctr_encrypt(Core.aes256_expand(AES.secret_key_bytes(key)),
76 AES.raw_nonce_bytes(nonce), plaintext))
77
78def checked_encrypt(+key: AES.SecretKey, +nonce: AES.Nonce,
79 +aad: List<&2, U32>, +plaintext: List<&2, U32>,
80 aad_ok: {AES.aad_valid(aad) == True{} : Bool},
81 plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}) ->
82 {L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)) ==
83 expanded(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad, plaintext) : List<&2, U32>}:
84 Equal.trans(List<&2, U32>,
85 L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)),
86 L.aes256gcm_nist_encrypt_observation(AES.encrypt_valid(key, nonce, aad, plaintext)),
87 expanded(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad, plaintext),
88 Equal.trans(List<&2, U32>,
89 L.aes256gcm_nist_encrypt_observation(AES.encrypt_checked(key, nonce, aad, plaintext,
90 AES.aad_valid(aad), AES.plaintext_valid(plaintext))),
91 L.aes256gcm_nist_encrypt_observation(AES.encrypt_checked(key, nonce, aad, plaintext,
92 True{}, AES.plaintext_valid(plaintext))),
93 L.aes256gcm_nist_encrypt_observation(AES.encrypt_checked(key, nonce, aad, plaintext,
94 True{}, True{})),
95 Equal.cong(Bool, List<&2, U32>, flag =>
96 L.aes256gcm_nist_encrypt_observation(AES.encrypt_checked(key, nonce, aad, plaintext,
97 flag, AES.plaintext_valid(plaintext))),
98 AES.aad_valid(aad), True{}, aad_ok),
99 Equal.cong(Bool, List<&2, U32>, flag =>
100 L.aes256gcm_nist_encrypt_observation(AES.encrypt_checked(key, nonce, aad, plaintext,
101 True{}, flag)),
102 AES.plaintext_valid(plaintext), True{}, plaintext_ok)),
103 valid_encrypt(key, nonce, aad, plaintext))
104
105def finish_encrypt(+key: AES.SecretKey, +nonce: AES.Nonce,
106 +aad: List<&2, U32>, +plaintext: List<&2, U32>,
107 +words: List<&2, U32>, +bytes: List<&2, U32>, +tag: List<&2, U32>,
108 aad_ok: {AES.aad_valid(aad) == True{} : Bool},
109 plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool},
110 key_matches: {Core.aes256_expand(AES.secret_key_bytes(key)) == words : List<&2, U32>},
111 ciphertext_matches: {ciphertext(Core.gcm_ctr_encrypt(words, AES.raw_nonce_bytes(nonce), plaintext)) == bytes : List<&2, U32>},
112 tag_matches: {Core.gcm_tag_bytes(Core.gcm_tag_output(words, AES.raw_nonce_bytes(nonce), aad, bytes)) == tag : List<&2, U32>}) ->
113 {L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)) ==
114 List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)) : List<&2, U32>}:
115 Equal.trans(List<&2, U32>,
116 L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)),
117 expanded(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad, plaintext),
118 List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)),
119 checked_encrypt(key, nonce, aad, plaintext, aad_ok, plaintext_ok),
120 Equal.trans(List<&2, U32>,
121 expanded(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad, plaintext),
122 expanded(words, nonce, aad, plaintext),
123 List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)),
124 Equal.cong(List<&2, U32>, List<&2, U32>, expanded_words =>
125 expanded(expanded_words, nonce, aad, plaintext),
126 Core.aes256_expand(AES.secret_key_bytes(key)), words, key_matches),
127 Equal.trans(List<&2, U32>, expanded(words, nonce, aad, plaintext),
128 parts(words, nonce, aad, bytes),
129 List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)),
130 Equal.cong(List<&2, U32>, List<&2, U32>, encrypted => parts(words, nonce, aad, encrypted),
131 ciphertext(Core.gcm_ctr_encrypt(words, AES.raw_nonce_bytes(nonce), plaintext)), bytes,
132 ciphertext_matches),
133 Equal.cong(List<&2, U32>, List<&2, U32>, tag_bytes =>
134 List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag_bytes)),
135 Core.gcm_tag_bytes(Core.gcm_tag_output(words, AES.raw_nonce_bytes(nonce), aad, bytes)),
136 tag, tag_matches))))
137
138def decrypt_expanded(+words: List<&2, U32>, +aad: List<&2, U32>,
139 +envelope: AES.Envelope) -> Result<&2, &2, AES.Error, List<&2, U32>>:
140 match envelope:
141 case AES.Envelope{nonce, bytes, tag, valid}:
142 AES.decrypt_authenticated_tag(words, AES.raw_nonce_bytes(nonce), aad, bytes, envelope, tag)
143
144def decrypt_key_shape(+key: AES.SecretKey, +aad: List<&2, U32>, +envelope: AES.Envelope) ->
145 {AES.decrypt_authenticated(key, aad, envelope) ==
146 decrypt_expanded(Core.aes256_expand(AES.secret_key_bytes(key)), aad, envelope) : Result<&2, &2, AES.Error, List<&2, U32>>}:
147 match key envelope:
148 case AES.SecretKey{key_bytes, key_size, key_valid} AES.Envelope{nonce, bytes, tag, valid}: {==}
149
150def payload_shape(+words: List<&2, U32>, +envelope: AES.Envelope) ->
151 {AES.decrypt_auth_result(words, envelope, True{}) ==
152 Done{Core.gcm_decrypt_expanded(words, AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), AES.ciphertext(envelope))} : Result<&2, &2, AES.Error, List<&2, U32>>}:
153 match envelope:
154 case AES.Envelope{nonce, bytes, tag, valid}: {==}
155
156def payload_parameters(+words: List<&2, U32>, +envelope: AES.Envelope,
157 +nonce: List<&2, U32>, +bytes: List<&2, U32>, +plaintext: List<&2, U32>,
158 nonce_matches: {AES.raw_nonce_bytes(AES.envelope_nonce(envelope)) == nonce : List<&2, U32>},
159 ciphertext_matches: {AES.ciphertext(envelope) == bytes : List<&2, U32>},
160 computed: {Core.gcm_decrypt_expanded(words, nonce, bytes) == plaintext : List<&2, U32>}) ->
161 {AES.decrypt_auth_result(words, envelope, True{}) == Done{plaintext} : Result<&2, &2, AES.Error, List<&2, U32>>}:
162 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>, AES.decrypt_auth_result(words, envelope, True{}),
163 Done{Core.gcm_decrypt_expanded(words, AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), AES.ciphertext(envelope))},
164 Done{plaintext}, payload_shape(words, envelope),
165 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
166 Done{Core.gcm_decrypt_expanded(words, AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), AES.ciphertext(envelope))},
167 Done{Core.gcm_decrypt_expanded(words, nonce, AES.ciphertext(envelope))}, Done{plaintext},
168 Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>, value => Done{Core.gcm_decrypt_expanded(words, value, AES.ciphertext(envelope))},
169 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), nonce, nonce_matches),
170 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>, Done{Core.gcm_decrypt_expanded(words, nonce, AES.ciphertext(envelope))},
171 Done{Core.gcm_decrypt_expanded(words, nonce, bytes)}, Done{plaintext},
172 Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>, value => Done{Core.gcm_decrypt_expanded(words, nonce, value)},
173 AES.ciphertext(envelope), bytes, ciphertext_matches),
174 Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>, value => Done{value},
175 Core.gcm_decrypt_expanded(words, nonce, bytes), plaintext, computed))))
176
177def envelope_tag_computed(+words: List<&2, U32>, +aad: List<&2, U32>, +envelope: AES.Envelope) -> List<&2, U32>:
178 Core.gcm_tag_bytes(Core.gcm_tag_output(words, AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), aad, AES.ciphertext(envelope)))
179
180def tag_parameters(+words: List<&2, U32>, +aad: List<&2, U32>, +envelope: AES.Envelope,
181 +nonce: List<&2, U32>, +bytes: List<&2, U32>, +tag: List<&2, U32>,
182 nonce_matches: {AES.raw_nonce_bytes(AES.envelope_nonce(envelope)) == nonce : List<&2, U32>},
183 ciphertext_matches: {AES.ciphertext(envelope) == bytes : List<&2, U32>},
184 computed: {Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, bytes)) == tag : List<&2, U32>}) ->
185 {envelope_tag_computed(words, aad, envelope) == tag : List<&2, U32>}:
186 Equal.trans(List<&2, U32>, envelope_tag_computed(words, aad, envelope),
187 Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, AES.ciphertext(envelope))), tag,
188 Equal.cong(List<&2, U32>, List<&2, U32>, value =>
189 Core.gcm_tag_bytes(Core.gcm_tag_output(words, value, aad, AES.ciphertext(envelope))),
190 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), nonce, nonce_matches),
191 Equal.trans(List<&2, U32>, Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, AES.ciphertext(envelope))),
192 Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, bytes)), tag,
193 Equal.cong(List<&2, U32>, List<&2, U32>, value =>
194 Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, value)),
195 AES.ciphertext(envelope), bytes, ciphertext_matches), computed))
196
197def auth_for_tag(+envelope: AES.Envelope, tag: List<&2, U32>) -> Bool:
198 AES.bytes_equal_full_scan(AES.tag_bytes(AES.envelope_tag(envelope)), tag)
199
200def decrypt_auth_shape(+words: List<&2, U32>, +aad: List<&2, U32>, +envelope: AES.Envelope) ->
201 {decrypt_expanded(words, aad, envelope) == AES.decrypt_auth_result(words, envelope,
202 auth_for_tag(envelope, envelope_tag_computed(words, aad, envelope))) : Result<&2, &2, AES.Error, List<&2, U32>>}:
203 match envelope:
204 case AES.Envelope{nonce, bytes, tag, valid}:
205 match tag:
206 case AES.Tag{tag_bytes, tag_size, tag_valid}: {==}
207
208def finish_auth(+words: List<&2, U32>, +aad: List<&2, U32>, +envelope: AES.Envelope,
209 +tag: List<&2, U32>, +flag: Bool, +result: Result<&2, &2, AES.Error, List<&2, U32>>,
210 tag_matches: {envelope_tag_computed(words, aad, envelope) == tag : List<&2, U32>},
211 compare_matches: {auth_for_tag(envelope, tag) == flag : Bool},
212 branch_matches: {AES.decrypt_auth_result(words, envelope, flag) == result : Result<&2, &2, AES.Error, List<&2, U32>>}) ->
213 {decrypt_expanded(words, aad, envelope) == result : Result<&2, &2, AES.Error, List<&2, U32>>}:
214 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
215 decrypt_expanded(words, aad, envelope),
216 AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, envelope_tag_computed(words, aad, envelope))),
217 result, decrypt_auth_shape(words, aad, envelope),
218 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
219 AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, envelope_tag_computed(words, aad, envelope))),
220 AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, tag)), result,
221 Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>, actual_tag =>
222 AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, actual_tag)),
223 envelope_tag_computed(words, aad, envelope), tag, tag_matches),
224 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
225 AES.decrypt_auth_result(words, envelope, auth_for_tag(envelope, tag)),
226 AES.decrypt_auth_result(words, envelope, flag), result,
227 Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>, accepted => AES.decrypt_auth_result(words, envelope, accepted),
228 auth_for_tag(envelope, tag), flag, compare_matches), branch_matches)))
229
230def finish_decrypt(+key: AES.SecretKey, +aad: List<&2, U32>, +envelope: AES.Envelope,
231 +words: List<&2, U32>, +result: Result<&2, &2, AES.Error, List<&2, U32>>,
232 aad_ok: {AES.aad_valid(aad) == True{} : Bool},
233 ciphertext_ok: {AES.plaintext_valid(AES.ciphertext(envelope)) == True{} : Bool},
234 key_matches: {Core.aes256_expand(AES.secret_key_bytes(key)) == words : List<&2, U32>},
235 expanded_matches: {decrypt_expanded(words, aad, envelope) == result : Result<&2, &2, AES.Error, List<&2, U32>>}) ->
236 {AES.decrypt(key, aad, envelope) == result : Result<&2, &2, AES.Error, List<&2, U32>>}:
237 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
238 AES.decrypt(key, aad, envelope), AES.decrypt_authenticated(key, aad, envelope), result,
239 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
240 AES.decrypt_checked(key, aad, envelope, AES.aad_valid(aad), AES.plaintext_valid(AES.ciphertext(envelope))),
241 AES.decrypt_checked(key, aad, envelope, True{}, AES.plaintext_valid(AES.ciphertext(envelope))),
242 AES.decrypt_checked(key, aad, envelope, True{}, True{}),
243 Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>, flag =>
244 AES.decrypt_checked(key, aad, envelope, flag, AES.plaintext_valid(AES.ciphertext(envelope))),
245 AES.aad_valid(aad), True{}, aad_ok),
246 Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>, flag =>
247 AES.decrypt_checked(key, aad, envelope, True{}, flag),
248 AES.plaintext_valid(AES.ciphertext(envelope)), True{}, ciphertext_ok)),
249 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
250 AES.decrypt_authenticated(key, aad, envelope),
251 decrypt_expanded(Core.aes256_expand(AES.secret_key_bytes(key)), aad, envelope), result,
252 decrypt_key_shape(key, aad, envelope),
253 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
254 decrypt_expanded(Core.aes256_expand(AES.secret_key_bytes(key)), aad, envelope),
255 decrypt_expanded(words, aad, envelope), result,
256 Equal.cong(List<&2, U32>, Result<&2, &2, AES.Error, List<&2, U32>>, expanded_words =>
257 decrypt_expanded(expanded_words, aad, envelope),
258 Core.aes256_expand(AES.secret_key_bytes(key)), words, key_matches), expanded_matches)))