-
Notifications
You must be signed in to change notification settings - Fork 1
/
norx3241.saw
119 lines (97 loc) · 4.1 KB
/
norx3241.saw
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
import "norx.cry";
m <- llvm_load_module "norx3241.bc";
print "NORX32-4-1: verify norx_init";
time (llvm_verify m "norx_init" [] do {
llvm_ptr "state" (llvm_array 16 (llvm_int 32));
state <- llvm_var "*state" (llvm_array 16 (llvm_int 32));
llvm_ptr "k" (llvm_array 16 (llvm_int 8));
k <- llvm_var "*k" (llvm_array 16 (llvm_int 8));
llvm_ptr "n" (llvm_array 16 (llvm_int 8));
n <- llvm_var "*n" (llvm_array 16 (llvm_int 8));
// Check resulting state.
llvm_ensure_eq "*state" {{ initialise 4 k n : [16][32] }};
// Verify.
llvm_verify_tactic abc;
});
let check_absorb_data bytes = do {
llvm_ptr "state" (llvm_array 16 (llvm_int 32));
state <- llvm_var "*state" (llvm_array 16 (llvm_int 32));
llvm_ptr "in" (llvm_array bytes (llvm_int 8));
inp <- llvm_var "*in" (llvm_array bytes (llvm_int 8));
inlen <- llvm_var "inlen" (llvm_int 64);
tag <- llvm_var "tag" (llvm_int 32);
// Input is ${bytes} long.
llvm_assert_eq "inlen" {{ `bytes : [64] }};
// Check resulting state.
llvm_ensure_eq "*state" {{ absorb 4 state inp tag : [16][32] }};
// Verify.
llvm_sat_branches true;
llvm_verify_tactic abc;
};
print "NORX32-4-1: verify norx_absorb_data";
time (llvm_verify m "norx_absorb_data" [] (check_absorb_data 32));
time (llvm_verify m "norx_absorb_data" [] (check_absorb_data 48));
time (llvm_verify m "norx_absorb_data" [] (check_absorb_data 49));
time (llvm_verify m "norx_absorb_data" [] (check_absorb_data 96));
let check_encrypt_data bytes = do {
llvm_ptr "state" (llvm_array 16 (llvm_int 32));
state <- llvm_var "*state" (llvm_array 16 (llvm_int 32));
llvm_ptr "out" (llvm_array bytes (llvm_int 8));
out <- llvm_var "*out" (llvm_array bytes (llvm_int 8));
llvm_ptr "in" (llvm_array bytes (llvm_int 8));
inp <- llvm_var "*in" (llvm_array bytes (llvm_int 8));
inlen <- llvm_var "inlen" (llvm_int 64);
// Input is ${bytes} long.
llvm_assert_eq "inlen" {{ `bytes : [64] }};
// Check resulting state and ciphertext.
let res = {{ encrypt 4 state inp }};
llvm_ensure_eq "*state" {{ res.0 : [16][32] }};
llvm_ensure_eq "*out" {{ res.1 : [_][8] }};
// Verify.
llvm_sat_branches true;
llvm_verify_tactic abc;
};
print "NORX32-4-1: verify norx_encrypt_data";
time (llvm_verify m "norx_encrypt_data" [] (check_encrypt_data 32));
time (llvm_verify m "norx_encrypt_data" [] (check_encrypt_data 48));
time (llvm_verify m "norx_encrypt_data" [] (check_encrypt_data 49));
time (llvm_verify m "norx_encrypt_data" [] (check_encrypt_data 96));
let check_decrypt_data bytes = do {
llvm_ptr "state" (llvm_array 16 (llvm_int 32));
state <- llvm_var "*state" (llvm_array 16 (llvm_int 32));
llvm_ptr "out" (llvm_array bytes (llvm_int 8));
out <- llvm_var "*out" (llvm_array bytes (llvm_int 8));
llvm_ptr "in" (llvm_array bytes (llvm_int 8));
inp <- llvm_var "*in" (llvm_array bytes (llvm_int 8));
inlen <- llvm_var "inlen" (llvm_int 64);
// Input is ${bytes} long.
llvm_assert_eq "inlen" {{ `bytes : [64] }};
// Check resulting state and plaintext.
let res = {{ decrypt 4 state inp }};
llvm_ensure_eq "*state" {{ res.0 : [16][32] }};
llvm_ensure_eq "*out" {{ res.1 : [_][8] }};
// Verify.
llvm_sat_branches true;
llvm_verify_tactic abc;
};
print "NORX32-4-1: verify norx_decrypt_data";
time (llvm_verify m "norx_decrypt_data" [] (check_decrypt_data 32));
time (llvm_verify m "norx_decrypt_data" [] (check_decrypt_data 48));
time (llvm_verify m "norx_decrypt_data" [] (check_decrypt_data 49));
time (llvm_verify m "norx_decrypt_data" [] (check_decrypt_data 96));
print "NORX32-4-1: verify norx_finalise";
time (llvm_verify m "norx_finalise" [] do {
llvm_ptr "k" (llvm_array 16 (llvm_int 8));
k <- llvm_var "*k" (llvm_array 16 (llvm_int 8));
llvm_ptr "state" (llvm_array 16 (llvm_int 32));
state <- llvm_var "*state" (llvm_array 16 (llvm_int 32));
llvm_ptr "tag" (llvm_array 16 (llvm_int 8));
tag <- llvm_var "*tag" (llvm_array 16 (llvm_int 8));
// Check resulting state and tag.
let res = {{ finalise 4 k state }};
llvm_ensure_eq "*state" {{ res.0 : [16][32] }};
llvm_ensure_eq "*tag" {{ res.1 : [16][8] }};
// Verify.
llvm_sat_branches true;
llvm_verify_tactic abc;
});