inductive Cryptlib.Primitives.KEM.KEM.KEMError : Type

• badCiphertext : KEMError
• unsafePublicKey : KEMError

@[instance_reducible]

instance Cryptlib.Primitives.KEM.KEM.instDecidableEqKEMError : DecidableEq KEMError

Equations

• Cryptlib.Primitives.KEM.KEM.instDecidableEqKEMError x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Cryptlib.Primitives.KEM.KEM.KEM : Type 1

• State : Type
• PublicKey : Type
• PrivateKey : Type
• Ciphertext : Type
• Plaintext : Type
• pubI : Inhabited self.PublicKey
• privI : Inhabited self.PrivateKey
• ctI : Inhabited self.Ciphertext
• ptI : Inhabited self.Plaintext
• stateI : Inhabited self.State

  Inhabitance witness only; never run a scheme against stateI.default.

• publicKeySize : Nat
• privateKeySize : Nat
• ciphertextSize : Nat
• plaintextSize : Nat
• encodePublicKey : self.PublicKey → Vector UInt8 self.publicKeySize
• decodePublicKey : Vector UInt8 self.publicKeySize → Option self.PublicKey
• encodePrivateKey : self.PrivateKey → Vector UInt8 self.privateKeySize
• decodePrivateKey : Vector UInt8 self.privateKeySize → Option self.PrivateKey
• encodeCiphertext : self.Ciphertext → Vector UInt8 self.ciphertextSize
• decodeCiphertext : Vector UInt8 self.ciphertextSize → Option self.Ciphertext
• encodePlaintext : self.Plaintext → Vector UInt8 self.plaintextSize
• decap : self.PrivateKey → self.Ciphertext → EStateM KEMError self.State self.Plaintext
• encap : self.PublicKey → EStateM KEMError self.State (self.Ciphertext × self.Plaintext)
• Reliable : self.State → Prop

  Pre-encapsulation states that cannot cause a decryption failure. True for a perfectly correct KEM; a lattice KEM restricts it to states whose sampled noise stays within bounds.

• generate : EStateM KEMError self.State ((pk : self.PublicKey) ×' { sk : self.PrivateKey // ∀ (s : self.State), self.Reliable s → ∀ (c : self.Ciphertext) (k : self.Plaintext) (s' : self.State), self.encap pk s = EStateM.Result.ok (c, k) s' → ∀ (t : self.State), ∃ (t' : self.State), self.decap sk c t = EStateM.Result.ok k t' })
• stateFromSeed : Vector UInt8 32 → self.State

  Deterministic state from a 32-byte seed.

• derivePublicKey : self.PrivateKey → self.PublicKey
• honestRoundTrip (sk : self.PrivateKey) (s : self.State) : self.Reliable s → ∀ (c : self.Ciphertext) (k : self.Plaintext) (s' : self.State), self.encap (self.derivePublicKey sk) s = EStateM.Result.ok (c, k) s' → ∀ (t : self.State), ∃ (t' : self.State), self.decap sk c t = EStateM.Result.ok k t'

  Round trip for any private key and its derived public key, from a Reliable state.

• decodePrivateKey_total (b : Vector UInt8 self.privateKeySize) : ∃ (sk : self.PrivateKey), self.decodePrivateKey b = some sk

  Every byte string of the right width decodes to a private key.

• decode_encode_pub (pk : self.PublicKey) : self.decodePublicKey (self.encodePublicKey pk) = some pk
• decode_encode_priv (sk : self.PrivateKey) : self.decodePrivateKey (self.encodePrivateKey sk) = some sk
• decode_encode_ct (c : self.Ciphertext) : self.decodeCiphertext (self.encodeCiphertext c) = some c
• plaintextEq : DecidableEq self.Plaintext

@[instance_reducible]

instance Cryptlib.Primitives.KEM.KEM.instInhabitedKEM : Inhabited KEM

Equations

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

@[instance_reducible]

instance Cryptlib.Primitives.KEM.KEM.instInhabitedState (kemSpec : KEM) : Inhabited kemSpec.State

Equations

• Cryptlib.Primitives.KEM.KEM.instInhabitedState kemSpec = kemSpec.stateI

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.KEM.KEMM (kemSpec : KEM) (α : Type) : Type

Equations

• Cryptlib.Primitives.KEM.KEM.KEMM kemSpec = EStateM Cryptlib.Primitives.KEM.KEM.KEMError kemSpec.State

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.KEM.PublicKey (kemSpec : KEM) : Type

Equations

• Cryptlib.Primitives.KEM.KEM.PublicKey kemSpec = kemSpec.PublicKey

@[instance_reducible]

instance Cryptlib.Primitives.KEM.KEM.instInhabitedPublicKey (kemSpec : KEM) : Inhabited (PublicKey kemSpec)

Equations

• Cryptlib.Primitives.KEM.KEM.instInhabitedPublicKey kemSpec = kemSpec.pubI

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.KEM.PrivateKey (kemSpec : KEM) : Type

Equations

• Cryptlib.Primitives.KEM.KEM.PrivateKey kemSpec = kemSpec.PrivateKey

@[instance_reducible]

instance Cryptlib.Primitives.KEM.KEM.instInhabitedPrivateKey (kemSpec : KEM) : Inhabited (PrivateKey kemSpec)

Equations

• Cryptlib.Primitives.KEM.KEM.instInhabitedPrivateKey kemSpec = kemSpec.privI

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.KEM.Ciphertext (kemSpec : KEM) : Type

Equations

• Cryptlib.Primitives.KEM.KEM.Ciphertext kemSpec = kemSpec.Ciphertext

@[instance_reducible]

instance Cryptlib.Primitives.KEM.KEM.instInhabitedCiphertext (kemSpec : KEM) : Inhabited (Ciphertext kemSpec)

Equations

• Cryptlib.Primitives.KEM.KEM.instInhabitedCiphertext kemSpec = kemSpec.ctI

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.KEM.Plaintext (kemSpec : KEM) : Type

Equations

• Cryptlib.Primitives.KEM.KEM.Plaintext kemSpec = kemSpec.Plaintext

@[instance_reducible]

instance Cryptlib.Primitives.KEM.KEM.instInhabitedPlaintext (kemSpec : KEM) : Inhabited (Plaintext kemSpec)

Equations

• Cryptlib.Primitives.KEM.KEM.instInhabitedPlaintext kemSpec = kemSpec.ptI

@[instance_reducible]

instance Cryptlib.Primitives.KEM.KEM.instDecidableEqPlaintext (kemSpec : KEM) : DecidableEq (Plaintext kemSpec)

Equations

• Cryptlib.Primitives.KEM.KEM.instDecidableEqPlaintext kemSpec = kemSpec.plaintextEq

def Cryptlib.Primitives.KEM.KEM.generate (kemSpec : KEM) : KEMM kemSpec (PublicKey kemSpec × PrivateKey kemSpec)

Equations

• Cryptlib.Primitives.KEM.KEM.generate kemSpec = do let __x ← kemSpec.generate match __x with | ⟨pk, ⟨sk, property⟩⟩ => pure (pk, sk)

def Cryptlib.Primitives.KEM.KEM.encap (kemSpec : KEM) : PublicKey kemSpec → KEMM kemSpec (Ciphertext kemSpec × Plaintext kemSpec)

Equations

• Cryptlib.Primitives.KEM.KEM.encap kemSpec = kemSpec.encap

def Cryptlib.Primitives.KEM.KEM.decap (kemSpec : KEM) : PrivateKey kemSpec → Ciphertext kemSpec → KEMM kemSpec (Plaintext kemSpec)

Equations

• Cryptlib.Primitives.KEM.KEM.decap kemSpec = kemSpec.decap

def Cryptlib.Primitives.KEM.KEM.IsEncapsulation (kemSpec : KEM) (sk : PrivateKey kemSpec) (c : Ciphertext kemSpec) (k : Plaintext kemSpec) : Prop

Equations

• Cryptlib.Primitives.KEM.KEM.IsEncapsulation kemSpec sk c k = ∀ (t : kemSpec.State), ∃ (t' : kemSpec.State), Cryptlib.Primitives.KEM.KEM.decap kemSpec sk c t = EStateM.Result.ok k t'

def Cryptlib.Primitives.KEM.KEM.KeyPair (kemSpec : KEM) (pk : PublicKey kemSpec) (sk : PrivateKey kemSpec) : Prop

Equations

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

theorem Cryptlib.Primitives.KEM.KEM.EStateM_triple_ok {ε σ α : Type u_1} {p : α → Prop} {x : EStateM ε σ α} (h : ∀ (t : σ) (a : α) (t' : σ), x t = EStateM.Result.ok a t' → p a) : ⦃⌜True⌝⦄ x ⦃(fun (a : α) => ⌜p a⌝, fun (x : ε) => ⌜True⌝, PUnit.unit)⦄

Partial-correctness triple: if x returns, its result satisfies p.

theorem Cryptlib.Primitives.KEM.KEM.EStateM_triple {ε σ α : Type u_1} {p : α → Prop} {x : EStateM ε σ α} (h : ∀ (t : σ), ∃ (a : α), ∃ (t' : σ), x t = EStateM.Result.ok a t' ∧ p a) : ⦃⌜True⌝⦄ x ⦃(fun (a : α) => ⌜p a⌝, fun (x : ε) => ⌜False⌝, PUnit.unit)⦄

Total-correctness triple: x always returns a result satisfying p.

theorem Cryptlib.Primitives.KEM.KEM.generate_keyPair (kemSpec : KEM) {t : kemSpec.State} {r : PublicKey kemSpec × PrivateKey kemSpec} {t' : kemSpec.State} (hr : generate kemSpec t = EStateM.Result.ok r t') : KeyPair kemSpec r.fst r.snd

Whatever generate returns is a valid key pair.

theorem Cryptlib.Primitives.KEM.KEM.generate_ok (kemSpec : KEM) : ⦃⌜True⌝⦄ generate kemSpec ⦃(fun (x : PublicKey kemSpec × PrivateKey kemSpec) => match x with | (pk, sk) => ⌜KeyPair kemSpec pk sk⌝, fun (x : KEMError) => ⌜True⌝, PUnit.unit)⦄

theorem Cryptlib.Primitives.KEM.KEM.encap_ok (kemSpec : KEM) {pk : PublicKey kemSpec} {sk : PrivateKey kemSpec} (h : KeyPair kemSpec pk sk) (t : kemSpec.State) (hrel : kemSpec.Reliable t) (r : Ciphertext kemSpec × Plaintext kemSpec) (t' : kemSpec.State) : encap kemSpec pk t = EStateM.Result.ok r t' → IsEncapsulation kemSpec sk r.fst r.snd

Encapsulation from a Reliable state to a valid key pair decapsulates correctly. Stated as a plain proposition because the precondition constrains the starting state.

theorem Cryptlib.Primitives.KEM.KEM.decap_ok (kemSpec : KEM) {sk : PrivateKey kemSpec} {ct : Ciphertext kemSpec} {k : Plaintext kemSpec} (h : IsEncapsulation kemSpec sk ct k) : ⦃⌜True⌝⦄ decap kemSpec sk ct ⦃(fun (k' : Plaintext kemSpec) => ⌜k' = k⌝, fun (x : KEMError) => ⌜False⌝, PUnit.unit)⦄