proof/AES_NistTamperVectorProof.bend
qasim-bend-kit@0.1.0.2 · 117 lines · 27 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_NistVectorProof.bend as V
8
9def 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
12def 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
15def checkpoint_zero_key() ->
16 {Core.aes256_expand(AES.secret_key_bytes(zero_key())) == zero_words() : List<&2, U32>}:
17 {==}
18
19def changed_aad_aad() -> List<&2, U32>:
20 [1]
21
22def 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
25def 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
29def 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
33def 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
39def 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
44def changed_key_aad() -> List<&2, U32>:
45 []
46
47def 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
50def 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
54def 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
58def 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
64def 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
69def changed_nonce_aad() -> List<&2, U32>:
70 []
71
72def 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
75def 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
79def 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
83def 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
89def 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
94def changed_ciphertext_aad() -> List<&2, U32>:
95 []
96
97def 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
100def 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
104def 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
108def 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
114def 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())