-
Notifications
You must be signed in to change notification settings - Fork 7
/
Copy pathtrivium.cry
95 lines (76 loc) · 3.22 KB
/
trivium.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
/* Source:
Alexander Semenov
Institute for System Dynamics and Control Theory
Russian Academy of Sciences
*/
module Primitive::Symmetric::Cipher::Stream::trivium where
Trivium_stream : [93] -> [84] -> [111] -> [inf]
Trivium_stream R1 R2 R3 = stream
where
(stream, ra, rb, rc) = shift_regs R1 R2 R3
type N = 300
Trivium : ([93], [84], [111]) -> [N]Bit
Trivium (reg1, reg2, reg3) = keystream
where
keystream = take`{N} (Trivium_stream reg1 reg2 reg3)
shift : {d} (fin d, d >=1) => [d] -> Bit -> [d]
shift fill bit = fills
where
fills = [bit]#(drop`{1} (fill >> 1))
shift_regs : {d,e,f} (fin d, fin e, fin f, d >=1, e >=1, f>=1) => [d] -> [e] -> [f] -> ([inf],[inf][d],[inf][e],[inf][f])
shift_regs r1 r2 r3 = (stream, regA, regB, regC)
where
s1 = [(f1 @ 65) ^ (f1 @ 92) | f1 <- regA]
s2 = [(f2 @ 68) ^ (f2 @ 83) | f2 <- regB]
s3 = [(f3 @ 65) ^ (f3 @ 110) | f3 <- regC]
stream = s1 ^ s2 ^ s3
t1 = [(f1 @ 65) ^ ((f1 @ 90) && (f1 @ 91)) ^ (f1 @ 92) ^ (f2 @ 77) |
f2 <- regB |
f1 <- regA ]
t2 = [(f2 @ 68) ^ ((f2 @ 81) && (f2 @ 82)) ^ (f2 @ 83) ^ (f3 @ 86) |
f2 <- regB |
f3 <- regC ]
t3 = [(f3 @ 65) ^ ((f3 @ 108) && (f3 @ 109)) ^ (f3 @ 110) ^ (f1 @ 68)|
f1 <- regA |
f3 <- regC ]
regA = [r1] # [shift f b| f <- regA | b <- t3]
regB = [r2] # [shift f b| f <- regB | b <- t1]
regC = [r3] # [shift f b| f <- regC | b <- t2]
Trivium_alt : ([93], [84], [111]) -> [N]Bit
Trivium_alt (r1, r2, r3) = take`{N} (s1 ^ s2 ^ s3)
where
a_65 = drop`{27} a_92
a_68 = drop`{24} a_92
a_90 = drop`{2} a_92
a_91 = drop`{1} a_92
a_92 = reverse r1 # t3
b_68 = drop`{15} b_83
b_77 = drop`{6} b_83
b_81 = drop`{2} b_83
b_82 = drop`{1} b_83
b_83 = reverse r2 # t1
c_65 = drop`{45} c_110
c_86 = drop`{24} c_110
c_108 = drop`{2} c_110
c_109 = drop`{1} c_110
c_110 = reverse r3 # t2
s1 = a_65 ^ a_92
s2 = b_68 ^ b_83
s3 = c_65 ^ c_110
t1 = s1 ^ (a_90 && a_91) ^ b_77
t2 = s2 ^ (b_81 && b_82) ^ c_86
t3 = s3 ^ (c_108 && c_109) ^ a_68
/*********************************************************/
iv1 = 0b111111111111111111101111111111111111111011111111111111111110111111111111111111101111111111111
iv2 = 0b000000000000000000001000000000000000000001000000000000000000001000000000000000000001
iv3 = 0b111111111111111110111111111111111111101111111111111111111011111111111111111110111111111111100000000000000000000
test_keystream = 0b011111110111101111110100001110000000000000100010000000000000000100011000101100001110001011011010101010000100101110001111100011000110000101001011001111011101110110111010011011010110001000111101101111101100101001000111010001010011111110011100100011101010011110101001001000011100001111111100000001110001
property Trivium_correct = (Trivium(iv1, iv2, iv3)) == test_keystream
property Trivium_search (x, y, z) = (Trivium(x, y, z)) == test_keystream
property Trivium_alt_correct = (Trivium_alt(iv1, iv2, iv3)) == test_keystream
property Trivium_alt_equivalent x = take`{200}(Trivium_alt x) == take (Trivium x)
cycle : {n} (fin n) => [n] -> ([93], [84], [111]) -> Bit
cycle n (rA, rB, rC) =
(rA == regAs @ n) /\ (rB == regBs @ n) /\ (rC == regCs @ n) /\ rA != 0 /\ rB != 0 /\ rC != 0
where
(_, regAs, regBs, regCs) = shift_regs rA rB rC