ML-KEM-768: FIPS203 at the MLKEM768 parameter set

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.ps : MLKEM.ParameterSet

Equations

• Cryptlib.Primitives.KEM.MLKEM768.ps = MLKEM.ParameterSet.MLKEM768

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.params : MLKEM.Params

Equations

• Cryptlib.Primitives.KEM.MLKEM768.params = Cryptlib.Primitives.KEM.FIPS203.params Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.encoding : MLKEM.Encoding (FIPS203.params ps)

Equations

• Cryptlib.Primitives.KEM.MLKEM768.encoding = Cryptlib.Primitives.KEM.FIPS203.encoding Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.primitives : MLKEM.Primitives (FIPS203.params ps) (FIPS203.encoding ps)

Equations

• Cryptlib.Primitives.KEM.MLKEM768.primitives = Cryptlib.Primitives.KEM.FIPS203.primitives Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.encodingLaws : (FIPS203.encoding ps).Laws

Equations

• Cryptlib.Primitives.KEM.MLKEM768.encodingLaws = ⋯

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.tBytes (x : (FIPS203.encoding ps).EncodedTHat) : ByteArray

Equations

• Cryptlib.Primitives.KEM.MLKEM768.tBytes = Cryptlib.Primitives.KEM.FIPS203.tBytes Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.bytesT (x : ByteArray) : (FIPS203.encoding ps).EncodedTHat

Equations

• Cryptlib.Primitives.KEM.MLKEM768.bytesT = Cryptlib.Primitives.KEM.FIPS203.bytesT Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.uBytes (x : (FIPS203.encoding ps).EncodedU) : ByteArray

Equations

• Cryptlib.Primitives.KEM.MLKEM768.uBytes = Cryptlib.Primitives.KEM.FIPS203.uBytes Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.bytesU (x : ByteArray) : (FIPS203.encoding ps).EncodedU

Equations

• Cryptlib.Primitives.KEM.MLKEM768.bytesU = Cryptlib.Primitives.KEM.FIPS203.bytesU Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.vBytes (x : (FIPS203.encoding ps).EncodedV) : ByteArray

Equations

• Cryptlib.Primitives.KEM.MLKEM768.vBytes = Cryptlib.Primitives.KEM.FIPS203.vBytes Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.bytesV (x : ByteArray) : (FIPS203.encoding ps).EncodedV

Equations

• Cryptlib.Primitives.KEM.MLKEM768.bytesV = Cryptlib.Primitives.KEM.FIPS203.bytesV Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.PublicKey : Type

Equations

• Cryptlib.Primitives.KEM.MLKEM768.PublicKey = Cryptlib.Primitives.KEM.FIPS203.PublicKey Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.PrivateKey : Type

Equations

• Cryptlib.Primitives.KEM.MLKEM768.PrivateKey = Cryptlib.Primitives.KEM.FIPS203.PrivateKey Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.CT : Type

Equations

• Cryptlib.Primitives.KEM.MLKEM768.CT = Cryptlib.Primitives.KEM.FIPS203.CT Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.encodePublicKey (pk : FIPS203.PublicKey ps) : Vector UInt8 (FIPS203.params ps).publicKeyBytes

Equations

• Cryptlib.Primitives.KEM.MLKEM768.encodePublicKey = Cryptlib.Primitives.KEM.FIPS203.encodePublicKey Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decodePublicKey (v : Vector UInt8 (FIPS203.params ps).publicKeyBytes) : Option (FIPS203.PublicKey ps)

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decodePublicKey = Cryptlib.Primitives.KEM.FIPS203.decodePublicKey Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.encodePrivateKey (sk : FIPS203.PrivateKey ps) : Vector UInt8 (FIPS203.params ps).secretKeyBytes

Equations

• Cryptlib.Primitives.KEM.MLKEM768.encodePrivateKey = Cryptlib.Primitives.KEM.FIPS203.encodePrivateKey Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decodePrivateKey (v : Vector UInt8 (FIPS203.params ps).secretKeyBytes) : Option (FIPS203.PrivateKey ps)

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decodePrivateKey = Cryptlib.Primitives.KEM.FIPS203.decodePrivateKey Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.encodeCiphertext (c : FIPS203.CT ps) : Vector UInt8 (FIPS203.params ps).ciphertextBytes

Equations

• Cryptlib.Primitives.KEM.MLKEM768.encodeCiphertext = Cryptlib.Primitives.KEM.FIPS203.encodeCiphertext Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decodeCiphertext (v : Vector UInt8 (FIPS203.params ps).ciphertextBytes) : Option (FIPS203.CT ps)

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decodeCiphertext = Cryptlib.Primitives.KEM.FIPS203.decodeCiphertext Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decode_encode_pub (pk : FIPS203.PublicKey ps) : FIPS203.decodePublicKey ps (FIPS203.encodePublicKey ps pk) = some pk

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decode_encode_pub = ⋯

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decode_encode_priv (sk : FIPS203.PrivateKey ps) : FIPS203.decodePrivateKey ps (FIPS203.encodePrivateKey ps sk) = some sk

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decode_encode_priv = ⋯

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decode_encode_ct (c : FIPS203.CT ps) : FIPS203.decodeCiphertext ps (FIPS203.encodeCiphertext ps c) = some c

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decode_encode_ct = ⋯

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.keygen768 (d z : MLKEM.Seed32) : MLKEM.EncapsulationKey (FIPS203.params ps) (FIPS203.encoding ps) × MLKEM.DecapsulationKey (FIPS203.params ps) (FIPS203.encoding ps)

Equations

• Cryptlib.Primitives.KEM.MLKEM768.keygen768 = Cryptlib.Primitives.KEM.FIPS203.keygen Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

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

Equations

• Cryptlib.Primitives.KEM.MLKEM768.encaps768 = Cryptlib.Primitives.KEM.FIPS203.encaps Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decaps768 (dk : MLKEM.DecapsulationKey (FIPS203.params ps) (FIPS203.encoding ps)) (c : MLKEM.Ciphertext (FIPS203.params ps) (FIPS203.encoding ps)) : MLKEM.SharedSecret

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decaps768 = Cryptlib.Primitives.KEM.FIPS203.decaps Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.keygen768_ek_wf (d z : MLKEM.Seed32) : (FIPS203.tBytes ps (FIPS203.keygen ps d z).1.tHatEncoded).size = 384 * (FIPS203.params ps).k

Equations

• Cryptlib.Primitives.KEM.MLKEM768.keygen768_ek_wf = ⋯

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.keygen768_dk_wf (d z : MLKEM.Seed32) : (FIPS203.tBytes ps (FIPS203.keygen ps d z).2.dkPKE.sHatEncoded).size = 384 * (FIPS203.params ps).k ∧ (FIPS203.tBytes ps (FIPS203.keygen ps d z).2.ekPKE.tHatEncoded).size = 384 * (FIPS203.params ps).k

Equations

• Cryptlib.Primitives.KEM.MLKEM768.keygen768_dk_wf = ⋯

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.checkEncapsulationKey (ek : MLKEM.EncapsulationKey (FIPS203.params ps) (FIPS203.encoding ps)) : Bool

Equations

• Cryptlib.Primitives.KEM.MLKEM768.checkEncapsulationKey = Cryptlib.Primitives.KEM.FIPS203.checkEncapsulationKey Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.checkDecapsulationKey (dk : MLKEM.DecapsulationKey (FIPS203.params ps) (FIPS203.encoding ps)) : Bool

Equations

• Cryptlib.Primitives.KEM.MLKEM768.checkDecapsulationKey = Cryptlib.Primitives.KEM.FIPS203.checkDecapsulationKey Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.Reliable (s : State) : Prop

Equations

• Cryptlib.Primitives.KEM.MLKEM768.Reliable = Cryptlib.Primitives.KEM.FIPS203.Reliable Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.encapM (pk : FIPS203.PublicKey ps) : EStateM KEM.KEMError State (FIPS203.CT ps × Vector UInt8 32)

Equations

• Cryptlib.Primitives.KEM.MLKEM768.encapM = Cryptlib.Primitives.KEM.FIPS203.encapM Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decapM (sk : FIPS203.PrivateKey ps) (c : FIPS203.CT ps) : EStateM KEM.KEMError State (Vector UInt8 32)

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decapM = Cryptlib.Primitives.KEM.FIPS203.decapM Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.derivePublicKeyM (sk : FIPS203.PrivateKey ps) : FIPS203.PublicKey ps

Equations

• Cryptlib.Primitives.KEM.MLKEM768.derivePublicKeyM = Cryptlib.Primitives.KEM.FIPS203.derivePublicKeyM Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.honestRoundTripM (sk : FIPS203.PrivateKey ps) (s : State) (hrel : FIPS203.Reliable ps s) (c : FIPS203.CT ps) (k : Vector UInt8 32) (s' : State) (hc : FIPS203.encapM ps (FIPS203.derivePublicKeyM ps sk) s = EStateM.Result.ok (c, k) s') (t : State) : ∃ (t' : State), FIPS203.decapM ps sk c t = EStateM.Result.ok k t'

Equations

• Cryptlib.Primitives.KEM.MLKEM768.honestRoundTripM = ⋯

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decodePrivateKey_totalM (v : Vector UInt8 (FIPS203.params ps).secretKeyBytes) : ∃ (sk : FIPS203.PrivateKey ps), FIPS203.decodePrivateKey ps v = some sk

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decodePrivateKey_totalM = ⋯

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.dummyPk : FIPS203.PublicKey ps

Equations

• Cryptlib.Primitives.KEM.MLKEM768.dummyPk = Cryptlib.Primitives.KEM.FIPS203.dummyPk Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.dummySk : FIPS203.PrivateKey ps

Equations

• Cryptlib.Primitives.KEM.MLKEM768.dummySk = Cryptlib.Primitives.KEM.FIPS203.dummySk Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.dummyCt : FIPS203.CT ps

Equations

• Cryptlib.Primitives.KEM.MLKEM768.dummyCt = Cryptlib.Primitives.KEM.FIPS203.dummyCt Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.derivePublicKeyFromSeed (sk : SeedPrivateKey) : FIPS203.PublicKey ps

Equations

• Cryptlib.Primitives.KEM.MLKEM768.derivePublicKeyFromSeed = Cryptlib.Primitives.KEM.FIPS203.derivePublicKeyFromSeed Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.expandSeed (sk : SeedPrivateKey) : FIPS203.PrivateKey ps

Equations

• Cryptlib.Primitives.KEM.MLKEM768.expandSeed = Cryptlib.Primitives.KEM.FIPS203.expandSeed Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decapMFromSeed (sk : SeedPrivateKey) (c : FIPS203.CT ps) : EStateM KEM.KEMError State (Vector UInt8 32)

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decapMFromSeed = Cryptlib.Primitives.KEM.FIPS203.decapMFromSeed Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.honestRoundTripFromSeed (sk : SeedPrivateKey) (s : State) : FIPS203.Reliable ps s → ∀ (c : FIPS203.CT ps) (k : Vector UInt8 32) (s' : State), FIPS203.encapM ps (FIPS203.derivePublicKeyFromSeed ps sk) s = EStateM.Result.ok (c, k) s' → ∀ (t : State), ∃ (t' : State), FIPS203.decapMFromSeed ps sk c t = EStateM.Result.ok k t'

Equations

• Cryptlib.Primitives.KEM.MLKEM768.honestRoundTripFromSeed = ⋯

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.encodePrivateKeyFromSeed (sk : SeedPrivateKey) : Vector UInt8 ((FIPS203.params ps).publicKeyBytes + 64)

Equations

• Cryptlib.Primitives.KEM.MLKEM768.encodePrivateKeyFromSeed = Cryptlib.Primitives.KEM.FIPS203.encodePrivateKeyFromSeed Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decodePrivateKeyFromSeed (v : Vector UInt8 ((FIPS203.params ps).publicKeyBytes + 64)) : Option SeedPrivateKey

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decodePrivateKeyFromSeed = Cryptlib.Primitives.KEM.FIPS203.decodePrivateKeyFromSeed Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decodePrivateKeyFromSeed_total (v : Vector UInt8 ((FIPS203.params ps).publicKeyBytes + 64)) : ∃ (sk : SeedPrivateKey), FIPS203.decodePrivateKeyFromSeed ps v = some sk

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decodePrivateKeyFromSeed_total = ⋯

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.decode_encode_privFromSeed (sk : SeedPrivateKey) : FIPS203.decodePrivateKeyFromSeed ps (FIPS203.encodePrivateKeyFromSeed ps sk) = some sk

Equations

• Cryptlib.Primitives.KEM.MLKEM768.decode_encode_privFromSeed = ⋯

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.kemMLKEM768 : KEM.KEM

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

Equations

• Cryptlib.Primitives.KEM.MLKEM768.kemMLKEM768 = Cryptlib.Primitives.KEM.FIPS203.kem Cryptlib.Primitives.KEM.MLKEM768.ps

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.MLKEM768.kemMLKEM768Seed : KEM.KEM

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

Equations

• Cryptlib.Primitives.KEM.MLKEM768.kemMLKEM768Seed = Cryptlib.Primitives.KEM.FIPS203.kemSeed Cryptlib.Primitives.KEM.MLKEM768.ps