Hedged ML-KEM-768

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEMHedged.encaps768Hedged (ek : MLKEM.EncapsulationKey (FIPS203.params MLKEM.ParameterSet.MLKEM768) (FIPS203.encoding MLKEM.ParameterSet.MLKEM768)) (m : MLKEM.Message) : MLKEM.SharedSecret × MLKEM.Ciphertext (FIPS203.params MLKEM.ParameterSet.MLKEM768) (FIPS203.encoding MLKEM.ParameterSet.MLKEM768)

Equations

• Cryptlib.Primitives.KEM.MLKEMHedged.encaps768Hedged = Cryptlib.Primitives.KEM.MLKEMHedged.encapsHedged MLKEM.ParameterSet.MLKEM768

theorem Cryptlib.Primitives.KEM.MLKEMHedged.encaps768Hedged_eq_encaps768_hashH (ek : MLKEM.EncapsulationKey MLKEM768.params MLKEM768.encoding) (m : MLKEM.Message) : encaps768Hedged ek m = MLKEM768.encaps768 ek (FIPS203.hashH (Util.Bytes.ofVector m))

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged768 : KEM.KEM

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

Equations

• Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged768 = Cryptlib.Primitives.KEM.MLKEMHedged.kem MLKEM.ParameterSet.MLKEM768

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged768Seed : KEM.KEM

Hedged ML-KEM-768 with the ek ‖ d ‖ z seed private key.

Equations

• Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged768Seed = Cryptlib.Primitives.KEM.MLKEMHedged.kemSeed MLKEM.ParameterSet.MLKEM768