mlkem: add external encaps function #149

- Replace calls by other modules to internal version with external
  versions
- minor clean-up of internal version

Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry

@@ -1041,9 +1041,9 @@ private
  * Warning: This function does not validate input and should not be used
  * externally!
  */
-Encaps_internal : (EncapsulationKey, [32]Byte) -> (SharedSecretKey, Ciphertext)
-Encaps_internal (ek, m) = (K, c) where
-  (K, r) = G(m#H(ek))
+Encaps_internal : EncapsulationKey -> [32]Byte -> (SharedSecretKey, Ciphertext)
+Encaps_internal ek m = (K, c) where
+  (K, r) = G (m # (H ek))
   c = K_PKE::Encrypt ek m r
 
 /**
@@ -1080,7 +1080,7 @@ Decaps_internal (c, dk) = K
 CorrectnessKEM : [32]Byte -> [32]Byte -> [32]Byte -> Bit
 property CorrectnessKEM z d m = (K == K') where
   (pk, sk) = KeyGen_internal d z
-  (K, c) = Encaps_internal(pk, m)
+  (K, c) = Encaps_internal pk m
   K' = Decaps_internal(c, sk)
 
 /*
@@ -1138,6 +1138,32 @@ KeyGen d z = (ek, dk) where
     // Step 6.
     (ek, dk) = KeyGen_internal d' z'
 
+/**
+ * Use the encapsulation key to generate a shared secret an an associated
+ * ciphertext.
+ * [FIPS-203] Section 7.1, Algorithm 20.
+ *
+ * This differs from the spec: it takes the randomness `m` as a parameter
+ * instead of generating it internally (because Cryptol cannot generate
+ * randomness).
+ *
+ * The encapsulation key passed as a parameter MUST be checked before use! The
+ * caller must have assurance that the encapsulation key is valid.
+ * @todo Marcella Hastings: once the validation function is written, add link.
+ */
+Encaps : EncapsulationKey -> Option ([32]Byte) -> (SharedSecretKey, Ciphertext)
+Encaps ek m = (K, c) where
+    // Step 1 is skipped because Cryptol cannot generate randomness.
+    // Step 2 - 4.
+    m' = case m of
+        None -> error "Random bit generation failed; `m` not initialized."
+        Some _m -> _m
+    // Step 5.
+    (K, c) = Encaps_internal ek m'
+
+
+
+
 
 parameter
     /*

Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM1024.cry

@@ -18,7 +18,7 @@ import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM1024 as ML_K
  */
 property t0 = keygenWorks && encapsWorks && decapsWorks where
     keygenWorks = ML_KEM::KeyGen (Some d) (Some z) == (pk, sk)
-    encapsWorks = ML_KEM::Encaps_internal (pk, msg) == (ss, ct)
+    encapsWorks = ML_KEM::Encaps pk (Some msg) == (ss, ct)
     decapsWorks = ML_KEM::Decaps_internal (ct, sk) == ss
 
     z = split 0xf696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68

Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM512.cry

@@ -18,7 +18,7 @@ import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM512 as ML_KE
  */
 property t0 = keygenWorks && encapsWorks && decapsWorks where
     keygenWorks = ML_KEM::KeyGen (Some d) (Some z) == (pk, sk)
-    encapsWorks = ML_KEM::Encaps_internal (pk, msg) == (ss, ct)
+    encapsWorks = ML_KEM::Encaps pk (Some msg) == (ss, ct)
     decapsWorks = ML_KEM::Decaps_internal (ct, sk) == ss
     decapsFailsCorrectly = ML_KEM::Decaps_internal (ct_n, sk) == ss_n
 

Primitive/Asymmetric/Cipher/ML_KEM/Tests/ML_KEM768.cry

@@ -18,7 +18,7 @@ import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM768 as ML_KE
  */
 property t0 = keygenWorks && encapsWorks && decapsWorks where
     keygenWorks = ML_KEM::KeyGen (Some d) (Some z) == (pk, sk)
-    encapsWorks = ML_KEM::Encaps_internal (pk, msg) == (ss, ct)
+    encapsWorks = ML_KEM::Encaps pk (Some msg) == (ss, ct)
     decapsWorks = ML_KEM::Decaps_internal (ct, sk) == ss
 
     z = split 0xf696484048ec21f96cf50a56d0759c448f3779752f0383d37449690694cf7a68

Primitive/Asymmetric/Cipher/ML_KEM/Tests/kat.awk

@@ -25,7 +25,7 @@ $1 == "ct" { print "let c_expected =", "0x" $3 }
 $1 == "ss" { print "let K_expected =", "0x" $3 }
 
 $1 == "ss" { print "let (ek_actual, dk_actual) = KeyGen (Some (groupBy d)) (Some (groupBy z))"
-             print "let (K, c_actual) = Encaps_internal(ek_actual, groupBy msg)"
+             print "let (K, c_actual) = Encaps ek_actual (Some (groupBy msg))"
              print "let K_actual = Decaps_internal(c_actual, dk_actual)"
              print "(ek_expected == join ek_actual) && (dk_expected == join dk_actual) && (c_expected == join c_actual) && (K_expected == join K_actual)"
            }