-
Notifications
You must be signed in to change notification settings - Fork 7
/
Copy pathGOST.cry
136 lines (103 loc) · 5.36 KB
/
GOST.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
// Cryptol GOST Implementation
// Copyright (c) 2018, Galois Inc.
// www.cryptol.net
// Author: Ajay Kumar Eeralla
// Block size: 64 bits, key size: 256 bits
module Primitive::Symmetric::Cipher::Block::GOST where
type BlockSize = 64
type StdBlockSize = 32
type KeySize = 256
//S-box used by Central Bank of Russian Federation
sbox = [
[0x4, 0xa, 0x9, 0x2, 0xd, 0x8, 0x0, 0xe, 0x6, 0xb, 0x1, 0xc, 0x7, 0xf, 0x5, 0x3],
[0xe, 0xb, 0x4, 0xc, 0x6, 0xd, 0xf, 0xa, 0x2, 0x3, 0x8, 0x1, 0x0, 0x7, 0x5, 0x9],
[0x5, 0x8, 0x1, 0xd, 0xa, 0x3, 0x4, 0x2, 0xe, 0xf, 0xc, 0x7, 0x6, 0x0, 0x9, 0xb],
[0x7, 0xd, 0xa, 0x1, 0x0, 0x8, 0x9, 0xf, 0xe, 0x4, 0x6, 0xc, 0xb, 0x2, 0x5, 0x3],
[0x6, 0xc, 0x7, 0x1, 0x5, 0xf, 0xd, 0x8, 0x4, 0xa, 0x9, 0xe, 0x0, 0x3, 0xb, 0x2],
[0x4, 0xb, 0xa, 0x0, 0x7, 0x2, 0x1, 0xd, 0x3, 0x6, 0x8, 0x5, 0x9, 0xc, 0xf, 0xe],
[0xd, 0xb, 0x4, 0x1, 0x3, 0xf, 0x5, 0x9, 0x0, 0xa, 0xe, 0x7, 0x6, 0x8, 0x2, 0xc],
[0x1, 0xf, 0xd, 0x0, 0x5, 0x7, 0xa, 0x4, 0x9, 0x2, 0x3, 0xe, 0x6, 0xb, 0x8, 0xc]
]
//Most recent S-box: GOST R 34.12-2015
sbox_rec = [
[0xc, 0x4, 0x6, 0x2, 0xa, 0x5, 0xb, 0x9, 0xe, 0x8, 0xd, 0x7, 0x0, 0x3, 0xf, 0x1],
[0x6, 0x8, 0x2, 0x3, 0x9, 0xa, 0x5, 0xc, 0x1, 0xe, 0x4, 0x7, 0xb, 0xd, 0x0, 0xf],
[0xb, 0x3, 0x5, 0x8, 0x2, 0xf, 0xa, 0xd, 0xe, 0x1, 0x7, 0x4, 0xc, 0x9, 0x6, 0x0],
[0xc, 0x8, 0x2, 0x1, 0xd, 0x4, 0xf, 0x6, 0x7, 0x0, 0xa, 0x5, 0x3, 0xe, 0x9, 0xb],
[0x7, 0xf, 0x5, 0xa, 0x8, 0x1, 0x6, 0xd, 0x0, 0x9, 0x3, 0xe, 0xb, 0x4, 0x2, 0xc],
[0x5, 0xd, 0xf, 0x6, 0x9, 0x2, 0xc, 0xa, 0xb, 0x7, 0x8, 0x1, 0x4, 0x3, 0xe, 0x0],
[0x8, 0xe, 0x2, 0x5, 0x6, 0x9, 0x1, 0xc, 0xf, 0x4, 0xb, 0x0, 0xd, 0xa, 0x3, 0x7],
[0x1, 0x7, 0xe, 0xd, 0x0, 0x5, 0x8, 0x3, 0x4, 0xf, 0xa, 0x6, 0x9, 0xc, 0xb, 0x2]
]
// Split the plain text two blocks of 32bits each
splitPt: [BlockSize] -> [2][StdBlockSize]
splitPt pt = split pt:[2][StdBlockSize]
// Key schedule: split the key into 8 blocks each with 32bit subkey
keySchedule : [KeySize] -> [8][StdBlockSize]
keySchedule key = split key : [8][StdBlockSize]
//Round key for encryption
roundKey:[KeySize] -> _
roundKey key = [ rk@0, rk@1, rk@2, rk@3, rk@4, rk@5, rk@6, rk@7,
rk@0, rk@1, rk@2, rk@3, rk@4, rk@5, rk@6, rk@7,
rk@0, rk@1, rk@2, rk@3, rk@4, rk@5, rk@6, rk@7,
rk@7, rk@6, rk@5, rk@4, rk@3, rk@2, rk@1, rk@0
]
where rk = (keySchedule key)
//Round key for decryption
roundKey':[KeySize] -> _
roundKey' key = [ rk@0, rk@1, rk@2, rk@3, rk@4, rk@5, rk@6, rk@7,
rk@7, rk@6, rk@5, rk@4, rk@3, rk@2, rk@1, rk@0,
rk@7, rk@6, rk@5, rk@4, rk@3, rk@2, rk@1, rk@0,
rk@7, rk@6, rk@5, rk@4, rk@3, rk@2, rk@1, rk@0
]
where rk = (keySchedule key)
//Round function
roundFun : [StdBlockSize]-> [StdBlockSize] -> [StdBlockSize]
roundFun subpt subkey = roundRes
where res = subpt + subkey
splitRes = split res: [8][4]
subSboxRes = [ (sbox@i)@(splitRes@i) | i<- [0..7] ]
roundRes = (join subSboxRes) <<< 11
//One round encryption
roundEncryption: [StdBlockSize] -> [StdBlockSize] -> [StdBlockSize] -> [BlockSize]
roundEncryption lpt rpt rkey = rpt # (lpt ^ (roundFun rpt rkey))
//Encryption
gostEncrypt: ([KeySize], [BlockSize]) -> [BlockSize]
gostEncrypt (key, pt) = hs'
where hs = [(roundEncryption left right (round_key@0))] # [ (roundEncryption ((splitPt pT)@0) ((splitPt pT)@1) (round_key@i))
| i <- [1,2..31]
| pT <- hs
]
splt_pt = (splitPt pt)
left = splt_pt@0
right = splt_pt@1
round_key = (roundKey key)
hs' = hs!0
//One round decryption
roundDecryption: [StdBlockSize] -> [StdBlockSize] -> [StdBlockSize] -> [BlockSize]
roundDecryption lpt rpt rkey = (rpt ^ (roundFun lpt rkey)) # lpt
// Decryption
gostDecrypt: ([KeySize], [BlockSize]) -> [BlockSize]
gostDecrypt (key, ct) = hs'
where hs = [(roundDecryption left right (round_key@0))] # [ (roundDecryption ((splitPt pT)@0) ((splitPt pT)@1) (round_key@i))
| i <- [1,2..31]
| pT <- hs
]
splt_pt = (splitPt ct)
left = splt_pt@0
right = splt_pt@1
round_key = (roundKey' key)
hs' = hs!0
// Correctness
property gostCorrect key m = gostDecrypt(key, gostEncrypt(key, m)) == m
// Helper functions to perform analysis
gostEncrypt64: ([BlockSize],[BlockSize]) -> [BlockSize]
gostEncrypt64 (pt, key) = gostEncrypt(key', pt)
where key' = key # zero
gostDecrypt64 : ([BlockSize], [BlockSize]) -> [BlockSize]
gostDecrypt64 (ct, key) = gostDecrypt(key', ct)
where key' = key #zero
property gostCorrect64 key m = gostDecrypt64( key, gostEncrypt64(key, m)) == m
// To analyze the schemes from 5 through 20, we take |mi| = k where k > n (block size)
gostEncrypt256 : ([KeySize], [KeySize]) -> [KeySize]
gostEncrypt256 (pt, key) = gostEncrypt(key, (take`{64} pt))# zero