-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathtiny-aes128.ads
More file actions
147 lines (118 loc) · 4.88 KB
/
tiny-aes128.ads
File metadata and controls
147 lines (118 loc) · 4.88 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
-- AES
-- an Ada implementation of the AES encryption algorithm
--
-- block size: 128 bits; length size: 128 bits
with Ada.Finalization;
generic
type T is mod <>;
type TIndex is range <>;
type TArray is array (TIndex range <>) of T;
package Tiny.AES128 with
Preelaborate,
Pure,
SPARK_Mode
is
-- The key, nonce and input are each 128 bits long.
subtype Block128 is TArray (1 .. 16);
type Round_Key_Array is private;
type Matrix_T is private;
-----------
-- ECB --
-----------
generic
Key : Block128;
package ECB with
SPARK_Mode
is
type Buffer is new Ada.Finalization.Limited_Controlled with private;
overriding
procedure Initialize (This : in out Buffer);
function Encrypt (This : Buffer; Data : Block128) return Block128;
private
type Buffer is new Ada.Finalization.Limited_Controlled with
record
Round_Keys : Round_Key_Array;
end record;
end ECB;
-----------
-- CTR --
-----------
generic
type Counter_T is mod <>;
with function "+" (Nonce : Block128; Value : Counter_T) return Block128;
Key, Nonce : Block128;
package CTR with
SPARK_Mode
is
package AES128_ECB is new ECB (Key);
type Buffer is tagged limited private;
function Xcrypt
(This : Buffer;
Data : Block128;
Counter : Counter_T)
return Block128;
private
type Buffer is
tagged limited record
Buffer : AES128_ECB.Buffer;
end record;
end CTR;
private
-- AES128 -> 10 rounds * (4 * 4) bytes = 128 bit
type Round_Key_Array is array (0 .. 10, 1 .. 4, 1 .. 4) of T;
type Matrix_T is array (1 .. 4, 1 .. 4) of T;
Sbox : constant TArray (TIndex'First .. TIndex'First + 255) :=
-- 0/8 1/9 2/a 3/b 4/c 5/d 6/e 7/f
[16#63#, 16#7c#, 16#77#, 16#7b#, 16#f2#, 16#6b#, 16#6f#, 16#c5#,
16#30#, 16#01#, 16#67#, 16#2b#, 16#fe#, 16#d7#, 16#ab#, 16#76#,
16#ca#, 16#82#, 16#c9#, 16#7d#, 16#fa#, 16#59#, 16#47#, 16#f0#,
16#ad#, 16#d4#, 16#a2#, 16#af#, 16#9c#, 16#a4#, 16#72#, 16#c0#,
16#b7#, 16#fd#, 16#93#, 16#26#, 16#36#, 16#3f#, 16#f7#, 16#cc#,
16#34#, 16#a5#, 16#e5#, 16#f1#, 16#71#, 16#d8#, 16#31#, 16#15#,
16#04#, 16#c7#, 16#23#, 16#c3#, 16#18#, 16#96#, 16#05#, 16#9a#,
16#07#, 16#12#, 16#80#, 16#e2#, 16#eb#, 16#27#, 16#b2#, 16#75#,
16#09#, 16#83#, 16#2c#, 16#1a#, 16#1b#, 16#6e#, 16#5a#, 16#a0#,
16#52#, 16#3b#, 16#d6#, 16#b3#, 16#29#, 16#e3#, 16#2f#, 16#84#,
16#53#, 16#d1#, 16#00#, 16#ed#, 16#20#, 16#fc#, 16#b1#, 16#5b#,
16#6a#, 16#cb#, 16#be#, 16#39#, 16#4a#, 16#4c#, 16#58#, 16#cf#,
16#d0#, 16#ef#, 16#aa#, 16#fb#, 16#43#, 16#4d#, 16#33#, 16#85#,
16#45#, 16#f9#, 16#02#, 16#7f#, 16#50#, 16#3c#, 16#9f#, 16#a8#,
16#51#, 16#a3#, 16#40#, 16#8f#, 16#92#, 16#9d#, 16#38#, 16#f5#,
16#bc#, 16#b6#, 16#da#, 16#21#, 16#10#, 16#ff#, 16#f3#, 16#d2#,
16#cd#, 16#0c#, 16#13#, 16#ec#, 16#5f#, 16#97#, 16#44#, 16#17#,
16#c4#, 16#a7#, 16#7e#, 16#3d#, 16#64#, 16#5d#, 16#19#, 16#73#,
16#60#, 16#81#, 16#4f#, 16#dc#, 16#22#, 16#2a#, 16#90#, 16#88#,
16#46#, 16#ee#, 16#b8#, 16#14#, 16#de#, 16#5e#, 16#0b#, 16#db#,
16#e0#, 16#32#, 16#3a#, 16#0a#, 16#49#, 16#06#, 16#24#, 16#5c#,
16#c2#, 16#d3#, 16#ac#, 16#62#, 16#91#, 16#95#, 16#e4#, 16#79#,
16#e7#, 16#c8#, 16#37#, 16#6d#, 16#8d#, 16#d5#, 16#4e#, 16#a9#,
16#6c#, 16#56#, 16#f4#, 16#ea#, 16#65#, 16#7a#, 16#ae#, 16#08#,
16#ba#, 16#78#, 16#25#, 16#2e#, 16#1c#, 16#a6#, 16#b4#, 16#c6#,
16#e8#, 16#dd#, 16#74#, 16#1f#, 16#4b#, 16#bd#, 16#8b#, 16#8a#,
16#70#, 16#3e#, 16#b5#, 16#66#, 16#48#, 16#03#, 16#f6#, 16#0e#,
16#61#, 16#35#, 16#57#, 16#b9#, 16#86#, 16#c1#, 16#1d#, 16#9e#,
16#e1#, 16#f8#, 16#98#, 16#11#, 16#69#, 16#d9#, 16#8e#, 16#94#,
16#9b#, 16#1e#, 16#87#, 16#e9#, 16#ce#, 16#55#, 16#28#, 16#df#,
16#8c#, 16#a1#, 16#89#, 16#0d#, 16#bf#, 16#e6#, 16#42#, 16#68#,
16#41#, 16#99#, 16#2d#, 16#0f#, 16#b0#, 16#54#, 16#bb#, 16#16#];
Rcon : constant TArray (1 .. 10) :=
-- 1/6 2/7 3/8 4/9 5/10
[16#01#, 16#02#, 16#04#, 16#08#, 16#10#,
16#20#, 16#40#, 16#80#, 16#1b#, 16#36#];
function Key_Expansion (Key : Block128) return Round_Key_Array;
function Cipher
(State : Matrix_T;
Round_Keys : Round_Key_Array)
return Matrix_T;
function Substitute (State : Matrix_T) return Matrix_T;
function Permute (State : Matrix_T) return Matrix_T;
function Multiplicate (State : Matrix_T) return Matrix_T;
function Add_Round_Key
(State : Matrix_T;
Round_Key : Matrix_T)
return Matrix_T;
function Shift_Left (Value : T; Amount : Natural) return T
with Import, Convention => Intrinsic;
function Shift_Right (Value : T; Amount : Natural) return T
with Import, Convention => Intrinsic;
end Tiny.AES128;