0 | module Crypto.Curve.Weierstrass
  1 |
  2 | import Crypto.Curve
  3 | import Data.Bits
  4 | import Data.List
  5 | import Data.Vect
  6 | import Utils.Bytes
  7 | import Utils.Misc
  8 |
  9 | -- Weiserstrass curve y^2 = x^3 + ax + b in Jacobian coordinate
 10 | public export
 11 | interface WeierstrassPoint p where
 12 |   a_coefficent : Integer
 13 |   b_coefficent : Integer
 14 |   prime : Integer -- If this isn't prime the skinwalker will devour you
 15 |   to_jacobian : p -> (Integer, Integer, Integer)
 16 |   from_jacobian : (Integer, Integer, Integer) -> p
 17 |   g : p
 18 |   to_from_jacobian : (x : (Integer, Integer, Integer)) -> to_jacobian (from_jacobian x) = x
 19 |   bits' : Nat
 20 |   curve_n : Integer
 21 |
 22 | j_point_double : WeierstrassPoint p => (Integer, Integer, Integer) -> (Integer, Integer, Integer)
 23 | j_point_double (x, y, z) =
 24 |   let modulus = prime {p=p}
 25 |       s  = (4 * x * y * y) `mod'` modulus
 26 |       z4 = pow_mod z 4 modulus
 27 |       y4 = pow_mod y 4 modulus
 28 |       m  = (3 * x * x + a_coefficent {p} * z4) `mod'` modulus
 29 |       x' = (m * m - 2 * s) `mod'` modulus
 30 |       y' = (m * (s - x') - 8 * y4) `mod'` modulus
 31 |       z' = (2 * y * z) `mod'` modulus
 32 |   in (x', y', z')
 33 |
 34 | j_point_add : WeierstrassPoint p => (Integer, Integer, Integer) -> (Integer, Integer, Integer) -> (Integer, Integer, Integer)
 35 | j_point_add (x, y, 0) b = b
 36 | j_point_add a (x, y, 0) = a
 37 | j_point_add a@(xp, yp, zp) b@(xq, yq, zq) =
 38 |   let m = prime {p=p}
 39 |       zq2 = pow_mod zq 2 m
 40 |       zq3 = pow_mod zq 3 m
 41 |       zp2 = pow_mod zp 2 m
 42 |       zp3 = pow_mod zp 3 m
 43 |       u1 = mul_mod xp zq2 m
 44 |       u2 = mul_mod xq zp2 m
 45 |       s1 = mul_mod yp zq3 m
 46 |       s2 = mul_mod yq zp3 m
 47 |       h = u2 - u1
 48 |       r = s2 - s1
 49 |       h2 = pow_mod h 2 m
 50 |       h3 = mul_mod h h2 m
 51 |       u1h2 = mul_mod u1 h2 m
 52 |       nx = ((r * r) - h3 - 2 * u1h2) `mod'` m
 53 |       ny = (r * (u1h2 - nx) - s1 * h3) `mod'` m
 54 |       nz = (h * zp * zq) `mod'` m
 55 |       in if h == 0 then (if r == 0 then j_point_double {p=p} a else (0, 1, 0)) else (nx, ny, nz)
 56 |
 57 | point_double : (Point p, WeierstrassPoint p) => p -> p
 58 | point_double b = from_jacobian {p=p} (j_point_double {p=p} (to_jacobian b))
 59 |
 60 | mul' : (Point p, WeierstrassPoint p) => p -> p -> Nat -> Integer -> p
 61 | mul' r0 r1 m d =
 62 |   let (r0', r1') = if testBit d m then (point_add r0 r1, point_double r1) else (point_double r0, point_add r0 r1)
 63 |   in case m of
 64 |        S m' => mul' r0' r1' m' d
 65 |        Z => r0'
 66 |
 67 | public export
 68 | WeierstrassPoint p => Point p where
 69 |   infinity = from_jacobian (0, 1, 0)
 70 |   generator = g
 71 |   bits = bits' {p=p}
 72 |   to_affine point =
 73 |     let (x, y, z) = to_jacobian point
 74 |         m = prime {p=p}
 75 |         z' = inv_mul_mod z m
 76 |         z2 = z' * z'
 77 |         z3 = z2 * z'
 78 |     in (mul_mod x z2 m, mul_mod y z3 m)
 79 |   modulus = prime {p=p}
 80 |   order = curve_n {p=p}
 81 |   point_add a b = from_jacobian {p=p} (j_point_add {p=p} (to_jacobian a) (to_jacobian b))
 82 |   mul s pt = mul' infinity pt (bits {p=p}) s
 83 |
 84 |   encode point =
 85 |     let bytes = (7 + bits {p=p}) `div` 8
 86 |         (x', y') = to_affine point
 87 |         x = toList $ integer_to_be bytes x'
 88 |         y = toList $ integer_to_be bytes y'
 89 |     in 4 :: (x <+> y)
 90 |
 91 |   decode (4 :: body) = do
 92 |     let bytes = (7 + bits {p=p}) `div` 8
 93 |     let (x', y') = splitAt bytes body
 94 |     x <- map be_to_integer $ exactLength bytes $ fromList x'
 95 |     y <- map be_to_integer $ exactLength bytes $ fromList y'
 96 |
 97 |     -- infinity check
 98 |     guard $ not $ (x == 0) && (y == 0)
 99 |
100 |     -- check on curve
101 |     let pri = modulus {p=p}
102 |     let lhs = pow_mod y 2 pri
103 |     let a   = a_coefficent {p=p}
104 |     let b   = b_coefficent {p=p}
105 |     let rhs = ((pow_mod x 3 pri) + (mul_mod x a pri) + b) `mod'` pri
106 |     guard $ lhs == rhs
107 |
108 |     pure $ from_jacobian (x, y, 1)
109 |   decode _ = Nothing
110 |
111 | public export
112 | data P256 : Type where
113 |   MkP256 : (Integer, Integer, Integer) -> P256
114 |
115 | public export
116 | WeierstrassPoint P256 where
117 |   prime =
118 |     0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff
119 |   a_coefficent =
120 |     0xffffffff00000001000000000000000000000000fffffffffffffffffffffffc
121 |   b_coefficent =
122 |     0x5ac635d8aa3a93e7b3ebbd55769886bc651d06b0cc53b0f63bce3c3e27d2604b
123 |   from_jacobian = MkP256
124 |   to_jacobian (MkP256 p) = p
125 |   g = MkP256
126 |     ( 0x6b17d1f2e12c4247f8bce6e563a440f277037d812deb33a0f4a13945d898c296
127 |     , 0x4fe342e2fe1a7f9b8ee7eb4a7c0f9e162bce33576b315ececbb6406837bf51f5
128 |     , 1 )
129 |   to_from_jacobian x = Refl
130 |   bits' = 256
131 |   curve_n =
132 |     0xffffffff00000000ffffffffffffffffbce6faada7179e84f3b9cac2fc632551
133 |
134 | public export
135 | data P384 : Type where
136 |   MkP384 : (Integer, Integer, Integer) -> P384
137 |
138 | public export
139 | WeierstrassPoint P384 where
140 |   prime =
141 |     0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff
142 |   a_coefficent =
143 |     0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffc
144 |   b_coefficent =
145 |     0xb3312fa7e23ee7e4988e056be3f82d19181d9c6efe8141120314088f5013875ac656398d8a2ed19d2a85c8edd3ec2aef
146 |   from_jacobian = MkP384
147 |   to_jacobian (MkP384 p) = p
148 |   g = MkP384
149 |     ( 0xaa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7
150 |     , 0x3617de4a96262c6f5d9e98bf9292dc29f8f41dbd289a147ce9da3113b5f0b8c00a60b1ce1d7e819d7a431d7c90ea0e5f
151 |     , 1 )
152 |   to_from_jacobian x = Refl
153 |   bits' = 384
154 |   curve_n =
155 |     0xffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973
156 |
157 | public export
158 | data P521 : Type where
159 |   MkP521 : (Integer, Integer, Integer) -> P521
160 |
161 | public export
162 | WeierstrassPoint P521 where
163 |   prime =
164 |     0x01ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
165 |   a_coefficent =
166 |     0x01fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc
167 |   b_coefficent =
168 |     0x0051953eb9618e1c9a1f929a21a0b68540eea2da725b99b315f3b8b489918ef109e156193951ec7e937b1652c0bd3bb1bf073573df883d2c34f1ef451fd46b503f00
169 |   from_jacobian = MkP521
170 |   to_jacobian (MkP521 p) = p
171 |   g = MkP521
172 |     ( 0x00c6858e06b70404e9cd9e3ecb662395b4429c648139053fb521f828af606b4d3dbaa14b5e77efe75928fe1dc127a2ffa8de3348b3c1856a429bf97e7e31c2e5bd66
173 |     , 0x011839296a789a3bc0045c8a5fb42c7d1bd998f54449579b446817afbd17273e662c97ee72995ef42640c550b9013fad0761353c7086a272c24088be94769fd16650
174 |     , 1 )
175 |   to_from_jacobian x = Refl
176 |   bits' = 521
177 |   curve_n =
178 |     0x01fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409
179 |
180 |