Hedged ML-KEM-1024

@[reducible, inline]

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

Equations

• Cryptlib.Primitives.KEM.MLKEMHedged.encaps1024Hedged = Cryptlib.Primitives.KEM.MLKEMHedged.encapsHedged MLKEM.ParameterSet.MLKEM1024

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged1024 : KEM.KEM

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

Equations

• Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged1024 = Cryptlib.Primitives.KEM.MLKEMHedged.kem MLKEM.ParameterSet.MLKEM1024

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged1024Seed : KEM.KEM

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

Equations

• Cryptlib.Primitives.KEM.MLKEMHedged.kemMLKEMHedged1024Seed = Cryptlib.Primitives.KEM.MLKEMHedged.kemSeed MLKEM.ParameterSet.MLKEM1024