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_NistVectorProof.bend as V 8 9 def zero_words() -> List<&2, U32>: 10 [0, 0, 0, 0, 0, 0, 0, 0, 1650680675, 1650680675, 1650680675, 1650680675, 2868640763, 2868640763, 2868640763, 2868640763, 1869376719, 219090860, 1869376719, 219090860, 2106428778, 3614865041, 2106428778, 3614865041, 1398074817, 1583080045, 825724578, 1010336014, 2525659585, 1107097424, 1014069818, 3943107755, 2661977896, 3237047621, 4056343527, 3456000745, 724642783, 1791876239, 1455204021, 3183192606, 1678179666, 2767687703, 1429304304, 2563707161, 1841015051, 125203844, 1372246833, 3966859567, 3887130780, 1128757387, 376834939, 2394495586, 1961692065, 1939570213, 575778068, 3458257979, 284690967, 1405055644, 1170831847, 3413140357] 11 12 def zero_key() -> AES.SecretKey: 13 AES.SecretKey{[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], {==}, {==}} 14 15 def checkpoint_zero_key() -> 16 {Core.aes256_expand(AES.secret_key_bytes(zero_key())) == zero_words() : List<&2, U32>}: 17 {==} 18 19 def changed_aad_aad() -> List<&2, U32>: 20 [1] 21 22 def changed_aad_computed_tag() -> List<&2, U32>: 23 [234, 201, 142, 11, 241, 133, 165, 69, 86, 235, 98, 228, 188, 36, 2, 6] 24 25 def changed_aad_envelope() -> AES.Envelope: 26 AES.Envelope{AES.Nonce{[202, 254, 186, 190, 250, 206, 219, 173, 222, 202, 248, 136], {==}, {==}}, [], 27 AES.Tag{V.empty_tag(), {==}, {==}}, {==}} 28 29 def checkpoint_changed_aad_tag() -> 30 {Obs.envelope_tag_computed(Key.words_60(), changed_aad_aad(), changed_aad_envelope()) == changed_aad_computed_tag() : List<&2, U32>}: 31 {==} 32 33 def checkpoint_changed_aad_rejected() -> 34 {Obs.decrypt_expanded(Key.words_60(), changed_aad_aad(), changed_aad_envelope()) == Fail{AES.AuthenticationFailed{}} : Result<&2, &2, AES.Error, List<&2, U32>>}: 35 Obs.finish_auth(Key.words_60(), changed_aad_aad(), changed_aad_envelope(), 36 changed_aad_computed_tag(), False{}, Fail{AES.AuthenticationFailed{}}, 37 checkpoint_changed_aad_tag(), {==}, {==}) 38 39 def rejects_changed_aad() -> 40 {AES.decrypt(L.aes256gcm_nist_key(), changed_aad_aad(), changed_aad_envelope()) == Fail{AES.AuthenticationFailed{}} : Result<&2, &2, AES.Error, List<&2, U32>>}: 41 Obs.finish_decrypt(L.aes256gcm_nist_key(), changed_aad_aad(), changed_aad_envelope(), 42 Key.words_60(), Fail{AES.AuthenticationFailed{}}, {==}, {==}, V.checkpoint_nist_schedule(), checkpoint_changed_aad_rejected()) 43 44 def changed_key_aad() -> List<&2, U32>: 45 [] 46 47 def changed_key_computed_tag() -> List<&2, U32>: 48 [239, 143, 216, 178, 152, 53, 97, 46, 103, 163, 19, 50, 155, 145, 168, 216] 49 50 def changed_key_envelope() -> AES.Envelope: 51 AES.Envelope{AES.Nonce{[202, 254, 186, 190, 250, 206, 219, 173, 222, 202, 248, 136], {==}, {==}}, [], 52 AES.Tag{V.empty_tag(), {==}, {==}}, {==}} 53 54 def checkpoint_changed_key_tag() -> 55 {Obs.envelope_tag_computed(zero_words(), changed_key_aad(), changed_key_envelope()) == changed_key_computed_tag() : List<&2, U32>}: 56 {==} 57 58 def checkpoint_changed_key_rejected() -> 59 {Obs.decrypt_expanded(zero_words(), changed_key_aad(), changed_key_envelope()) == Fail{AES.AuthenticationFailed{}} : Result<&2, &2, AES.Error, List<&2, U32>>}: 60 Obs.finish_auth(zero_words(), changed_key_aad(), changed_key_envelope(), 61 changed_key_computed_tag(), False{}, Fail{AES.AuthenticationFailed{}}, 62 checkpoint_changed_key_tag(), {==}, {==}) 63 64 def rejects_changed_key() -> 65 {AES.decrypt(zero_key(), changed_key_aad(), changed_key_envelope()) == Fail{AES.AuthenticationFailed{}} : Result<&2, &2, AES.Error, List<&2, U32>>}: 66 Obs.finish_decrypt(zero_key(), changed_key_aad(), changed_key_envelope(), 67 zero_words(), Fail{AES.AuthenticationFailed{}}, {==}, {==}, checkpoint_zero_key(), checkpoint_changed_key_rejected()) 68 69 def changed_nonce_aad() -> List<&2, U32>: 70 [] 71 72 def changed_nonce_computed_tag() -> List<&2, U32>: 73 [233, 144, 99, 34, 140, 197, 191, 38, 223, 98, 138, 58, 82, 20, 52, 245] 74 75 def changed_nonce_envelope() -> AES.Envelope: 76 AES.Envelope{AES.Nonce{[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], {==}, {==}}, [], 77 AES.Tag{V.empty_tag(), {==}, {==}}, {==}} 78 79 def checkpoint_changed_nonce_tag() -> 80 {Obs.envelope_tag_computed(Key.words_60(), changed_nonce_aad(), changed_nonce_envelope()) == changed_nonce_computed_tag() : List<&2, U32>}: 81 {==} 82 83 def checkpoint_changed_nonce_rejected() -> 84 {Obs.decrypt_expanded(Key.words_60(), changed_nonce_aad(), changed_nonce_envelope()) == Fail{AES.AuthenticationFailed{}} : Result<&2, &2, AES.Error, List<&2, U32>>}: 85 Obs.finish_auth(Key.words_60(), changed_nonce_aad(), changed_nonce_envelope(), 86 changed_nonce_computed_tag(), False{}, Fail{AES.AuthenticationFailed{}}, 87 checkpoint_changed_nonce_tag(), {==}, {==}) 88 89 def rejects_changed_nonce() -> 90 {AES.decrypt(L.aes256gcm_nist_key(), changed_nonce_aad(), changed_nonce_envelope()) == Fail{AES.AuthenticationFailed{}} : Result<&2, &2, AES.Error, List<&2, U32>>}: 91 Obs.finish_decrypt(L.aes256gcm_nist_key(), changed_nonce_aad(), changed_nonce_envelope(), 92 Key.words_60(), Fail{AES.AuthenticationFailed{}}, {==}, {==}, V.checkpoint_nist_schedule(), checkpoint_changed_nonce_rejected()) 93 94 def changed_ciphertext_aad() -> List<&2, U32>: 95 [] 96 97 def changed_ciphertext_computed_tag() -> List<&2, U32>: 98 [121, 67, 50, 73, 40, 25, 211, 209, 162, 58, 88, 216, 225, 249, 199, 126] 99 100 def changed_ciphertext_envelope() -> AES.Envelope: 101 AES.Envelope{AES.Nonce{[202, 254, 186, 190, 250, 206, 219, 173, 222, 202, 248, 136], {==}, {==}}, [1], 102 AES.Tag{V.empty_tag(), {==}, {==}}, {==}} 103 104 def checkpoint_changed_ciphertext_tag() -> 105 {Obs.envelope_tag_computed(Key.words_60(), changed_ciphertext_aad(), changed_ciphertext_envelope()) == changed_ciphertext_computed_tag() : List<&2, U32>}: 106 {==} 107 108 def checkpoint_changed_ciphertext_rejected() -> 109 {Obs.decrypt_expanded(Key.words_60(), changed_ciphertext_aad(), changed_ciphertext_envelope()) == Fail{AES.AuthenticationFailed{}} : Result<&2, &2, AES.Error, List<&2, U32>>}: 110 Obs.finish_auth(Key.words_60(), changed_ciphertext_aad(), changed_ciphertext_envelope(), 111 changed_ciphertext_computed_tag(), False{}, Fail{AES.AuthenticationFailed{}}, 112 checkpoint_changed_ciphertext_tag(), {==}, {==}) 113 114 def rejects_changed_ciphertext() -> 115 {AES.decrypt(L.aes256gcm_nist_key(), changed_ciphertext_aad(), changed_ciphertext_envelope()) == Fail{AES.AuthenticationFailed{}} : Result<&2, &2, AES.Error, List<&2, U32>>}: 116 Obs.finish_decrypt(L.aes256gcm_nist_key(), changed_ciphertext_aad(), changed_ciphertext_envelope(), 117 Key.words_60(), Fail{AES.AuthenticationFailed{}}, {==}, {==}, V.checkpoint_nist_schedule(), checkpoint_changed_ciphertext_rejected())