proof/AES_NistCtr2BlockProof.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, 2]
9
10def state_0() -> List<&2, U32>:
11 [52, 1, 83, 44, 124, 171, 168, 177, 179, 160, 119, 28, 103, 48, 131, 10]
12
13def state_1() -> List<&2, U32>:
14 [250, 64, 203, 227, 0, 240, 211, 194, 158, 235, 100, 65, 172, 140, 90, 1]
15
16def state_2() -> List<&2, U32>:
17 [17, 132, 122, 87, 52, 20, 116, 219, 144, 219, 27, 179, 176, 134, 108, 77]
18
19def state_3() -> List<&2, U32>:
20 [77, 234, 206, 15, 102, 49, 82, 113, 143, 165, 106, 197, 76, 40, 130, 191]
21
22def state_4() -> List<&2, U32>:
23 [180, 92, 89, 235, 69, 46, 66, 167, 206, 112, 90, 227, 77, 248, 23, 168]
24
25def state_5() -> List<&2, U32>:
26 [212, 208, 25, 253, 65, 225, 197, 189, 206, 93, 179, 65, 46, 237, 96, 21]
27
28def state_6() -> List<&2, U32>:
29 [148, 83, 72, 53, 34, 104, 138, 107, 111, 62, 15, 166, 207, 195, 44, 206]
30
31def state_7() -> List<&2, U32>:
32 [33, 77, 219, 136, 55, 210, 149, 237, 163, 8, 68, 35, 222, 103, 178, 115]
33
34def state_8() -> List<&2, U32>:
35 [228, 94, 229, 33, 182, 91, 128, 118, 101, 160, 230, 138, 25, 198, 155, 246]
36
37def state_9() -> List<&2, U32>:
38 [128, 124, 126, 120, 187, 195, 130, 128, 254, 148, 231, 207, 13, 62, 53, 38]
39
40def state_10() -> List<&2, U32>:
41 [144, 69, 247, 76, 185, 11, 22, 234, 173, 129, 113, 12, 62, 144, 246, 32]
42
43def state_11() -> List<&2, U32>:
44 [239, 178, 116, 130, 96, 251, 29, 126, 143, 210, 240, 36, 96, 137, 182, 182]
45
46def state_12() -> List<&2, U32>:
47 [38, 208, 241, 208, 72, 8, 10, 27, 44, 150, 234, 234, 11, 73, 115, 109]
48
49def state_13() -> List<&2, U32>:
50 [121, 241, 104, 139, 36, 1, 17, 215, 132, 122, 248, 15, 23, 31, 251, 137]
51
52def result() -> List<&2, U32>:
53 [139, 28, 243, 213, 97, 210, 123, 226, 81, 38, 62, 102, 133, 113, 100, 231]
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 {==}