Add XMSS parameters

Primitive/Asymmetric/Signature/XMSS/Instantiations/WOTSP_SHA2_256.cry → Primitive/Asymmetric/Signature/WOTS/Instantiations/WOTSP_SHA2_256.cry

@@ -20,14 +20,12 @@
  * @copyright Galois, Inc.
  * @author Marcella Hastings <[email protected]>
  */
-module Primitive::Asymmetric::Signature::XMSS::Instantiations::WOTSP_SHA2_256 =
-    Primitive::Asymmetric::Signature::XMSS::Wots where
+module Primitive::Asymmetric::Signature::WOTS::Instantiations::WOTSP_SHA2_256 =
+    Primitive::Asymmetric::Signature::WOTS::Specification where
         import Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 as SHA256
 
-        type n = 32
-        type w = 16
-
-        F KEY M = split (SHA256::hash (join ((zero : [32][8]) # KEY # M)))
-        PRF KEY M = split (SHA256::hash (join ((zero : [31][8]) # [(3 : [8])] # KEY # M)))
-
+        type n' = 32
+        type w' = 16
 
+        F' KEY M = split (SHA256::hash (join ((zero : [32][8]) # KEY # M)))
+        PRF' KEY M = split (SHA256::hash (join ((zero : [31][8]) # [(3 : [8])] # KEY # M)))

Primitive/Asymmetric/Signature/WOTS/Interface.cry

@@ -0,0 +1,141 @@
+/*
+ * Public interface for the WOTS+ one-time signature scheme.
+ *
+ * We expect that there will only be one implementation of this scheme.
+ * However, to support its typical use as a component in a more complex scheme
+ * (like XMSS and SPHINCS+), we want to allow other protocols to be
+ * defined in terms of the generic WOTS, and then instantiated with both
+ * WOTS-specific and scheme-specific parameters (and potentially with
+ * additional interface constraints).
+ *
+ * Some documentation is duplicated between this interface and the
+ * specification. This is based on the API in [RFC-8391].
+ *
+ * [RFC-8391]: Andreas Huelsing, Denis Butin, Stefan-Lukas Gazdag, Joost
+ *     Rijneveld, and Aziz Mohaisen. XMSS: eXtended Merkle Signature Scheme.
+ *     Internet Requests for Comments (RFC) 8391. May 2018.
+ *     @see https://datatracker.ietf.org/doc/rfc8391
+ *
+ * @copyright Galois, Inc.
+ * @author Marcella Hastings <[email protected]>
+ */
+interface module Primitive::Asymmetric::Signature::WOTS::Interface where
+
+/**
+ * Security parameter.
+ * This defines the message length, the length of a private key, the length
+ * of a public key, and a signature element (in bytes).
+ * [RFC-8391] Section 3.1.1.
+ */
+type n : #
+type constraint (fin n)
+
+/**
+ * The Winternitz parameter. This must be either 4 or 16.
+ * [RFC-8391] Section 3.1.1.
+ *
+ * The type constraint is a bit contrived, but it requires that
+ * `w` is in the range `[0, 16]`, is divisible by 4 (`{0, 4, 8, 12, 16}`),
+ * and is congruent to 1 mod 3 (`{4, 16}`).
+ */
+type w : #
+type constraint (fin w, w % 4 == 0, w % 3 == 1, w <= 16)
+
+/**
+ * A keyed cryptographic hash function that takes a key and a message.
+ * [RFC-8391] Section 3.1.1.1.
+ */
+F : [n][8] -> [n][8] -> [n][8]
+
+/**
+ * A pseudorandom function that takes a key and an index.
+ * [RFC-8391] Section 3.1.1.1.
+ */
+PRF : [n][8] -> [32][8] -> [n][8]
+
+/**
+ * A length value (fixed with respect to `n` and `w`).
+ * [RFC-8391] Section 3.1.1.
+ */
+type len_1 = (8 * n) /^ (lg2 w)
+
+/**
+ * A length value (fixed with respect to `n` and `w`).
+ * [RFC-8391] Section 3.1.1.
+ */
+
+type len_2 = lg2 (len_1 * (w - 1)) / lg2 w + 1
+
+/**
+ * The number of `n`-byte string elements in a WOTS+ private key, public key,
+ * and signature.
+ * [RFC-8391] Section 3.1.1.
+ */
+type len = len_1 + len_2
+
+/**
+ * A byte is a sequence of 8 bits using big-endian representation.
+ * [RFC-8391] Section 2.1.
+ */
+type Byte = [8]
+
+/**
+ * Address scheme for randomizing hash function calls in the OTS scheme.
+ * [RFC-8391] Section 2.5.
+ */
+type Address = [8 * 4]Byte
+
+/**
+ * A private, or secret, key in WOTS+ is a length `len` array of `n`-byte
+ * strings.
+ *
+ * It represents the start nodes in a set of hash chains.
+ *
+ * ⚠️ Warning ⚠️: A private key MUST be selected randomly from the uniform
+ * distribution or selected using a cryptographically secure pseudorandom
+ * process! Cryptol cannot verify that a `PrivateKey` was chosen suitably!
+ * Implementors must independently audit private key generation!
+ *
+ * [RFC-8391] Section 3.1.3.
+ *
+ * An implementation may also use a cryptographically secure pseudorandom
+ * method to generate the private key from a single `n`-byte value. See
+ * [RFC-8391] Section 3.1.7 for a sample method.
+ */
+type PrivateKey = [len][n]Byte
+
+/**
+ * A WOTS+ public key is a length `len` array of `n`-byte strings.
+ *
+ * It represents the end nodes i a set of length-`w` hash chains, where the
+ * start nodes are defined in the corresponding `PrivateKey`.
+ */
+type PublicKey = [len][n]Byte
+
+/**
+ * A WOTS+ signature.
+ * [RFC-8391] Section 3.1.5.
+ */
+type Signature = [len][n]Byte
+
+/**
+ * Generate a WOTS+ public key from a private key.
+ * [RFC-8391] Section 3.1.4, Algorithm 4 (called `WOTS_genPK` in the spec).
+ */
+genPK : PrivateKey -> Address -> [n]Byte -> PublicKey
+
+/**
+ * Generate a signature from a private key and a message.
+ * [RFC-8391] Section 3.1.5, Algorithm 5 (called `WOTS_sign` in the spec).
+ */
+sign : [n]Byte -> PrivateKey -> Address -> [n]Byte -> Signature
+
+/**
+ * Compute a WOTS+ public key from a message and its signature.
+ * [RFC-8391] Section 3.1.6, Algorithm 6 (called `WOTS_pkFromSig` in the spec).
+ *
+ * The result of this function must be compared to the given public key. If
+ * the values are not equal, the signature MUST be rejected. This algorithm
+ * does not actually reject any signatures!!
+ */
+pkFromSig : [n]Byte -> Signature -> Address -> [n]Byte -> PublicKey

Primitive/Asymmetric/Signature/XMSS/Wots.cry → Primitive/Asymmetric/Signature/WOTS/Specification.cry

@@ -1,9 +1,13 @@
 /**
  * WOTS+: One-Time Signatures.
  *
- * This signature primitive is used in the XMSS signature scheme. In WOTS+,
- * a private key can be used to sign any message, but each private key can
- * be used only once.
+ * WOTS+ is a signature scheme. A notable limitation of WOTS+ is that a given
+ * key pair can produce exactly ONE signature; repeated signatures with a
+ * single key pair will compromise the private key!!
+ *
+ * This scheme should typically be used as a component of a less limited
+ * signature scheme, like XMSS or SPHINCS+.
+ *
  * Warning: If a private key is used to sign two different messages, the scheme
  * becomes insecure! Cryptol cannot protect against this failure mode!
  *
@@ -22,8 +26,7 @@
  * @copyright Galois, Inc.
  * @author Marcella Hastings <[email protected]>
  */
-module Primitive::Asymmetric::Signature::XMSS::Wots where
-
+module Primitive::Asymmetric::Signature::WOTS::Specification where
 
 parameter
     /**
@@ -32,8 +35,8 @@ parameter
      * of a public key, and a signature element (in bytes).
      * [RFC-8391] Section 3.1.1.
      */
-    type n : #
-    type constraint (fin n)
+    type n' : #
+    type constraint (fin n')
 
     /**
      * The Winternitz parameter. This must be either 4 or 16.
@@ -43,20 +46,20 @@ parameter
      * `w` is in the range `[0, 16]`, is divisible by 4 (`{0, 4, 8, 12, 16}`),
      * and is congruent to 1 mod 3 (`{4, 16}`).
      */
-    type w : #
-    type constraint (fin w, w % 4 == 0, w % 3 == 1, w <= 16)
+    type w' : #
+    type constraint (fin w', w' % 4 == 0, w' % 3 == 1, w' <= 16)
 
     /**
      * A keyed cryptographic hash function that takes a key and a message.
      * [RFC-8391] Section 3.1.1.1.
      */
-    F : [n][8] -> [n][8] -> [n][8]
+    F' : [n'][8] -> [n'][8] -> [n'][8]
 
     /**
      * A pseudorandom function that takes a key and an index.
      * [RFC-8391] Section 3.1.1.1.
      */
-    PRF : [n][8] -> [32][8] -> [n][8]
+    PRF' : [n'][8] -> [32][8] -> [n'][8]
 
     /**
      * A length value (fixed with respect to `n` and `w`).
@@ -65,15 +68,15 @@ parameter
      * The type constraint is drawn from Algorithm 5, where a computed checksum
      * of length `len_1 * (w - 1) * 2^8` must fit in 32 bits for correctness.
      */
-    type len_1 = (8 * n) /^ (lg2 w)
-    type constraint (width (len_1 * (w - 1) * 2^^8) <= 32)
+    type len_1 = (8 * n') /^ (lg2 w')
+    type constraint (width (len_1 * (w' - 1) * 2^^8) <= 32)
 
     /**
      * A length value (fixed with respect to `n` and `w`).
      * [RFC-8391] Section 3.1.1.
      */
 
-    type len_2 = lg2 (len_1 * (w - 1)) / lg2 w + 1
+    type len_2 = lg2 (len_1 * (w' - 1)) / lg2 w' + 1
 
     /**
      * The number of `n`-byte string elements in a WOTS+ private key, public key,
@@ -98,6 +101,11 @@ parameter
      */
     type constraint (32 >= width len)
 
+type n = n'
+type w = w'
+F = F'
+PRF = PRF'
+
 /**
  * A byte is a sequence of 8 bits using big-endian representation.
  * [RFC-8391] Section 2.1.

Primitive/Asymmetric/Signature/XMSS/Instantiations/XMSS_SHA2_10_256.cry

@@ -0,0 +1,12 @@
+/**
+ * Instantiation of XMSS with the approved parameter set `XMSS_SHA2_10_256`.
+ *
+ * @copyright Galois, Inc
+ * @author Marcella Hastings <[email protected]>
+ */
+module Primitive::Asymmetric::Signature::XMSS::Instantiations::XMSS_SHA2_10_256 =
+    Primitive::Asymmetric::Signature::XMSS::Specification {
+        Parameters = Primitive::Asymmetric::Signature::XMSS::ParameterSets::XMSS_SHA2_10_256_Parameters,
+        WOTS = Primitive::Asymmetric::Signature::WOTS::Instantiations::WOTSP_SHA2_256
+
+    }

Primitive/Asymmetric/Signature/XMSS/ParameterSets/XMSS_SHA2_10_256_Parameters.cry

@@ -0,0 +1,25 @@
+/**
+ * Definition of the approved parameter set used to instantiate
+ * `XMSS_SHA2_10_256`.
+ * [RFC-8391] Section 5.1.
+ *
+ * @copyright Galois, Inc
+ * @author Marcella Hastings <[email protected]>
+ */
+module Primitive::Asymmetric::Signature::XMSS::ParameterSets::XMSS_SHA2_10_256_Parameters
+where
+    import Primitive::Keyless::Hash::SHA2::Instantiations::SHA256 as SHA256
+
+    type n = 32
+    type h = 10
+
+    H KEY M = split (SHA256::hash ((1 : [32 * 8]) # join (KEY # M)))
+
+    // The maximum message width is defined by SHA256.
+    type MaxMessageWidth = SHA256::MaxMessageWidth
+
+    // The padding in this instantiation includes the domain separator (32
+    // bytes) and the key (3n bytes).
+    type PaddingWidth = (32 * 8) + (3 * n * 8)
+
+    H_msg KEY M = split (SHA256::hash ((2 : [32 * 8]) # join (KEY # M)))

Primitive/Asymmetric/Signature/XMSS/Parameters.cry

@@ -0,0 +1,58 @@
+/*
+ * Parameters for the XMSS signature scheme.
+ *
+ * @copyright Galois, Inc
+ * @author Marcella Hastings <[email protected]>
+ */
+interface module Primitive::Asymmetric::Signature::XMSS::Parameters where
+
+/**
+ * Height of the XMSS tree.
+ * [RFC-8391] Section 4.1.1.
+ */
+type h : #
+type constraint (fin h)
+
+/**
+ * The length (in bytes) of the message digest, as well as each node.
+ * [RFC-8391] Section 4.1.1.
+ */
+type n : #
+type constraint (fin n)
+
+/**
+ * A cryptographic hash function that takes a key and a message.
+ * [RFC-8391] Section 4.1.2.
+ */
+H : [n][8] -> [2 * n][8] -> [n][8]
+
+/**
+ * Maximum width in bits for a message under the hash function used to
+ * instantiate `H_msg`.
+ *
+ * `H_msg` allows arbitrary-length messages, but in practice, the hash
+ * functions used to instantiate it may limit their input to some maximum
+ * width.
+ */
+type MaxMessageWidth : #
+
+/**
+ * Width of the non-message bits passed to the hash function in `H_msg`.
+ *
+ * In the approved instantiations defined in [RFC-8391] and [SP-800-208],
+ * this includes domain separation and a fixed-length key.
+ * This is used to enforce the max message width constraint.
+ */
+type PaddingWidth : #
+
+/**
+ * A cryptographic hash function that takes a key and an arbitrary-length
+ * message.
+ * [RFC-8391] Section 4.1.2.
+ *
+ * Note: Some approved instantiations of this function use hash functions that
+ * have a maximum width for messages. The type constraint enforces this by
+ * limiting the length of the hashed message to the maximum width.
+ */
+H_msg : {m} (fin m, (PaddingWidth + width (8 * m)) < MaxMessageWidth)
+    => [3 * n][8] -> [m][8] -> [n][8]

Primitive/Asymmetric/Signature/XMSS/Specification.cry

@@ -0,0 +1,18 @@
+/*
+ * XMSS: eXtended Merkle Signature Scheme.
+ *
+ * References:
+ * [RFC-8391]: Andreas Huelsing, Denis Butin, Stefan-Lukas Gazdag, Joost
+ *     Rijneveld, and Aziz Mohaisen. XMSS: eXtended Merkle Signature Scheme.
+ *     Internet Requests for Comments (RFC) 8391. May 2018.
+ *     @see https://datatracker.ietf.org/doc/rfc8391
+ *
+ * @copyright Galois, Inc.
+ * @author Marcella Hastings <[email protected]>
+ */
+module Primitive::Asymmetric::Signature::XMSS::Specification where
+
+import interface Primitive::Asymmetric::Signature::XMSS::Parameters
+import interface Primitive::Asymmetric::Signature::WOTS::Interface as WOTS
+
+interface constraint (n == WOTS::n)