proof/AES_NistCtr4BlockProof.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 [202, 254, 186, 190, 250, 206, 219, 173, 222, 202, 248, 136, 0, 0, 0, 4]
9
10def state_0() -> List<&2, U32>:
11 [52, 1, 83, 44, 124, 171, 168, 177, 179, 160, 119, 28, 103, 48, 131, 12]
12
13def state_1() -> List<&2, U32>:
14 [99, 217, 123, 202, 0, 240, 211, 194, 158, 235, 100, 65, 172, 140, 90, 1]
15
16def state_2() -> List<&2, U32>:
17 [166, 82, 172, 54, 81, 113, 219, 17, 174, 153, 103, 141, 244, 254, 80, 113]
18
19def state_3() -> List<&2, U32>:
20 [155, 192, 165, 13, 75, 13, 40, 217, 246, 34, 202, 144, 6, 131, 131, 67]
21
22def state_4() -> List<&2, U32>:
23 [21, 3, 100, 171, 164, 36, 74, 15, 196, 240, 19, 210, 116, 94, 85, 252]
24
25def state_5() -> List<&2, U32>:
26 [223, 38, 193, 186, 244, 248, 161, 8, 114, 81, 72, 38, 193, 79, 56, 30]
27
28def state_6() -> List<&2, U32>:
29 [231, 134, 36, 132, 145, 183, 101, 62, 108, 233, 136, 9, 47, 76, 77, 238]
30
31def state_7() -> List<&2, U32>:
32 [104, 86, 0, 74, 167, 231, 84, 108, 232, 159, 63, 210, 13, 193, 141, 25]
33
34def state_8() -> List<&2, U32>:
35 [217, 77, 77, 11, 127, 252, 79, 130, 159, 160, 42, 15, 249, 37, 185, 214]
36
37def state_9() -> List<&2, U32>:
38 [103, 32, 186, 13, 12, 79, 251, 202, 94, 106, 243, 137, 0, 205, 73, 19]
39
40def state_10() -> List<&2, U32>:
41 [246, 120, 185, 168, 55, 216, 222, 141, 223, 204, 67, 83, 142, 120, 170, 6]
42
43def state_11() -> List<&2, U32>:
44 [20, 12, 6, 188, 47, 123, 119, 85, 2, 226, 46, 116, 9, 96, 78, 254]
45
46def state_12() -> List<&2, U32>:
47 [86, 128, 159, 221, 185, 66, 186, 239, 79, 111, 105, 114, 7, 70, 62, 206]
48
49def state_13() -> List<&2, U32>:
50 [24, 186, 12, 86, 232, 131, 159, 167, 220, 179, 8, 240, 88, 249, 199, 27]
51
52def result() -> List<&2, U32>:
53 [144, 140, 130, 221, 204, 101, 178, 110, 136, 127, 133, 52, 31, 36, 61, 29]
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 {==}