-
Notifications
You must be signed in to change notification settings - Fork 86
/
KES.hs
214 lines (186 loc) · 8.01 KB
/
KES.hs
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
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DeriveAnyClass #-}
module Test.Crypto.KES
( tests
) where
import Data.Proxy (Proxy (..))
import GHC.Generics (Generic)
import Numeric.Natural (Natural)
import Test.QuickCheck
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)
import Ouroboros.Consensus.Crypto.DSIGN
import Ouroboros.Consensus.Crypto.KES
import Ouroboros.Consensus.Util.Random
import Ouroboros.Network.Serialise (Serialise, prop_serialise)
--
-- The list of all tests
--
tests :: TestTree
tests =
testGroup "Crypto.KES"
[ testKESAlgorithm (Proxy :: Proxy MockKES) "MockKES"
, testKESAlgorithm (Proxy :: Proxy (SimpleKES Ed448DSIGN)) "SimpleKES (with Ed448)"
]
testKESAlgorithm :: KESAlgorithm v => proxy v -> String -> TestTree
testKESAlgorithm p n =
testGroup n
[ testProperty "serialise VerKey" $ prop_KES_serialise_VerKey p
, testProperty "serialise SignKey" $ prop_KES_serialise_SignKey p
, testProperty "serialise Sig" $ prop_KES_serialise_Sig p
, testProperty "verify positive" $ prop_KES_verify_pos p
, testProperty "verify negative (wrong key)" $ prop_KES_verify_neg_key p
, testProperty "verify negative (wrong message)" $ prop_KES_verify_neg_msg p
, testProperty "verify negative (wrong time)" $ prop_KES_verify_neg_time p
]
prop_KES_serialise_VerKey :: KESAlgorithm v
=> proxy v
-> Duration_Seed_SK v
-> Property
prop_KES_serialise_VerKey _ (Duration_Seed_SK _ _ sk _) =
prop_serialise (deriveVerKeyKES sk)
prop_KES_serialise_SignKey :: KESAlgorithm v
=> proxy v
-> Duration_Seed_SK v
-> Property
prop_KES_serialise_SignKey _ (Duration_Seed_SK _ _ sk _) =
prop_serialise sk
prop_KES_serialise_Sig :: KESAlgorithm v
=> proxy v
-> Duration_Seed_SK_Times v String
-> Seed
-> Property
prop_KES_serialise_Sig _ d seed = case withSeed seed $ trySign d of
Left e -> counterexample e False
Right xs -> conjoin [prop_serialise sig |(_, _, sig) <- xs]
prop_KES_verify_pos :: KESAlgorithm v
=> proxy v
-> Duration_Seed_SK_Times v String
-> Seed
-> Property
prop_KES_verify_pos _ d seed =
let vk = getFirstVerKey d
in case withSeed seed $ trySign d of
Left e -> counterexample e False
Right xs -> conjoin [verifyKES vk j a sig | (j, a, sig) <- xs]
prop_KES_verify_neg_key :: KESAlgorithm v
=> proxy v
-> Duration_Seed_SK_Times v Int
-> Seed
-> Property
prop_KES_verify_neg_key _ d seed = getDuration d > 0 ==>
case withSeed seed $ trySign d of
Left e -> counterexample e False
Right xs -> conjoin [ not $ verifyKES (getSecondVerKey d) j a sig
| (j, a, sig) <- xs]
prop_KES_verify_neg_msg :: KESAlgorithm v
=> proxy v
-> Duration_Seed_SK_Times v Double
-> Double
-> Seed
-> Property
prop_KES_verify_neg_msg _ d a seed =
let vk = getFirstVerKey d
in case withSeed seed $ trySign d of
Left e -> counterexample e False
Right xs -> conjoin [a /= a' ==> not $ verifyKES vk j a sig | (j, a', sig) <- xs]
prop_KES_verify_neg_time :: KESAlgorithm v
=> proxy v
-> Duration_Seed_SK_Times v Double
-> Integer
-> Property
prop_KES_verify_neg_time _ d i =
let seed = Seed (1, 0, 2, 0, 1)
vk = getFirstVerKey d
t = fromIntegral $ abs i
in case withSeed seed $ trySign d of
Left e -> counterexample e False
Right xs -> conjoin [t /= j ==> not $ verifyKES vk t a sig | (j, a, sig) <- xs]
getDuration :: KESAlgorithm v => Duration_Seed_SK_Times v a -> Natural
getDuration d = case d of
(Duration_Seed_SK_Times duration _ _ _ _) -> duration
getFirstVerKey :: KESAlgorithm v => Duration_Seed_SK_Times v a -> VerKeyKES v
getFirstVerKey d = case d of
(Duration_Seed_SK_Times _ _ sk _ _) -> deriveVerKeyKES sk
getSecondVerKey :: KESAlgorithm v => Duration_Seed_SK_Times v a -> VerKeyKES v
getSecondVerKey d = case d of
(Duration_Seed_SK_Times _ _ _ vk _) -> vk
trySign :: forall m v a.
( MonadRandom m
, KESAlgorithm v
, Serialise a
, Show a)
=> Duration_Seed_SK_Times v a
-> m (Either String [(Natural, a, SigKES v)])
trySign (Duration_Seed_SK_Times _ _ sk _ ts) =
go sk ts
where
go :: SignKeyKES v
-> [(Natural, a)]
-> m (Either String [(Natural, a, SigKES v)])
go _ [] = return $ Right []
go sk' ((j, a) : xs) = do
m <- signKES j a sk'
case m of
Nothing -> return $ Left $
"trySign: error signing " ++
show a ++ " at " ++ show j ++ " with " ++ show sk
Just (sig, sk'') -> do
e <- go sk'' xs
return $ case e of
Right ys -> Right ((j, a, sig) : ys)
Left _ -> e
data Duration_Seed_SK v = Duration_Seed_SK Natural Seed (SignKeyKES v) (VerKeyKES v)
deriving Generic
deriving instance KESAlgorithm v => Show (Duration_Seed_SK v)
deriving instance KESAlgorithm v => Eq (Duration_Seed_SK v)
deriving instance KESAlgorithm v => Serialise (Duration_Seed_SK v)
instance KESAlgorithm v => Arbitrary (Duration_Seed_SK v) where
arbitrary = do
duration <- genNat
seed <- arbitrary
return $ duration_Seed_SK duration seed
shrink (Duration_Seed_SK duration seed _ _) =
[duration_Seed_SK d seed | d <- shrinkNat duration]
data Duration_Seed_SK_Times v a =
Duration_Seed_SK_Times Natural Seed (SignKeyKES v) (VerKeyKES v) [(Natural, a)]
deriving Generic
instance (KESAlgorithm v, Arbitrary a) => Arbitrary (Duration_Seed_SK_Times v a) where
arbitrary = arbitrary >>= gen_Duration_Seed_SK_Times
shrink (Duration_Seed_SK_Times d s sk vk ts) = do
Duration_Seed_SK d' s' sk' vk' <- shrink $ Duration_Seed_SK d s sk vk
let ts' = filter ((< d') . fst) ts
return $ Duration_Seed_SK_Times d' s' sk' vk' ts'
deriving instance (KESAlgorithm v, Show a) => Show (Duration_Seed_SK_Times v a)
deriving instance (KESAlgorithm v, Eq a) => Eq (Duration_Seed_SK_Times v a)
deriving instance (KESAlgorithm v, Serialise a) => Serialise (Duration_Seed_SK_Times v a)
duration_Seed_SK :: KESAlgorithm v => Natural -> Seed -> Duration_Seed_SK v
duration_Seed_SK duration seed =
let (sk, vk) = withSeed seed go
in Duration_Seed_SK duration seed sk vk
where
go = do
sk <- genKeyKES duration
sk' <- genKeyKES duration
let vk = deriveVerKeyKES sk'
if duration > 0 && deriveVerKeyKES sk == vk
then go
else return (sk, vk)
gen_Duration_Seed_SK_Times :: Arbitrary a
=> Duration_Seed_SK v
-> Gen (Duration_Seed_SK_Times v a)
gen_Duration_Seed_SK_Times (Duration_Seed_SK duration seed sk vk) = do
ts <- genTimes 0
return $ Duration_Seed_SK_Times duration seed sk vk ts
where
genTimes :: Arbitrary a => Natural -> Gen [(Natural, a)]
genTimes j
| j >= duration = return []
| otherwise = do
k <- genNatBetween j (duration - 1)
a <- arbitrary
ns <- genTimes $ k + 1
return ((k, a) : ns)