ecdsa: add the other P384 test vector #94

Primitive/Asymmetric/Signature/ECDSA/Tests/ECDSA_P384.cry

@@ -14,12 +14,12 @@ import Common::utils(BVtoZ)
 
 /**
  * Test vector for ECDSA with curve P-384 and SHA-256 as the hash.
- * [RFC6979] Appendeix A.2.6.
+ * [RFC6979] Appendix A.2.6.
  * ```repl
- * :prove testVector
+ * :prove sampleVector
  * ```
  */
-property testVector = signIsCorrect && verifyIsCorrect
+property sampleVector = signIsCorrect && verifyIsCorrect
   where
     M = join "sample"
     d = BVtoZ 0x6B9D3DAD2E1B8C1C05B19875B6659F4DE23C3B667BF297BA9AA47740787137D896D5724E4C70A825F872C9EA60D2EDF5
@@ -37,3 +37,27 @@ property testVector = signIsCorrect && verifyIsCorrect
         Some (r,s) -> ECDSA::verify M (r,s) Q
         None -> False
 
+/**
+ * Test vector for ECDSA with curve P-384 and SHA-256 as the hash.
+ * [RFC6979] Appendix A.2.6.
+ * ```repl
+ * :prove testVector
+ * ```
+ */
+property testVector = signIsCorrect && verifyIsCorrect
+  where
+    M = join "test"
+    d = BVtoZ 0x6B9D3DAD2E1B8C1C05B19875B6659F4DE23C3B667BF297BA9AA47740787137D896D5724E4C70A825F872C9EA60D2EDF5
+    k = BVtoZ 0x0CFAC37587532347DC3389FDC98286BBA8C73807285B184C83E62E26C401C0FAA48DD070BA79921A3457ABFF2D630AD7
+    expected_r = BVtoZ 0x6D6DEFAC9AB64DABAFE36C6BF510352A4CC27001263638E5B16D9BB51D451559F918EEDAF2293BE5B475CC8F0188636B
+    expected_s = BVtoZ 0x2D46F3BECBCC523D5F1A1256BF0C9B024D879BA9E838144C8BA6BAEB4B53B47D51AB373F9845C0514EEFB14024787265
+
+    sig = ECDSA::sign M d k
+    signIsCorrect = case sig of
+        Some (r,s) -> (expected_r == r) && (expected_s == s)
+        None -> False
+
+    Q = ECDSA::publicKey d
+    verifyIsCorrect = case sig of
+        Some (r,s) -> ECDSA::verify M (r,s) Q
+        None -> False