-
Notifications
You must be signed in to change notification settings - Fork 1
/
norx.cry
233 lines (190 loc) · 7.99 KB
/
norx.cry
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
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
/*
* NORX 3.0 Cryptol implementation by Tim Taubert <[email protected]>.
*
* The specification can be found at <https://norx.io/data/norx.pdf>.
*
* To the extent possible under law, the author(s) have dedicated all copyright
* and related and neighboring rights to this software to the public domain
* worldwide. This software is distributed without any warranty.
*
* You should have received a copy of the CC0 Public Domain Dedication along with
* this software. If not, see <http://creativecommons.org/publicdomain/zero/1.0/>.
*/
module NORX where
/* -------------------------------------------------------------------------- */
/* -- Configuration --------------------------------------------------------- */
// Pick a word size.
import NORX32Impl as NORXImpl
//import NORX64Impl as NORXImpl
/* -------------------------------------------------------------------------- */
/* -- Public API ------------------------------------------------------------ */
// 4-round NORX with p=1.
NORX4_Encrypt = NORX encrypt 4
NORX4_Decrypt = NORX decrypt 4
// 6-round NORX with p=1.
NORX6_Encrypt = NORX encrypt 6
NORX6_Decrypt = NORX decrypt 6
private
NORX f l k n a m z = (ct, tag)
where (st, ct) = f l (absorb l (initialise l k n) a DomHeader) m
(_, tag) = finalise l k (absorb l st z DomTrailer)
/* -------------------------------------------------------------------------- */
/* -- Implementation -------------------------------------------------------- */
// Initialise the internal state.
initialise : [Nw] -> Key -> Nonce -> State
initialise l k n = F l (ns # ks # [u8, u9, u10, u11] # ps) ^ (zero # ks)
where [u0, u1, u2, u3, u4, u5, u6, u7,
u8, u9, u10, u11, u12, u13, u14, u15] = F 2 [0..15]
ps = [u12 ^ `Nw, u13 ^ l, u14 ^ `Np, u15 ^ (`Nw * 4)]
ns = to_le n
ks = to_le k
// Absorb additional data.
absorb l s x v = state
where (state, block) = (absorb_data l s x v f) ! 0
f st bl = st ^ (bl # zero)
// Encrypt message.
encrypt : {n} (fin n) => [Nw] -> State -> [n][8] -> (State, [n][8])
encrypt l s x = ((abs ! 0).0, take ciphertext)
where ciphertext = from_le (join [ y.1 | y <- abs ])
abs = absorb_data l s x DomPayload f
f st bl = st ^ (bl # zero)
// Decrypt message.
decrypt : {n} (fin n) => [Nw] -> State -> [n][8] -> (State, [n][8])
decrypt l s x = (state', take plaintext)
where plaintext = from_le (join [ y.1 | y <- abs ])
abs = absorb_data l s x DomPayload f
f st bl = bl # (drop st)
// Fix the state returned by decrypt() so that the padding
// (if any) is properly XOR'ed with the last state Sj.
state' = (to_le mask ^ block) # (drop state)
mask = (take`{n % Nrb} sj # zero) : [Nrb][8]
sj = from_le (take state ^ block)
(state, block) = abs ! 0
// Finalise.
finalise : [Nw] -> Key -> State -> (State, Tag)
finalise l k s = (st, from_le (drop st))
where st = F l (F l (tag_state s DomTag) ^ ks) ^ ks
ks = zero # to_le k
private
type Nw = NORXImpl::Nw
type Nr = Nw * 12
type Nrb = Nr / 8
type Np = 1
type State = [16][Nw]
type Key = [Nw / 2][8]
type Nonce = [Nw / 2][8]
type Tag = [Nw / 2][8]
type Block = [Nr / Nw][Nw]
DomHeader = 1
DomPayload = 2
DomTrailer = 4
DomTag = 8
// Convert bytes to LE integers.
to_le : {n} (fin n, (n * 8) % Nw == 0) => [n][8] -> [n * 8 / Nw][Nw]
to_le x = [ join (reverse y) | y <- groupBy`{Nw / 8} x ]
// Convert LE integers to bytes.
from_le : {n} (fin n) => [n][Nw] -> [n * Nw / 8][8]
from_le x = join [ reverse (groupBy`{8} y) | y <- x ]
// Tag a given state.
tag_state : State -> [Nw] -> State
tag_state s v = zero # [v] ^ s
// l-round permutation.
F : [Nw] -> State -> State
F l s = xs @ l where xs = [s] # [ round x | x <- xs ]
// Inspired by the core of the ChaCha20 algorithm.
round [s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15] =
[u0, u1, u2, u3, u4, u5, u6, u7, u8, u9, u10, u11, u12, u13, u14, u15]
where
// Column step.
[t0, t4, t8, t12] = G [s0, s4, s8, s12]
[t1, t5, t9, t13] = G [s1, s5, s9, s13]
[t2, t6, t10, t14] = G [s2, s6, s10, s14]
[t3, t7, t11, t15] = G [s3, s7, s11, s15]
// Diagonal step.
[u0, u5, u10, u15] = G [t0, t5, t10, t15]
[u1, u6, u11, u12] = G [t1, t6, t11, t12]
[u2, u7, u8, u13] = G [t2, t7, t8, t13]
[u3, u4, u9, u14] = G [t3, t4, t9, t14]
// Inspired by ChaCha20's quarter round.
G [a, b, c, d] = [a'', b'', c'', d'']
where H x y = (x ^ y) ^ ((x && y) << 1)
a' = H a b
d' = (a' ^ d) >>> NORXImpl::rot.0
c' = H c d'
b' = (b ^ c') >>> NORXImpl::rot.1
a'' = H a' b'
d'' = (a'' ^ d') >>> NORXImpl::rot.2
c'' = H c' d''
b'' = (b' ^ c'') >>> NORXImpl::rot.3
// Multi-rate padding.
pad : {n, np}
( np == Nr - (n * 8) % Nr // number of padding bits
) => [n][8] -> [np / 8][8]
pad x = groupBy`{8} (postfix : [np])
where postfix = 0x01 # zero ^ (zero # 0x80)
// Base absorption function.
absorb_data : {n, num}
( // number of states + blocks returned
num == n / Nrb + 1
) => [Nw] -> State -> [n][8] -> [Nw] -> (State -> Block -> State)
-> [num](State, Block)
absorb_data l s x v f = drop`{1} ys
where blocks = groupBy (x # (pad x))
ys = [(s, zero)] # [ next y (to_le b) | b <- blocks | (y,_) <- ys ]
next y b = (f st b, take st ^ b)
where st = F l (tag_state y v)
/* -------------------------------------------------------------------------- */
/* -- Tests ----------------------------------------------------------------- */
private
tests = NORXImpl::tests
// Test Vectors [A.1]
property p_a1 = F 2 [0..15] == tests.vec_init_const
// Test Vectors [A.2]
K = [0..Nw/2-1]
N = [ 32 + x | x <- K ]
A = [0..127]
M = [0..127]
Z = [0..127]
// Test Values (4 rounds).
t_init = initialise 4 K N
t_header = absorb 4 t_init A DomHeader
(t_encrypt, t_ciphertext) = encrypt 4 t_header M
t_trailer = absorb 4 t_encrypt Z DomTrailer
(t_final, t_tag) = finalise 4 K t_trailer
t_decrypt = decrypt 4 t_header t_ciphertext
// Test Values (6 rounds).
t_init' = initialise 6 K N
t_header' = absorb 6 t_init' A DomHeader
(t_encrypt', t_ciphertext') = encrypt 6 t_header' M
t_trailer' = absorb 6 t_encrypt' Z DomTrailer
(t_final', t_tag') = finalise 6 K t_trailer'
t_decrypt' = decrypt 6 t_header' t_ciphertext'
// State after initialisation.
property p_a2_1_4 = t_init == tests.vec_init4
property p_a2_1_6 = t_init' == tests.vec_init6
// State after header processing.
property p_a2_2_4 = t_header == tests.vec_header4
property p_a2_2_6 = t_header' == tests.vec_header6
// State after message encryption.
property p_a2_3_4 = t_encrypt == tests.vec_encryption4
property p_a2_3_6 = t_encrypt' == tests.vec_encryption6
// State after trailer processing.
property p_a2_4_4 = t_trailer == tests.vec_trailer4
property p_a2_4_6 = t_trailer' == tests.vec_trailer6
// State after finalisation.
property p_a2_5_4 = t_final == tests.vec_final4
property p_a2_5_6 = t_final' == tests.vec_final6
// Ciphertext.
property p_a2_6_4 = t_ciphertext == tests.vec_ciphertext4
property p_a2_6_6 = t_ciphertext' == tests.vec_ciphertext6
// Authentication tag.
property p_a2_7_4 = t_tag == tests.vec_tag4
property p_a2_7_6 = t_tag' == tests.vec_tag6
// Decryption.
property p_a2_8_4 = (t_encrypt, M) == t_decrypt
property p_a2_8_6 = (t_encrypt', M) == t_decrypt'
// Public API.
property p_a2_9_4 = NORX4_Encrypt K N A M Z == (tests.vec_ciphertext4, tests.vec_tag4)
property p_a2_9_6 = NORX6_Encrypt K N A M Z == (tests.vec_ciphertext6, tests.vec_tag6)
property p_a2_10_4 = NORX4_Decrypt K N A tests.vec_ciphertext4 Z == (M, tests.vec_tag4)
property p_a2_10_6 = NORX6_Decrypt K N A tests.vec_ciphertext6 Z == (M, tests.vec_tag6)