0 | module Crypto.Curve.XCurves
 1 |
 2 | -- This doesn't implement the Point interface because I can't be bothered will implementing
 3 | -- point addition. This module is for DH strictly.
 4 |
 5 | import Data.Bits
 6 | import Data.Bool.Xor
 7 | import Data.Vect
 8 | import Utils.Bytes
 9 | import Utils.Misc
10 |
11 | data XCurvesParameter : (n : Nat) -> Type where
12 |   XCParam : {n : Nat} ->
13 |             (bits : Nat) ->
14 |             (u : Integer) ->
15 |             (a24 : Integer) ->
16 |             (scalar_decoder : Vect n Bits8 -> Integer) ->
17 |             (prime : Integer) ->
18 |             XCurvesParameter n
19 |
20 | cswap : Integer -> Integer -> Integer -> (Integer, Integer)
21 | cswap swap x2 x3 =
22 |   let dummy = (0 - swap) .&. (x2 `xor` x3)
23 |   in (x2 `xor` dummy, x3 `xor` dummy)
24 |
25 | mul_go : {n : Nat} -> XCurvesParameter n -> Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Nat ->
26 |          (Integer, Integer, Integer, Integer, Integer)
27 | mul_go param@(XCParam _ _ a24 _ prime) x1 x2 z2 x3 z3 swap k t =
28 |   let mul = (\a,b => mul_mod a b prime)
29 |       pow = (\a,b => pow_mod a b prime)
30 |       k_t = (shiftR k t) .&. 1
31 |       swap' = xor swap k_t
32 |       (x2, x3) = cswap swap' x2 x3
33 |       (z2, z3) = cswap swap' z2 z3
34 |       a = x2 + z2
35 |       aa = a `mul` a
36 |       b = x2 - z2
37 |       bb = b `mul` b
38 |       e = aa - bb
39 |       c = x3 + z3
40 |       d = x3 - z3
41 |       da = d `mul` a
42 |       cb = c `mul` b
43 |       x3 = pow (da + cb) 2
44 |       z3 = x1 `mul` (pow (da - cb) 2)
45 |       x2 = aa `mul` bb
46 |       z2 = e `mul` (aa + (a24 `mul` e))
47 |   in case t of
48 |        Z => (x2, x3, z2, z3, k_t)
49 |        S t' => mul_go param x1 x2 z2 x3 z3 k_t k t'
50 |
51 | public export
52 | mul : {n : Nat} -> XCurvesParameter n -> Vect n Bits8 -> Vect n Bits8 -> Maybe (Vect n Bits8)
53 | mul {n} param@(XCParam bits _ a24 decode prime) k u =
54 |   let u' = le_to_integer u
55 |       k' = decode k
56 |       (x2, x3, z2, z3, swap) = mul_go param u' 1 0 u' 1 0 k' (minus bits 1)
57 |       (x2', x3') = cswap swap x2 x3
58 |       (z2', z3') = cswap swap z2 z3
59 |       beta = pow_mod z2' (prime-2) prime
60 |       secret = mul_mod x2' beta prime
61 |   in guard (secret /= 0) *> (pure $ integer_to_le _ secret )
62 |
63 | generator : {n : Nat} -> XCurvesParameter n -> Vect n Bits8
64 | generator (XCParam _ u _ _ _) = integer_to_le _ u
65 |
66 | public export
67 | derive_public_key : {n : Nat} -> XCurvesParameter n -> Vect n Bits8 -> Maybe (Vect n Bits8)
68 | derive_public_key param k = mul param k $ generator param
69 |
70 | decode_scalar_25519 : Vect 32 Bits8 -> Integer
71 | decode_scalar_25519 =
72 |   le_to_integer
73 |   . updateAt 0  (.&. 248)
74 |   . updateAt 31 (.&. 127)
75 |   . updateAt 31 (.|.  64)
76 |
77 | decode_scalar_448 : Vect 56 Bits8 -> Integer
78 | decode_scalar_448 =
79 |   le_to_integer
80 |   . updateAt 0  (.&. 252)
81 |   . updateAt 55 (.|. 128)
82 |
83 | public export
84 | x25519 : XCurvesParameter 32
85 | x25519 = XCParam 255 9 121665 decode_scalar_25519 $ (bit 255) - 19
86 |
87 | public export
88 | x448 : XCurvesParameter 56
89 | x448 = XCParam 448 5 39081 decode_scalar_448 $ (bit 448) - (bit 224) - 1
90 |