Documentation

Cryptlib.Primitives.KEM.MLKEMHedged.MLKEMHedged

Hedged ML-KEM: round-3 Kyber's m ← H(m) pre-hash #

Encapsulation replaces the sampled message m with H(m) before deriving coins and encrypting, hedging against a weak RNG. This is not FIPS 203. Decapsulation, key generation and encodings are FIPS203's.

encapsHedged #

source
def Cryptlib.Primitives.KEM.MLKEMHedged.encapsHedged (ps : MLKEM.ParameterSet) (ek : MLKEM.EncapsulationKey (FIPS203.params ps) (FIPS203.encoding ps)) (m : MLKEM.Message) :
MLKEM.SharedSecret × MLKEM.Ciphertext (FIPS203.params ps) (FIPS203.encoding ps)

ML-KEM.Encaps_internal on H(m), with H = SHA3-256.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Cryptlib.Primitives.KEM.MLKEMHedged.encapsHedged_eq_encaps_hashH (ps : MLKEM.ParameterSet) (ek : MLKEM.EncapsulationKey (FIPS203.params ps) (FIPS203.encoding ps)) (m : MLKEM.Message) :
    encapsHedged ps ek m = FIPS203.encaps ps ek (FIPS203.hashH (Util.Bytes.ofVector m))

    Hedged encapsulation is FIPS203.encaps applied to H(m).

    The KEM.KEM instance #

    State and randomness are FIPS203's.

    source
    def Cryptlib.Primitives.KEM.MLKEMHedged.Reliable (ps : MLKEM.ParameterSet) (s : FIPS203.State) :
    Prop

    The next draw from s, encapsulated with encapsHedged against any key pair, decapsulates correctly.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Cryptlib.Primitives.KEM.MLKEMHedged.encapM (ps : MLKEM.ParameterSet) (pk : FIPS203.PublicKey ps) :
      EStateM KEM.KEMError FIPS203.State (FIPS203.CT ps × Vector UInt8 32)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Cryptlib.Primitives.KEM.MLKEMHedged.honestRoundTripM (ps : MLKEM.ParameterSet) (sk : FIPS203.PrivateKey ps) (s : FIPS203.State) (hrel : Reliable ps s) (c : FIPS203.CT ps) (k : Vector UInt8 32) (s' : FIPS203.State) (hc : encapM ps (FIPS203.derivePublicKeyM ps sk) s = EStateM.Result.ok (c, k) s') (t : FIPS203.State) :
        ∃ (t' : FIPS203.State), FIPS203.decapM ps sk c t = EStateM.Result.ok k t'

        Round trip from a Reliable state, as FIPS203.honestRoundTripM.

        source
        def Cryptlib.Primitives.KEM.MLKEMHedged.kem (ps : MLKEM.ParameterSet) :
        KEM.KEM

        Hedged ML-KEM with the expanded FIPS 203 private key.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Seed-format private keys, as in FIPS203.kemSeed #

          source
          theorem Cryptlib.Primitives.KEM.MLKEMHedged.honestRoundTripFromSeed (ps : MLKEM.ParameterSet) (sk : FIPS203.SeedPrivateKey) (s : FIPS203.State) :
          Reliable ps s → ∀ (c : FIPS203.CT ps) (k : Vector UInt8 32) (s' : FIPS203.State), encapM ps (FIPS203.derivePublicKeyFromSeed ps sk) s = EStateM.Result.ok (c, k) s' → ∀ (t : FIPS203.State), ∃ (t' : FIPS203.State), FIPS203.decapMFromSeed ps sk c t = EStateM.Result.ok k t'
          source
          def Cryptlib.Primitives.KEM.MLKEMHedged.kemSeed (ps : MLKEM.ParameterSet) :
          KEM.KEM

          Hedged ML-KEM with FIPS203.kemSeed's private-key format.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For