
  0 | module Crypto.Curve
  1 | 
  2 | import Crypto.Random
  3 | import Data.Bits
  4 | import Utils.Misc
  5 | 
  6 | public export
  7 | interface Point p where
  8 |   to_affine : p -> (Integer, Integer)
  9 |   generator : p
 10 |   infinity : p
 11 |   bits : Nat
 12 |   modulus : Integer
 13 |   order : Integer
 14 | 
 15 |   point_add : p -> p -> p
 16 |   mul : Integer -> p -> p
 17 | 
 18 |   encode : p -> List Bits8
 19 |   decode : List Bits8 -> Maybe p
 20 | 
 21 | Point p => Eq p where
 22 |   (==) a b = (to_affine a) == (to_affine b)
 23 | 
 24 | public export
 25 | data ECDSASignature : (p : Type) -> Type where
 26 |   MkSignature : (Point p) => p -> (Integer, Integer) -> ECDSASignature p
 27 | 
 28 | public export
 29 | ecdsa_sign : (Point p, MonadRandom m) => (sk : Integer) -> (msg : Integer) -> m (ECDSASignature p)
 30 | ecdsa_sign {p} private_key message = do
 31 |   k <- uniform_random' 1 (order {p} - 1)
 32 |   let public_key = mul private_key generator {p}
 33 |   let (x, y) = to_affine $ mul k generator {p}
 34 |   let r = x `mod` (order {p})
 35 |   let s = mul_mod (inv_mul_mod k $ order {p}) (message + (r * private_key)) (order {p})
 36 |   if (r == 0) || (s == 0)
 37 |      then ecdsa_sign {p} private_key message
 38 |      else pure $ MkSignature public_key (r, s)
 39 | 
 40 | within_interval : Point p => Integer -> Bool
 41 | within_interval n = n > 0 && n < (order {p})
 42 | 
 43 | public export
 44 | ecdsa_verify : Integer -> ECDSASignature p -> Bool
 45 | ecdsa_verify message (MkSignature public_key (r, s)) =
 46 |   let n = order {p}
 47 |       s_inv = inv_mul_mod s n
 48 |       u1 = mul_mod message s_inv n
 49 |       u2 = mul_mod r s_inv n
 50 |       pt = point_add (mul u1 generator) (mul u2 public_key)
 51 |       (x, _) = to_affine pt
 52 |   in within_interval {p} r && within_interval {p} s && (infinity /= pt) && (r `mod'` n) == (x `mod'` n)
 53 |