
  0 | module Crypto.ECDH
  1 | 
  2 | import Crypto.Random
  3 | import Crypto.Curve.XCurves
  4 | import Crypto.Curve
  5 | import Data.Vect
  6 | import Utils.Misc
  7 | import Utils.Bytes
  8 | 
  9 | public export
 10 | interface ECDHCyclicGroup (0 a : Type) where
 11 |   Scalar : Type
 12 |   Element : Type
 13 |   diffie_hellman : Scalar -> Element -> Maybe (List Bits8)
 14 |   generate_key_pair : MonadRandom m => m (Scalar,Element)
 15 | 
 16 |   deserialize_pk : List Bits8 -> Maybe Element
 17 |   serialize_pk : Element -> List Bits8
 18 | 
 19 | public export
 20 | deserialize_then_dh : ECDHCyclicGroup dh => Scalar {a=dh} -> List Bits8 -> Maybe (List Bits8)
 21 | deserialize_then_dh sk pk = (deserialize_pk {a=dh} pk) >>= (diffie_hellman sk)
 22 | 
 23 | public export
 24 | data X25519_DH : Type where
 25 | 
 26 | public export
 27 | ECDHCyclicGroup X25519_DH where
 28 |   Scalar = Vect 32 Bits8
 29 |   Element = Vect 32 Bits8
 30 |   diffie_hellman sk pk = map toList (XCurves.mul x25519 sk pk)
 31 |   generate_key_pair = do
 32 |     sk <- random_bytes 32
 33 |     let Just pk = derive_public_key x25519 sk
 34 |     | Nothing => generate_key_pair {a=X25519_DH}
 35 |     pure (sk,pk)
 36 |   deserialize_pk content = exactLength 32 $ fromList content
 37 |   serialize_pk = toList
 38 | 
 39 | public export
 40 | data X448_DH : Type where
 41 | 
 42 | public export
 43 | ECDHCyclicGroup X448_DH where
 44 |   Scalar = Vect 56 Bits8
 45 |   Element = Vect 56 Bits8
 46 |   diffie_hellman sk pk = map toList (XCurves.mul x448 sk pk)
 47 |   generate_key_pair = do
 48 |     sk <- random_bytes 56
 49 |     let Just pk = derive_public_key x448 sk
 50 |     | Nothing => generate_key_pair {a=X448_DH}
 51 |     pure (sk,pk)
 52 |   deserialize_pk content = exactLength 56 $ fromList content
 53 |   serialize_pk = toList
 54 | 
 55 | public export
 56 | {p : _} -> Point p => ECDHCyclicGroup p where
 57 |   Scalar = Integer
 58 |   Element = p
 59 |   diffie_hellman sk pk =
 60 |     let (x, _) = to_affine $ mul sk pk
 61 |         bytes = divCeilNZ (bits {p=p}) 8 SIsNonZero
 62 |     in Just $ toList $ integer_to_be bytes x
 63 |   generate_key_pair = do
 64 |     sk <- uniform_random' 2 (order {p=p} - 1)
 65 |     let pk = mul sk $ generator {p=p}
 66 |     pure (sk,pk)
 67 |   deserialize_pk = decode {p=p}
 68 |   serialize_pk = encode {p=p}
 69 |