Add ECDH primitives

Common/EC/ECInterface.cry

@@ -41,16 +41,56 @@ interface module Common::EC::ECInterface where
     type Point : *
 
     /**
-     * Order of the elliptic curve.
+     * Order of the base point `G` for the curve.
      */
     type n : #
     type constraint (fin n, prime n, n >= 1)
 
+    /**
+     * Modulus of the field over which the curve is defined.
+     *
+     * The curve must be defined over a Galois fields `GF(q)` for some `q`
+     * (typically an odd prime or 2^m).
+     */
+    type q : #
+    type constraint (fin q, q >= 1)
+
+    /**
+     * Cofactor for the elliptic curve.
+     *
+     * The order of the curve is defined as `h * n`, where `h` is small
+     * and `n`, the order of the base point `G`, is prime. If `h` is not
+     * 1, then the base point does not generate the entire curve.
+     */
+    h : Integer
+
     /**
      * Base point for the curve.
      */
     G : Point
 
+    /**
+     * Indicate whether a point is the point at infinity (also known as the
+     * identity).
+     */
+    isInfinity : Point -> Bool
+
+    /**
+     * Indicate whether a point is valid: either the point at infinity or
+     * another point on the curve.
+     *
+     * This should check the following:
+     * - The coordinates of the `Point` are correctly formed
+     * - The point is either on the curve (e.g. satisfies the curve equation)
+     *   OR is the point at infinity.
+     */
+    isValid : Point -> Bool
+
+    /**
+     * Indicate whether two points are the same.
+     */
+    pointEq : Point -> Point -> Bool
+
     /**
      * Addition of two points.
      */
@@ -80,12 +120,7 @@ interface module Common::EC::ECInterface where
     twin_mul : Integer -> Point -> Integer -> Point -> Point
 
     /**
-     * ECDSA requires a routine to extract the x-coordinate of the affine
-     * representation of a `Point` and convert it from a field element an
-     * integer mod the order of the curve (`n`). This is not defined and
-     * returns `None` for the point at infinity.
-     *
-     * For NIST-standardized curves, this should match the conversion
-     * routine in [SP-800-186] Appendix F.1.
+     * Extract the x-coordinate of the affine representation of a `Point`,
+     * or `None` if it's the point at infinity.
      */
-    xCoordModOrder: Point -> Option (Z n)
+    xCoord: Point -> Option (Z q)

Common/EC/PrimeField/PFEC.cry

@@ -97,6 +97,14 @@ parameter
  */
 type n = n'
 
+/**
+ * Modulus of the field over which the curve is defined.
+ *
+ * This is called `q` for the `ECInterface`, which is designed to support
+ * curves that are not necessarily over prime order fields.
+ */
+type q = P
+
 /**
  * Coefficient that defines the curve.
  * For a curve in short-Weierstrass form, the equation is
@@ -146,18 +154,35 @@ affineEq p1 p2 = case p1 of
         Affine x' y' -> (x == x') && (y == y')
         _ -> False
 
+/**
+ * The EC interface uses `pointEq` to compare equality on two points, since it
+ * isn't prescriptive about what its point type is, exactly.
+ */
+pointEq = affineEq
+
 /**
  * Check that a given point is on the curve -- either it is the point at
  * infinity or it satisfies the curve equation.
  * [SP-800-186] Section 2.1.1.
  * [SEC1-v2] Section 2.2.1.
  * [MATH-2008] Routine 2.2.5.
+ *
+ * Note: by definition, the coordinates of an affine point will be correctly
+ * formed (e.g. in the range [0, P-1]), because they are of type `Z P`.
  */
-valid_point : Point -> Bit
-valid_point point = case point of
+isValid : Point -> Bit
+isValid point = case point of
     Infinity -> True
     Affine x y -> (y ^^ 2 == x ^^ 3 + a * x + b)
 
+/**
+ * Indicate whether a point is the point at infinity.
+ */
+isInfinity : Point -> Bool
+isInfinity point = case point of
+    Infinity -> True
+    _ -> False
+
 /**
  * Convenient `Point` representation of the base point `G`.
  */
@@ -191,13 +216,13 @@ property gOrderIsN = affineEq G ((`n + 1) ~* G)
  * :prove gIsValid
  * ```
  */
-property gIsValid = valid_point G
+property gIsValid = isValid G
 
 /**
  * Add two elliptic curve points together.
  *
  * Assumption: The `Point`s passed as parameters must be valid EC points,
- * otherwise this operation makes no sense. Use `valid_point` to make sure
+ * otherwise this operation makes no sense. Use `isValid` to make sure
  * the inputs are valid before calling this function.
  */
 add : Point -> Point -> Point
@@ -210,7 +235,7 @@ add p1 p2 = to_affine (ec_full_add (to_projective p1) (to_projective p2))
  * :check addIsClosed
  * ```
  */
-property addIsClosed k1 k2 = valid_point (add p1 p2)
+property addIsClosed k1 k2 = isValid (add p1 p2)
     where
         p1 = validPointFromK k1
         p2 = validPointFromK k2
@@ -219,7 +244,7 @@ property addIsClosed k1 k2 = valid_point (add p1 p2)
  * Double an elliptic curve point.
  *
  * Assumption: The `Point` passed as a parameter must be a valid EC point,
- * otherwise this operation makes no sense. Use `valid_point` to make sure
+ * otherwise this operation makes no sense. Use `isValid` to make sure
  * the input is valid before calling this function.
  */
 double : Point -> Point
@@ -232,15 +257,15 @@ double p = to_affine (ec_double (to_projective p))
  * :check doubleIsClosed
  * ```
  */
-property doubleIsClosed k = valid_point (double p)
+property doubleIsClosed k = isValid (double p)
     where
         p = validPointFromK k
 
 /**
  * Subtract one curve point from another.
  *
  * Assumption: The `Point`s passed as parameters must be valid EC points,
- * otherwise this operation makes no sense. Use `valid_point` to make sure
+ * otherwise this operation makes no sense. Use `isValid` to make sure
  * the inputs are valid before calling this function.
  */
 sub : Point -> Point -> Point
@@ -253,7 +278,7 @@ sub p1 p2 = to_affine (ec_full_sub (to_projective p1) (to_projective p2))
  * :check subIsClosed
  * ```
  */
-property subIsClosed k1 k2 = valid_point (sub p1 p2)
+property subIsClosed k1 k2 = isValid (sub p1 p2)
     where
         p1 = validPointFromK k1
         p2 = validPointFromK k2
@@ -270,7 +295,7 @@ property subIsClosed k1 k2 = valid_point (sub p1 p2)
  * In this implementation, we use a variant from [MATH-2008] (see `ec_mult`).
  *
  * Assumption: The `Point` passed as a parameter must be a valid EC point,
- * otherwise this operation makes no sense. Use `valid_point` to make sure
+ * otherwise this operation makes no sense. Use `isValid` to make sure
  * the input is valid before calling this function.
  */
 scmul : Integer -> Point -> Point
@@ -285,7 +310,7 @@ scmul k p = to_affine (ec_mult (fromInteger k) (to_projective p))
  * :check scmulIsClosed
  * ```
  */
-property scmulIsClosed m = valid_point (m ~* G)
+property scmulIsClosed m = isValid (m ~* G)
 
 /**
  * Scalar multiplication is commutative.
@@ -304,18 +329,14 @@ twin_mul c P d Q = to_affine (ec_twin_mult c' P' d' Q')
         [c', d'] = [fromInteger   x | x <- [c, d]]
         [P', Q'] = [to_projective p | p <- [P, Q]]
 
-
-
 /**
- * Convert the x-coordinate `Z P` value into a `Z n` value, if the point is not
- * the point at infinity.
- *
- * [SP-800-186] Appendix F.1.
+ * Extract the x-coordinate `Z P` value, if the point is not the point at
+ * infinity.
  */
-xCoordModOrder: Point -> Option (Z n)
-xCoordModOrder p = case p of
+xCoord: Point -> Option (Z P)
+xCoord p = case p of
     Infinity -> None
-    Affine x _ -> Some (fromInteger (fromZ x))
+    Affine x _ -> Some x
 
 
 private

Common/EC/PrimeField/Tests/P192.cry

@@ -34,7 +34,7 @@ T = P192::Affine (BVtoZ 0xf22c4395213e9ebe67ddecdd87fdbd01be16fb059b9753a4)
  * :prove sAndTAreValid
  * ```
  */
-property sAndTAreValid = P192::valid_point S && P192::valid_point T
+property sAndTAreValid = P192::isValid S && P192::isValid T
 
 /**
  * ```repl

Common/EC/PrimeField/Tests/P224.cry

@@ -30,7 +30,7 @@ T = P224::Affine (BVtoZ 0xb72b25aea5cb03fb88d7e842002969648e6ef23c5d39ac903826bd
  * :prove sAndTAreValid
  * ```
  */
-property sAndTAreValid = P224::valid_point S && P224::valid_point T
+property sAndTAreValid = P224::isValid S && P224::isValid T
 
 /**
  * ```repl

Common/EC/PrimeField/Tests/P256.cry

@@ -29,7 +29,7 @@ T = P256::Affine (BVtoZ 0x55a8b00f8da1d44e62f6b3b25316212e39540dc861c89575bb8cf9
  * :prove sAndTAreValid
  * ```
  */
-property sAndTAreValid = P256::valid_point S && P256::valid_point T
+property sAndTAreValid = P256::isValid S && P256::isValid T
 
 /**
  * ```repl

Common/EC/PrimeField/Tests/P384.cry

@@ -30,7 +30,7 @@ T = P384::Affine (BVtoZ 0xaacc05202e7fda6fc73d82f0a66220527da8117ee8f8330ead7d20
  * :prove sAndTAreValid
  * ```
  */
-property sAndTAreValid = P384::valid_point S && P384::valid_point T
+property sAndTAreValid = P384::isValid S && P384::isValid T
 
 /**
  * ```repl

Common/EC/PrimeField/Tests/P521.cry

@@ -30,7 +30,7 @@ T = P521::Affine (BVtoZ 0x000000f411f2ac2eb971a267b80297ba67c322dba4bb21cec8b700
  * :prove sAndTAreValid
  * ```
  */
-property sAndTAreValid = P521::valid_point S && P521::valid_point T
+property sAndTAreValid = P521::isValid S && P521::isValid T
 
 /**
  * ```repl

Primitive/Asymmetric/Generation/ECDH/Instantiations/ECDH_P256.cry

@@ -0,0 +1,14 @@
+/*
+ * Instantiate cryptographic primitives for key establishment with curve P-256
+ * (also known as secp256p1).
+ *
+ * @copyright Galois, Inc.
+ * @author Marcella Hastings <marcella@galois.com>
+ */
+module Primitive::Asymmetric::Generation::ECDH::Instantiations::ECDH_P256 =
+    Primitive::Asymmetric::Generation::ECDH::Specification {
+        Common::EC::PrimeField::Instantiations::P256
+    }
+
+
+