1 import Base 2 import ../LAWS.bend as L 3 import ../libs/AES256GCM.bend as AES 4 import ../libs/AES256GCMCore.bend as Core 5 6 def ciphertext(output: Core.GcmCiphertext) -> List<&2, U32>: 7 match output: 8 case Core.GcmCiphertext{bytes, valid}: bytes 9 10 def 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 18 def 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 31 def 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 35 def 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 41 def 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 50 def 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 57 def 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 62 def 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 70 def 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 78 def 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 105 def 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 138 def 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 144 def 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 150 def 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 156 def 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 177 def 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 180 def 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 197 def 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 200 def 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 208 def 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 230 def 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)))