proof/AES_NistVectorProof.bend
qasim-bend-kit@0.1.0.2 · 330 lines · 67 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
5import qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend as Key
6import qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend as Obs
7import qasim-bend-kit@0.1.0.2/proof/AES_NistTagProof.bend as TagProof
8import qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend as Hash
9import qasim-bend-kit@0.1.0.2/proof/AES_NistCtrProof.bend as Ctr
10import qasim-bend-kit@0.1.0.2/proof/AES_NistCtr2BlockProof.bend as Ctr2
11
12def checkpoint_nist_schedule() ->
13 {Core.aes256_expand(AES.secret_key_bytes(L.aes256gcm_nist_key())) == Key.words_60() : List<&2, U32>}:
14 Obs.schedule_input_matches(L.aes256gcm_nist_key(), Key.key_bytes(), Key.words_60(), {==}, Key.key_schedule_matches())
15
16def empty_aad() -> List<&2, U32>:
17 []
18
19def empty_plaintext() -> List<&2, U32>:
20 []
21
22def empty_ciphertext() -> List<&2, U32>:
23 []
24
25def empty_tag() -> List<&2, U32>:
26 [253, 44, 170, 22, 165, 131, 46, 118, 170, 19, 44, 20, 83, 238, 218, 126]
27
28def empty_auth() -> List<&2, U32>:
29 [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
30
31def checkpoint_empty_ciphertext() ->
32 {Obs.ciphertext(Core.gcm_ctr_encrypt(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), empty_plaintext())) == empty_ciphertext() : List<&2, U32>}:
33 {==}
34
35def checkpoint_empty_ghash() ->
36 {TagProof.auth_from_hash(Hash.result(), empty_aad(), empty_ciphertext()) == empty_auth() : List<&2, U32>}:
37 {==}
38
39def checkpoint_empty_tag() ->
40 {Core.gcm_tag_bytes(Core.gcm_tag_output(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), empty_aad(), empty_ciphertext())) == empty_tag() : List<&2, U32>}:
41 TagProof.nist_tag(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), empty_aad(), empty_ciphertext(),
42 empty_auth(), empty_tag(), {==}, checkpoint_empty_ghash(), {==})
43
44def empty_encrypt() ->
45 {L.aes256gcm_nist_encrypt_observation(AES.encrypt(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(), empty_aad(), empty_plaintext())) ==
46 L.aes256gcm_nist_encrypt_observation(Done{L.aes256gcm_nist_empty()}) : List<&2, U32>}:
47 Obs.finish_encrypt(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(),
48 empty_aad(), empty_plaintext(), Key.words_60(), empty_ciphertext(), empty_tag(),
49 {==}, {==}, checkpoint_nist_schedule(), checkpoint_empty_ciphertext(), checkpoint_empty_tag())
50
51def checkpoint_empty_plaintext() ->
52 {Core.gcm_decrypt_expanded(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), empty_ciphertext()) == empty_plaintext() : List<&2, U32>}:
53 {==}
54
55def checkpoint_empty_authenticated() ->
56 {Obs.decrypt_expanded(Key.words_60(), empty_aad(), L.aes256gcm_nist_empty()) == Done{empty_plaintext()} : Result<&2, &2, AES.Error, List<&2, U32>>}:
57 Obs.finish_auth(Key.words_60(), empty_aad(), L.aes256gcm_nist_empty(),
58 empty_tag(), True{}, Done{empty_plaintext()},
59 Obs.tag_parameters(Key.words_60(), empty_aad(), L.aes256gcm_nist_empty(),
60 AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), empty_ciphertext(), empty_tag(),
61 {==}, {==}, checkpoint_empty_tag()), {==},
62 Obs.payload_parameters(Key.words_60(), L.aes256gcm_nist_empty(),
63 AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), empty_ciphertext(), empty_plaintext(),
64 {==}, {==}, checkpoint_empty_plaintext()))
65
66def empty_decrypt() ->
67 {AES.decrypt(L.aes256gcm_nist_key(), empty_aad(), L.aes256gcm_nist_empty()) == Done{empty_plaintext()} : Result<&2, &2, AES.Error, List<&2, U32>>}:
68 Obs.finish_decrypt(L.aes256gcm_nist_key(), empty_aad(), L.aes256gcm_nist_empty(),
69 Key.words_60(), Done{empty_plaintext()}, {==}, {==}, checkpoint_nist_schedule(),
70 checkpoint_empty_authenticated())
71
72def multiblock_aad() -> List<&2, U32>:
73 []
74
75def multiblock_plaintext() -> List<&2, U32>:
76 [217, 49, 50, 37, 248, 132, 6, 229, 165, 89, 9, 197, 175, 245, 38, 154, 134, 167, 169, 83, 21, 52, 247, 218, 46, 76, 48, 61, 138, 49, 138, 114, 28, 60, 12, 149, 149, 104, 9, 83, 47, 207, 14, 36, 73, 166, 181, 37, 177, 106, 237, 245, 170, 13, 230, 87, 186, 99, 123, 57, 26, 175, 210, 85]
77
78def multiblock_ciphertext() -> List<&2, U32>:
79 [82, 45, 193, 240, 153, 86, 125, 7, 244, 127, 55, 163, 42, 132, 66, 125, 100, 58, 140, 220, 191, 229, 192, 201, 117, 152, 162, 189, 37, 85, 209, 170, 140, 176, 142, 72, 89, 13, 187, 61, 167, 176, 139, 16, 86, 130, 136, 56, 197, 246, 30, 99, 147, 186, 122, 10, 188, 201, 246, 98, 137, 128, 21, 173]
80
81def multiblock_tag() -> List<&2, U32>:
82 [176, 148, 218, 197, 217, 52, 113, 189, 236, 26, 80, 34, 112, 227, 204, 108]
83
84def multiblock_auth() -> List<&2, U32>:
85 [77,184,112,211,124,183,95,203,70,9,124,54,35,13,22,18]
86
87def checkpoint_multiblock_plaintext_stream() ->
88 {Core.gcm_ctr_stream_exact(List.length(&2, U32, multiblock_plaintext()), Key.words_60(), Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce())))) == Ctr.stream_64() : List<&2, U32>}:
89 Obs.stream_parameters(List.length(&2, U32, multiblock_plaintext()), Key.words_60(),
90 Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()))), 64n, Ctr2.block(), Ctr.stream_64(),
91 {==}, {==}, Ctr.checkpoint_stream_64())
92
93def checkpoint_multiblock_ciphertext_stream() ->
94 {Core.gcm_ctr_stream_exact(List.length(&2, U32, multiblock_ciphertext()), Key.words_60(), Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce())))) == Ctr.stream_64() : List<&2, U32>}:
95 Obs.stream_parameters(List.length(&2, U32, multiblock_ciphertext()), Key.words_60(),
96 Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()))), 64n, Ctr2.block(), Ctr.stream_64(),
97 {==}, {==}, Ctr.checkpoint_stream_64())
98
99def checkpoint_multiblock_ciphertext() ->
100 {Obs.ciphertext(Core.gcm_ctr_encrypt(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), multiblock_plaintext())) == multiblock_ciphertext() : List<&2, U32>}:
101 Obs.finish_cipher(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), multiblock_plaintext(), Ctr.stream_64(), multiblock_ciphertext(), checkpoint_multiblock_plaintext_stream(), {==})
102
103def checkpoint_multiblock_ghash() ->
104 {TagProof.auth_from_hash(Hash.result(), multiblock_aad(), multiblock_ciphertext()) == multiblock_auth() : List<&2, U32>}:
105 {==}
106
107def checkpoint_multiblock_tag() ->
108 {Core.gcm_tag_bytes(Core.gcm_tag_output(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), multiblock_aad(), multiblock_ciphertext())) == multiblock_tag() : List<&2, U32>}:
109 TagProof.nist_tag(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), multiblock_aad(), multiblock_ciphertext(),
110 multiblock_auth(), multiblock_tag(), {==}, checkpoint_multiblock_ghash(), {==})
111
112def multiblock_encrypt() ->
113 {L.aes256gcm_nist_encrypt_observation(AES.encrypt(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(), multiblock_aad(), multiblock_plaintext())) ==
114 L.aes256gcm_nist_encrypt_observation(Done{L.aes256gcm_nist_multiblock()}) : List<&2, U32>}:
115 Obs.finish_encrypt(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(),
116 multiblock_aad(), multiblock_plaintext(), Key.words_60(), multiblock_ciphertext(), multiblock_tag(),
117 {==}, {==}, checkpoint_nist_schedule(), checkpoint_multiblock_ciphertext(), checkpoint_multiblock_tag())
118
119def checkpoint_multiblock_plaintext() ->
120 {Core.gcm_decrypt_expanded(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), multiblock_ciphertext()) == multiblock_plaintext() : List<&2, U32>}:
121 Equal.trans(List<&2, U32>, Core.gcm_decrypt_expanded(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), multiblock_ciphertext()), Core.gcm_zip_xor(multiblock_ciphertext(), Ctr.stream_64()), multiblock_plaintext(), Obs.xor_from_stream(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), multiblock_ciphertext(), Ctr.stream_64(), checkpoint_multiblock_ciphertext_stream()), {==})
122
123def checkpoint_multiblock_authenticated() ->
124 {Obs.decrypt_expanded(Key.words_60(), multiblock_aad(), L.aes256gcm_nist_multiblock()) == Done{multiblock_plaintext()} : Result<&2, &2, AES.Error, List<&2, U32>>}:
125 Obs.finish_auth(Key.words_60(), multiblock_aad(), L.aes256gcm_nist_multiblock(),
126 multiblock_tag(), True{}, Done{multiblock_plaintext()},
127 Obs.tag_parameters(Key.words_60(), multiblock_aad(), L.aes256gcm_nist_multiblock(),
128 AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), multiblock_ciphertext(), multiblock_tag(),
129 {==}, {==}, checkpoint_multiblock_tag()), {==},
130 Obs.payload_parameters(Key.words_60(), L.aes256gcm_nist_multiblock(),
131 AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), multiblock_ciphertext(), multiblock_plaintext(),
132 {==}, {==}, checkpoint_multiblock_plaintext()))
133
134def multiblock_decrypt() ->
135 {AES.decrypt(L.aes256gcm_nist_key(), multiblock_aad(), L.aes256gcm_nist_multiblock()) == Done{multiblock_plaintext()} : Result<&2, &2, AES.Error, List<&2, U32>>}:
136 Obs.finish_decrypt(L.aes256gcm_nist_key(), multiblock_aad(), L.aes256gcm_nist_multiblock(),
137 Key.words_60(), Done{multiblock_plaintext()}, {==}, {==}, checkpoint_nist_schedule(),
138 checkpoint_multiblock_authenticated())
139
140def aad_only_aad() -> List<&2, U32>:
141 [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133, 3, 185, 105, 157, 231, 133, 137, 90, 150, 253, 186, 175, 67, 177, 205, 127, 89, 142, 206, 35, 136, 27, 0, 227, 237, 3, 6, 136, 123, 12, 120, 94, 39, 232, 173, 63, 130, 35, 32, 113, 4, 114, 93, 212]
142
143def aad_only_plaintext() -> List<&2, U32>:
144 []
145
146def aad_only_ciphertext() -> List<&2, U32>:
147 []
148
149def aad_only_tag() -> List<&2, U32>:
150 [222, 52, 182, 220, 212, 206, 226, 253, 190, 195, 206, 160, 26, 241, 238, 68]
151
152def aad_only_auth() -> List<&2, U32>:
153 [35,24,28,202,113,77,204,139,20,208,226,180,73,31,52,58]
154
155def checkpoint_aad_only_ciphertext() ->
156 {Obs.ciphertext(Core.gcm_ctr_encrypt(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_only_plaintext())) == aad_only_ciphertext() : List<&2, U32>}:
157 {==}
158
159def checkpoint_aad_only_ghash() ->
160 {TagProof.auth_from_hash(Hash.result(), aad_only_aad(), aad_only_ciphertext()) == aad_only_auth() : List<&2, U32>}:
161 {==}
162
163def checkpoint_aad_only_tag() ->
164 {Core.gcm_tag_bytes(Core.gcm_tag_output(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_only_aad(), aad_only_ciphertext())) == aad_only_tag() : List<&2, U32>}:
165 TagProof.nist_tag(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_only_aad(), aad_only_ciphertext(),
166 aad_only_auth(), aad_only_tag(), {==}, checkpoint_aad_only_ghash(), {==})
167
168def aad_only_encrypt() ->
169 {L.aes256gcm_nist_encrypt_observation(AES.encrypt(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(), aad_only_aad(), aad_only_plaintext())) ==
170 L.aes256gcm_nist_encrypt_observation(Done{L.aes256gcm_nist_aad_only()}) : List<&2, U32>}:
171 Obs.finish_encrypt(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(),
172 aad_only_aad(), aad_only_plaintext(), Key.words_60(), aad_only_ciphertext(), aad_only_tag(),
173 {==}, {==}, checkpoint_nist_schedule(), checkpoint_aad_only_ciphertext(), checkpoint_aad_only_tag())
174
175def checkpoint_aad_only_plaintext() ->
176 {Core.gcm_decrypt_expanded(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_only_ciphertext()) == aad_only_plaintext() : List<&2, U32>}:
177 {==}
178
179def checkpoint_aad_only_authenticated() ->
180 {Obs.decrypt_expanded(Key.words_60(), aad_only_aad(), L.aes256gcm_nist_aad_only()) == Done{aad_only_plaintext()} : Result<&2, &2, AES.Error, List<&2, U32>>}:
181 Obs.finish_auth(Key.words_60(), aad_only_aad(), L.aes256gcm_nist_aad_only(),
182 aad_only_tag(), True{}, Done{aad_only_plaintext()},
183 Obs.tag_parameters(Key.words_60(), aad_only_aad(), L.aes256gcm_nist_aad_only(),
184 AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_only_ciphertext(), aad_only_tag(),
185 {==}, {==}, checkpoint_aad_only_tag()), {==},
186 Obs.payload_parameters(Key.words_60(), L.aes256gcm_nist_aad_only(),
187 AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_only_ciphertext(), aad_only_plaintext(),
188 {==}, {==}, checkpoint_aad_only_plaintext()))
189
190def aad_only_decrypt() ->
191 {AES.decrypt(L.aes256gcm_nist_key(), aad_only_aad(), L.aes256gcm_nist_aad_only()) == Done{aad_only_plaintext()} : Result<&2, &2, AES.Error, List<&2, U32>>}:
192 Obs.finish_decrypt(L.aes256gcm_nist_key(), aad_only_aad(), L.aes256gcm_nist_aad_only(),
193 Key.words_60(), Done{aad_only_plaintext()}, {==}, {==}, checkpoint_nist_schedule(),
194 checkpoint_aad_only_authenticated())
195
196def aad_and_multiblock_aad() -> List<&2, U32>:
197 [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133, 3, 185, 105, 157, 231, 133, 137, 90, 150, 253, 186, 175, 67, 177, 205, 127, 89, 142, 206, 35, 136, 27, 0, 227, 237, 3, 6, 136, 123, 12, 120, 94, 39, 232, 173, 63, 130, 35, 32, 113, 4, 114, 93, 212]
198
199def aad_and_multiblock_plaintext() -> List<&2, U32>:
200 [217, 49, 50, 37, 248, 132, 6, 229, 165, 89, 9, 197, 175, 245, 38, 154, 134, 167, 169, 83, 21, 52, 247, 218, 46, 76, 48, 61, 138, 49, 138, 114, 28, 60, 12, 149, 149, 104, 9, 83, 47, 207, 14, 36, 73, 166, 181, 37, 177, 106, 237, 245, 170, 13, 230, 87, 186, 99, 123, 57, 26, 175, 210, 85]
201
202def aad_and_multiblock_ciphertext() -> List<&2, U32>:
203 [82, 45, 193, 240, 153, 86, 125, 7, 244, 127, 55, 163, 42, 132, 66, 125, 100, 58, 140, 220, 191, 229, 192, 201, 117, 152, 162, 189, 37, 85, 209, 170, 140, 176, 142, 72, 89, 13, 187, 61, 167, 176, 139, 16, 86, 130, 136, 56, 197, 246, 30, 99, 147, 186, 122, 10, 188, 201, 246, 98, 137, 128, 21, 173]
204
205def aad_and_multiblock_tag() -> List<&2, U32>:
206 [192, 109, 118, 243, 25, 48, 254, 243, 122, 202, 226, 62, 212, 101, 174, 98]
207
208def aad_and_multiblock_auth() -> List<&2, U32>:
209 [61,65,220,229,188,179,208,133,208,217,206,42,135,139,116,28]
210
211def checkpoint_aad_and_multiblock_plaintext_stream() ->
212 {Core.gcm_ctr_stream_exact(List.length(&2, U32, aad_and_multiblock_plaintext()), Key.words_60(), Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce())))) == Ctr.stream_64() : List<&2, U32>}:
213 Obs.stream_parameters(List.length(&2, U32, aad_and_multiblock_plaintext()), Key.words_60(),
214 Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()))), 64n, Ctr2.block(), Ctr.stream_64(),
215 {==}, {==}, Ctr.checkpoint_stream_64())
216
217def checkpoint_aad_and_multiblock_ciphertext_stream() ->
218 {Core.gcm_ctr_stream_exact(List.length(&2, U32, aad_and_multiblock_ciphertext()), Key.words_60(), Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce())))) == Ctr.stream_64() : List<&2, U32>}:
219 Obs.stream_parameters(List.length(&2, U32, aad_and_multiblock_ciphertext()), Key.words_60(),
220 Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()))), 64n, Ctr2.block(), Ctr.stream_64(),
221 {==}, {==}, Ctr.checkpoint_stream_64())
222
223def checkpoint_aad_and_multiblock_ciphertext() ->
224 {Obs.ciphertext(Core.gcm_ctr_encrypt(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_and_multiblock_plaintext())) == aad_and_multiblock_ciphertext() : List<&2, U32>}:
225 Obs.finish_cipher(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_and_multiblock_plaintext(), Ctr.stream_64(), aad_and_multiblock_ciphertext(), checkpoint_aad_and_multiblock_plaintext_stream(), {==})
226
227def checkpoint_aad_and_multiblock_ghash() ->
228 {TagProof.auth_from_hash(Hash.result(), aad_and_multiblock_aad(), aad_and_multiblock_ciphertext()) == aad_and_multiblock_auth() : List<&2, U32>}:
229 {==}
230
231def checkpoint_aad_and_multiblock_tag() ->
232 {Core.gcm_tag_bytes(Core.gcm_tag_output(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_and_multiblock_aad(), aad_and_multiblock_ciphertext())) == aad_and_multiblock_tag() : List<&2, U32>}:
233 TagProof.nist_tag(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_and_multiblock_aad(), aad_and_multiblock_ciphertext(),
234 aad_and_multiblock_auth(), aad_and_multiblock_tag(), {==}, checkpoint_aad_and_multiblock_ghash(), {==})
235
236def aad_and_multiblock_encrypt() ->
237 {L.aes256gcm_nist_encrypt_observation(AES.encrypt(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(), aad_and_multiblock_aad(), aad_and_multiblock_plaintext())) ==
238 L.aes256gcm_nist_encrypt_observation(Done{L.aes256gcm_nist_aad_and_multiblock()}) : List<&2, U32>}:
239 Obs.finish_encrypt(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(),
240 aad_and_multiblock_aad(), aad_and_multiblock_plaintext(), Key.words_60(), aad_and_multiblock_ciphertext(), aad_and_multiblock_tag(),
241 {==}, {==}, checkpoint_nist_schedule(), checkpoint_aad_and_multiblock_ciphertext(), checkpoint_aad_and_multiblock_tag())
242
243def checkpoint_aad_and_multiblock_plaintext() ->
244 {Core.gcm_decrypt_expanded(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_and_multiblock_ciphertext()) == aad_and_multiblock_plaintext() : List<&2, U32>}:
245 Equal.trans(List<&2, U32>, Core.gcm_decrypt_expanded(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_and_multiblock_ciphertext()), Core.gcm_zip_xor(aad_and_multiblock_ciphertext(), Ctr.stream_64()), aad_and_multiblock_plaintext(), Obs.xor_from_stream(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_and_multiblock_ciphertext(), Ctr.stream_64(), checkpoint_aad_and_multiblock_ciphertext_stream()), {==})
246
247def checkpoint_aad_and_multiblock_authenticated() ->
248 {Obs.decrypt_expanded(Key.words_60(), aad_and_multiblock_aad(), L.aes256gcm_nist_aad_and_multiblock()) == Done{aad_and_multiblock_plaintext()} : Result<&2, &2, AES.Error, List<&2, U32>>}:
249 Obs.finish_auth(Key.words_60(), aad_and_multiblock_aad(), L.aes256gcm_nist_aad_and_multiblock(),
250 aad_and_multiblock_tag(), True{}, Done{aad_and_multiblock_plaintext()},
251 Obs.tag_parameters(Key.words_60(), aad_and_multiblock_aad(), L.aes256gcm_nist_aad_and_multiblock(),
252 AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_and_multiblock_ciphertext(), aad_and_multiblock_tag(),
253 {==}, {==}, checkpoint_aad_and_multiblock_tag()), {==},
254 Obs.payload_parameters(Key.words_60(), L.aes256gcm_nist_aad_and_multiblock(),
255 AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), aad_and_multiblock_ciphertext(), aad_and_multiblock_plaintext(),
256 {==}, {==}, checkpoint_aad_and_multiblock_plaintext()))
257
258def aad_and_multiblock_decrypt() ->
259 {AES.decrypt(L.aes256gcm_nist_key(), aad_and_multiblock_aad(), L.aes256gcm_nist_aad_and_multiblock()) == Done{aad_and_multiblock_plaintext()} : Result<&2, &2, AES.Error, List<&2, U32>>}:
260 Obs.finish_decrypt(L.aes256gcm_nist_key(), aad_and_multiblock_aad(), L.aes256gcm_nist_aad_and_multiblock(),
261 Key.words_60(), Done{aad_and_multiblock_plaintext()}, {==}, {==}, checkpoint_nist_schedule(),
262 checkpoint_aad_and_multiblock_authenticated())
263
264def partial_block_aad() -> List<&2, U32>:
265 [58, 215, 123, 180, 13, 122, 54, 96, 168, 158, 202, 243, 36, 102, 239, 151, 245, 211, 213, 133]
266
267def partial_block_plaintext() -> List<&2, U32>:
268 [217, 49, 50, 37, 248, 132, 6, 229, 165, 89, 9, 197, 175, 245, 38, 154, 134, 167, 169, 83, 21, 52, 247, 218, 46, 76, 48, 61, 138, 49, 138, 114, 28, 60, 12, 149, 149, 104, 9, 83, 47, 207, 14, 36, 73, 166, 181, 37, 177, 106, 237, 245, 170, 13, 230, 87, 186, 99, 123, 57]
269
270def partial_block_ciphertext() -> List<&2, U32>:
271 [82, 45, 193, 240, 153, 86, 125, 7, 244, 127, 55, 163, 42, 132, 66, 125, 100, 58, 140, 220, 191, 229, 192, 201, 117, 152, 162, 189, 37, 85, 209, 170, 140, 176, 142, 72, 89, 13, 187, 61, 167, 176, 139, 16, 86, 130, 136, 56, 197, 246, 30, 99, 147, 186, 122, 10, 188, 201, 246, 98]
272
273def partial_block_tag() -> List<&2, U32>:
274 [224, 151, 25, 95, 69, 50, 218, 137, 95, 185, 23, 165, 165, 92, 106, 160]
275
276def partial_block_auth() -> List<&2, U32>:
277 [29,187,179,73,224,177,244,255,245,170,59,177,246,178,176,222]
278
279def checkpoint_partial_block_plaintext_stream() ->
280 {Core.gcm_ctr_stream_exact(List.length(&2, U32, partial_block_plaintext()), Key.words_60(), Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce())))) == Ctr.stream_60() : List<&2, U32>}:
281 Obs.stream_parameters(List.length(&2, U32, partial_block_plaintext()), Key.words_60(),
282 Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()))), 60n, Ctr2.block(), Ctr.stream_60(),
283 {==}, {==}, Ctr.checkpoint_stream_60())
284
285def checkpoint_partial_block_ciphertext_stream() ->
286 {Core.gcm_ctr_stream_exact(List.length(&2, U32, partial_block_ciphertext()), Key.words_60(), Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce())))) == Ctr.stream_60() : List<&2, U32>}:
287 Obs.stream_parameters(List.length(&2, U32, partial_block_ciphertext()), Key.words_60(),
288 Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()))), 60n, Ctr2.block(), Ctr.stream_60(),
289 {==}, {==}, Ctr.checkpoint_stream_60())
290
291def checkpoint_partial_block_ciphertext() ->
292 {Obs.ciphertext(Core.gcm_ctr_encrypt(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_plaintext())) == partial_block_ciphertext() : List<&2, U32>}:
293 Obs.finish_cipher(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_plaintext(), Ctr.stream_60(), partial_block_ciphertext(), checkpoint_partial_block_plaintext_stream(), {==})
294
295def checkpoint_partial_block_ghash() ->
296 {TagProof.auth_from_hash(Hash.result(), partial_block_aad(), partial_block_ciphertext()) == partial_block_auth() : List<&2, U32>}:
297 {==}
298
299def checkpoint_partial_block_tag() ->
300 {Core.gcm_tag_bytes(Core.gcm_tag_output(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_aad(), partial_block_ciphertext())) == partial_block_tag() : List<&2, U32>}:
301 TagProof.nist_tag(AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_aad(), partial_block_ciphertext(),
302 partial_block_auth(), partial_block_tag(), {==}, checkpoint_partial_block_ghash(), {==})
303
304def partial_block_encrypt() ->
305 {L.aes256gcm_nist_encrypt_observation(AES.encrypt(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(), partial_block_aad(), partial_block_plaintext())) ==
306 L.aes256gcm_nist_encrypt_observation(Done{L.aes256gcm_nist_partial_block()}) : List<&2, U32>}:
307 Obs.finish_encrypt(L.aes256gcm_nist_key(), L.aes256gcm_nist_nonce(),
308 partial_block_aad(), partial_block_plaintext(), Key.words_60(), partial_block_ciphertext(), partial_block_tag(),
309 {==}, {==}, checkpoint_nist_schedule(), checkpoint_partial_block_ciphertext(), checkpoint_partial_block_tag())
310
311def checkpoint_partial_block_plaintext() ->
312 {Core.gcm_decrypt_expanded(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_ciphertext()) == partial_block_plaintext() : List<&2, U32>}:
313 Equal.trans(List<&2, U32>, Core.gcm_decrypt_expanded(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_ciphertext()), Core.gcm_zip_xor(partial_block_ciphertext(), Ctr.stream_60()), partial_block_plaintext(), Obs.xor_from_stream(Key.words_60(), AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_ciphertext(), Ctr.stream_60(), checkpoint_partial_block_ciphertext_stream()), {==})
314
315def checkpoint_partial_block_authenticated() ->
316 {Obs.decrypt_expanded(Key.words_60(), partial_block_aad(), L.aes256gcm_nist_partial_block()) == Done{partial_block_plaintext()} : Result<&2, &2, AES.Error, List<&2, U32>>}:
317 Obs.finish_auth(Key.words_60(), partial_block_aad(), L.aes256gcm_nist_partial_block(),
318 partial_block_tag(), True{}, Done{partial_block_plaintext()},
319 Obs.tag_parameters(Key.words_60(), partial_block_aad(), L.aes256gcm_nist_partial_block(),
320 AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_ciphertext(), partial_block_tag(),
321 {==}, {==}, checkpoint_partial_block_tag()), {==},
322 Obs.payload_parameters(Key.words_60(), L.aes256gcm_nist_partial_block(),
323 AES.raw_nonce_bytes(L.aes256gcm_nist_nonce()), partial_block_ciphertext(), partial_block_plaintext(),
324 {==}, {==}, checkpoint_partial_block_plaintext()))
325
326def partial_block_decrypt() ->
327 {AES.decrypt(L.aes256gcm_nist_key(), partial_block_aad(), L.aes256gcm_nist_partial_block()) == Done{partial_block_plaintext()} : Result<&2, &2, AES.Error, List<&2, U32>>}:
328 Obs.finish_decrypt(L.aes256gcm_nist_key(), partial_block_aad(), L.aes256gcm_nist_partial_block(),
329 Key.words_60(), Done{partial_block_plaintext()}, {==}, {==}, checkpoint_nist_schedule(),
330 checkpoint_partial_block_authenticated())