proof/AES_NistHashBlockProof.bend
qasim-bend-kit@0.1.0.2 · 113 lines · 31 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
3import qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend as Key
4
5
6
7def block() -> List<&2, U32>:
8 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
9
10def state_0() -> List<&2, U32>:
11 [254, 255, 233, 146, 134, 101, 115, 28, 109, 106, 143, 148, 103, 48, 131, 8]
12
13def state_1() -> List<&2, U32>:
14 [7, 123, 169, 26, 171, 69, 39, 160, 155, 224, 52, 233, 225, 49, 115, 65]
15
16def state_2() -> List<&2, U32>:
17 [67, 161, 220, 40, 172, 229, 209, 156, 89, 19, 112, 108, 45, 199, 222, 85]
18
19def state_3() -> List<&2, U32>:
20 [226, 50, 179, 95, 26, 147, 52, 166, 100, 146, 82, 51, 20, 31, 212, 69]
21
22def state_4() -> List<&2, U32>:
23 [11, 113, 151, 179, 69, 121, 252, 116, 200, 5, 219, 180, 122, 53, 255, 176]
24
25def state_5() -> List<&2, U32>:
26 [51, 79, 89, 198, 109, 32, 191, 114, 231, 128, 200, 247, 124, 62, 44, 8]
27
28def state_6() -> List<&2, U32>:
29 [164, 187, 38, 171, 158, 214, 214, 74, 70, 239, 135, 11, 207, 19, 152, 58]
30
31def state_7() -> List<&2, U32>:
32 [83, 243, 220, 241, 104, 61, 9, 247, 165, 1, 84, 145, 80, 229, 175, 226]
33
34def state_8() -> List<&2, U32>:
35 [69, 43, 40, 150, 236, 171, 32, 196, 155, 104, 143, 135, 32, 149, 159, 180]
36
37def state_9() -> List<&2, U32>:
38 [81, 30, 137, 82, 246, 53, 149, 171, 60, 226, 141, 31, 56, 243, 176, 130]
39
40def state_10() -> List<&2, U32>:
41 [86, 150, 237, 202, 234, 227, 57, 161, 44, 231, 220, 82, 80, 133, 232, 132]
42
43def state_11() -> List<&2, U32>:
44 [213, 144, 246, 62, 238, 44, 26, 237, 214, 49, 93, 168, 11, 142, 26, 194]
45
46def state_12() -> List<&2, U32>:
47 [172, 192, 117, 199, 120, 154, 187, 207, 146, 185, 155, 71, 237, 226, 212, 217]
48
49def state_13() -> List<&2, U32>:
50 [172, 59, 160, 40, 195, 156, 109, 136, 31, 120, 114, 152, 4, 69, 39, 2]
51
52def result() -> List<&2, U32>:
53 [172, 190, 242, 5, 121, 180, 184, 235, 206, 136, 155, 172, 135, 50, 218, 215]
54
55def initial_matches() ->
56 {Core.aes_add_key(block(), Key.words_60(), 0n) == state_0() : List<&2, U32>}:
57 {==}
58
59def round_1_matches() ->
60 {Core.aes_middle_round(state_0(), Key.words_60(), 1n) == state_1() : List<&2, U32>}:
61 {==}
62
63def round_2_matches() ->
64 {Core.aes_middle_round(state_1(), Key.words_60(), 2n) == state_2() : List<&2, U32>}:
65 {==}
66
67def round_3_matches() ->
68 {Core.aes_middle_round(state_2(), Key.words_60(), 3n) == state_3() : List<&2, U32>}:
69 {==}
70
71def round_4_matches() ->
72 {Core.aes_middle_round(state_3(), Key.words_60(), 4n) == state_4() : List<&2, U32>}:
73 {==}
74
75def round_5_matches() ->
76 {Core.aes_middle_round(state_4(), Key.words_60(), 5n) == state_5() : List<&2, U32>}:
77 {==}
78
79def round_6_matches() ->
80 {Core.aes_middle_round(state_5(), Key.words_60(), 6n) == state_6() : List<&2, U32>}:
81 {==}
82
83def round_7_matches() ->
84 {Core.aes_middle_round(state_6(), Key.words_60(), 7n) == state_7() : List<&2, U32>}:
85 {==}
86
87def round_8_matches() ->
88 {Core.aes_middle_round(state_7(), Key.words_60(), 8n) == state_8() : List<&2, U32>}:
89 {==}
90
91def round_9_matches() ->
92 {Core.aes_middle_round(state_8(), Key.words_60(), 9n) == state_9() : List<&2, U32>}:
93 {==}
94
95def round_10_matches() ->
96 {Core.aes_middle_round(state_9(), Key.words_60(), 10n) == state_10() : List<&2, U32>}:
97 {==}
98
99def round_11_matches() ->
100 {Core.aes_middle_round(state_10(), Key.words_60(), 11n) == state_11() : List<&2, U32>}:
101 {==}
102
103def round_12_matches() ->
104 {Core.aes_middle_round(state_11(), Key.words_60(), 12n) == state_12() : List<&2, U32>}:
105 {==}
106
107def round_13_matches() ->
108 {Core.aes_middle_round(state_12(), Key.words_60(), 13n) == state_13() : List<&2, U32>}:
109 {==}
110
111def final_matches() ->
112 {Core.aes_final_round(state_13(), Key.words_60()) == result() : List<&2, U32>}:
113 {==}