1 import Base 2 import ../LAWS.bend as L 3 import ../libs/AES256GCM.bend as AES 4 import ../libs/AES256GCMCore.bend as Core 5 import ./AES_NistKeyScheduleProof.bend as Key 6 import ./AES_NistObservationProof.bend as Obs 7 import ./AES_NistTagProof.bend as TagProof 8 import ./AES_NistHashBlockProof.bend as Hash 9 import ./AES_NistCtrProof.bend as Ctr 10 import ./AES_NistCtr2BlockProof.bend as Ctr2 11 12 def 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 16 def empty_aad() -> List<&2, U32>: 17 [] 18 19 def empty_plaintext() -> List<&2, U32>: 20 [] 21 22 def empty_ciphertext() -> List<&2, U32>: 23 [] 24 25 def empty_tag() -> List<&2, U32>: 26 [253, 44, 170, 22, 165, 131, 46, 118, 170, 19, 44, 20, 83, 238, 218, 126] 27 28 def empty_auth() -> List<&2, U32>: 29 [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0] 30 31 def 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 35 def checkpoint_empty_ghash() -> 36 {TagProof.auth_from_hash(Hash.result(), empty_aad(), empty_ciphertext()) == empty_auth() : List<&2, U32>}: 37 {==} 38 39 def 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 44 def 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 51 def 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 55 def 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 66 def 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 72 def multiblock_aad() -> List<&2, U32>: 73 [] 74 75 def 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 78 def 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 81 def multiblock_tag() -> List<&2, U32>: 82 [176, 148, 218, 197, 217, 52, 113, 189, 236, 26, 80, 34, 112, 227, 204, 108] 83 84 def multiblock_auth() -> List<&2, U32>: 85 [77,184,112,211,124,183,95,203,70,9,124,54,35,13,22,18] 86 87 def 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 93 def 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 99 def 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 103 def checkpoint_multiblock_ghash() -> 104 {TagProof.auth_from_hash(Hash.result(), multiblock_aad(), multiblock_ciphertext()) == multiblock_auth() : List<&2, U32>}: 105 {==} 106 107 def 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 112 def 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 119 def 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 123 def 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 134 def 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 140 def 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 143 def aad_only_plaintext() -> List<&2, U32>: 144 [] 145 146 def aad_only_ciphertext() -> List<&2, U32>: 147 [] 148 149 def aad_only_tag() -> List<&2, U32>: 150 [222, 52, 182, 220, 212, 206, 226, 253, 190, 195, 206, 160, 26, 241, 238, 68] 151 152 def aad_only_auth() -> List<&2, U32>: 153 [35,24,28,202,113,77,204,139,20,208,226,180,73,31,52,58] 154 155 def 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 159 def 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 163 def 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 168 def 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 175 def 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 179 def 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 190 def 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 196 def 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 199 def 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 202 def 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 205 def 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 208 def 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 211 def 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 217 def 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 223 def 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 227 def 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 231 def 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 236 def 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 243 def 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 247 def 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 258 def 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 264 def 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 267 def 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 270 def 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 273 def partial_block_tag() -> List<&2, U32>: 274 [224, 151, 25, 95, 69, 50, 218, 137, 95, 185, 23, 165, 165, 92, 106, 160] 275 276 def partial_block_auth() -> List<&2, U32>: 277 [29,187,179,73,224,177,244,255,245,170,59,177,246,178,176,222] 278 279 def 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 285 def 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 291 def 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 295 def 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 299 def 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 304 def 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 311 def 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 315 def 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 326 def 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())