Merge pull request #212 from GaloisInc/192-verify

MLDSA: Add internal verify function

Primitive/Asymmetric/Signature/ML_DSA/Specification.cry

@@ -26,25 +26,12 @@ module Primitive::Asymmetric::Signature::ML_DSA::Specification where
 import Primitive::Keyless::Hash::SHAKE::SHAKE128 as SHAKE128
 import Primitive::Keyless::Hash::SHAKE::SHAKE256 as SHAKE256
 
-type Byte = [8]
-
-/**
- * Public key for the ML-DSA scheme.
- * [FIPS-204] Section 5.1, Algorithm 1 (and throughout).
- */
-type PublicKey = [32 + 32 * k * (width (q - 1) - d)]Byte
-
 /**
- * Private key for the ML-DSA scheme.
- * [FIPS-204] Section 5.1, Algorithm 1 (and throughout).
+ * The set {0, 1, ..., 255} of integers represented by a byte, denoted 𝔹 in
+ * the spec.
+ * [FIPS-204] Section 2.3, "𝔹".
  */
-type PrivateKey = [32 + 32 + 64 + 32 * ((k + ell) * width (2 * η) + d * k)]Byte
-
-/**
- * Signature generated by the ML-DSA scheme.
- * [FIPS-204] Section 5.2, Algorithm 2 (and throughout).
- */
-type Signature = [λ / 4 + ell * 32 * (1 + width (γ1 - 1)) + ω + k]Byte
+type Byte = [8]
 
 /**
  * The `bitlen` function defined in the spec is equivalent to the Cryptol
@@ -319,9 +306,33 @@ type d = 13
  */
 β = `(η * τ) : Integer
 
+/**
+ * Public key for the ML-DSA scheme.
+ * [FIPS-204] Section 5.1, Algorithm 1 (and throughout).
+ */
+type PublicKey = [32 + 32 * k * (width (q - 1) - d)]Byte
+
+/**
+ * Private key for the ML-DSA scheme.
+ * [FIPS-204] Section 5.1, Algorithm 1 (and throughout).
+ */
+type PrivateKey = [32 + 32 + 64 + 32 * ((k + ell) * width (2 * η) + d * k)]Byte
+
+/**
+ * Signature generated by the ML-DSA scheme.
+ * [FIPS-204] Section 5.2, Algorithm 2 (and throughout).
+ */
+type Signature = [λ / 4 + ell * 32 * (1 + width (γ1 - 1)) + ω + k]Byte
+
 /**
  * Generate a public-private key pair from a seed.
  * [FIPS-204] Section 6.1, Algorithm 6.
+ *
+ * Warning: This interface must not be made available to applications (other
+ * than for testing purposes)! Implementations must manually verify that this
+ * interface is not public.
+ * The randomness `ξ` passed to this function should be generated by a
+ * cryptographic module.
  */
 KeyGen_internal : [32]Byte -> (PublicKey, PrivateKey)
 KeyGen_internal ξ = (pk, sk) where
@@ -353,6 +364,12 @@ KeyGen_internal ξ = (pk, sk) where
 /**
  * Deterministic algorithm to generate a signature for a formatted message `M'`.
  * [FIPS-204] Section 6.2, Algorithm 7.
+ *
+ * Warning: This interface must not be made available to applications (other
+ * than for testing purposes)! Implementations must manually verify that this
+ * interface is not public.
+ * The randomness `rnd` passed to this function should be generated by a
+ * cryptographic module.
  */
 Sign_internal : {m} (fin m) => PrivateKey -> [m] -> [32]Byte -> Signature
 Sign_internal sk M' rnd = σ where
@@ -412,6 +429,51 @@ Sign_internal sk M' rnd = σ where
     // Step 33.
     σ = sigEncode c_tilFinal (modPlusMinus_Vec zFinal) hFinal
 
+/**
+ * Internal function to verify a signature for a formatted message.
+ * [FIPS-204] Section 6.3, Algorithm 8.
+ *
+ * This interface should not be provided to applications (other than for
+ * testing purposes).
+ *
+ * If an implementation accepts inputs for the public key or the signature of
+ * any length other than those defined by `PublicKey` and `Signature`, this
+ * function should reject them.
+ */
+Verify_internal : {m} (fin m) => PublicKey -> [m] -> Signature -> Bool
+Verify_internal pk M' σ = isValid where
+    // Step 1 - 2.
+    (rho, t1) = pkDecode pk
+    (c_til, z, h) = sigDecode σ
+
+    // Step 5.
+    A_hat = ExpandA rho
+    // Step 6.
+    tr = H`{64} pk
+    // Step 7. The endianness does not align with the spec here -- we had to
+    // use `join` instead of `BytesToBits`.
+    mu = HBits`{64} (join tr # M')
+
+    // Step 8.
+    [c] = castToRq [(SampleInBall c_til)]
+
+    // These casts are implicit in Step 9 in the sepc.
+    t1' = castToRq t1
+    z' = castToRq z
+    // The spec uses the shorthand `t1 * 2^d`; in Cryptol, we need to create
+    // a matrix with the same dimensions as `t1` where every element is `2^d`.
+    two_d = repeat (repeat (2^^`d))
+
+    // Step 9.
+    wApprox' = NTTInv_Vec (A_hat ∘∘ NTT_Vec z' - (NTT c ∘ NTT_Vec (t1' * two_d)))
+
+    // Steps 3 - 4, 10 - 13.
+    isValid = case h of
+        None -> False
+        Some h' -> (infNormR z < `γ1 - β) && (c_til == c_til') where
+            w1' = UseHint h' wApprox'
+            c_til' = H`{λ / 4} (mu # w1Encode w1')
+
 /**
  * Compute a base-2 representation of the input mod `2^α` using little-endian
  * order.
@@ -1299,7 +1361,7 @@ MakeHint z_vec r_vec = hint where
  * the vectors, per the description at the beginning of Section 7.4.
  */
 UseHint : [k]R2 -> [k]Rq -> [k]R
-UseHint h_vec r_vec = r1_vec where
+UseHint h_vec r_vec = r1'_vec where
     // Step 1.
     m = (`q - 1) / (2 * `γ2)
     // Step 2.

Primitive/Asymmetric/Signature/ML_DSA/Tests/ML_DSA_44.cry

@@ -22,14 +22,21 @@ import Primitive::Asymmetric::Signature::ML_DSA::Instantiations::ML_DSA_44 as ML
  * "Raw" categorizes the set of functions being tested -- in this case, the
  * `{KeyGen, Sign, Verify}_internal` functions. See [PQC-KAT] README.md for
  * more details.
+ *
+ * The [PQC-KAT] vectors provide the expected signature in the format
+ * `sig || msg`, while [FIPS-204] has sign and verify interact with just `sig`.
  */
-tryDetKAT xi expected_pk expected_sk msg expected_sig = signWorks where
+tryDetKAT xi expected_pk expected_sk msg expected_sig = mldsaWorks where
     (pk, sk) = ML_DSA::KeyGen_internal xi
     keygenWorks = (pk == expected_pk) && (sk == expected_sk)
 
     sig = ML_DSA::Sign_internal expected_sk msg zero
     signWorks = expected_sig == (sig # (split msg))
 
+    verifyWorks = ML_DSA::Verify_internal expected_pk msg (take expected_sig)
+
+    mldsaWorks = keygenWorks && signWorks && verifyWorks
+
 /**
  * Test the raw, deterministic KAT with count 0.
  * ```repl