Symbolic/Specifications/Model/EquationalTheory/Kem.lean

class kemPkL27–33 ↗#

public
class CanPQKem.{u} (Bytes: Type u) where
  kemPk: (sk: Bytes) → Bytes
  kemEncap: (pk: Bytes) → (entropy: Bytes) → Bytes × Bytes
  kemDecap: (sk: Bytes) → (cipher: Bytes) → Err Bytes
  /-- Kyber-1024 implicit-rejection key derived from `sk` and `cipher`. -/
  kemRejKey: (sk: Bytes) → (cipher: Bytes) → Bytes

structure SubFL39–41 ↗#

1568-byte KEM public key kemPk sk.

public structure SubF (Bytes: Type) where
  sk: Bytes

instanceL43 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .unary SubF.sk

instanceL44 ↗#

public instance: SubBytesFunctor SubF := .unary SubF.sk SubF.mk

def SubF.lengthL45 ↗#

@[expose] public def SubF.length [BytesFunctor]: Bytes.PartialLength SubF := fun _ _ => 1568

structure SubFL51–54 ↗#

1568-byte KEM ciphertext encapsulated to pk with randomness entropy.

public structure SubF (Bytes: Type) where
  pk: Bytes
  entropy: Bytes

instanceL56 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .binary SubF.pk SubF.entropy

instanceL57 ↗#

public instance: SubBytesFunctor SubF := .binary SubF.pk SubF.entropy SubF.mk

def SubF.lengthL58 ↗#

@[expose] public def SubF.length [BytesFunctor]: Bytes.PartialLength SubF := fun _ _ => 1568

structure SubFL64–67 ↗#

32-byte KEM shared secret bound to pk and entropy.

public structure SubF (Bytes: Type) where
  pk: Bytes
  entropy: Bytes

instanceL69 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .binary SubF.pk SubF.entropy

instanceL70 ↗#

public instance: SubBytesFunctor SubF := .binary SubF.pk SubF.entropy SubF.mk

def SubF.lengthL71 ↗#

@[expose] public def SubF.length [BytesFunctor]: Bytes.PartialLength SubF := fun _ _ => 32

structure SubFL77–81 ↗#

32-byte Kyber-1024 implicit-rejection key derived from sk and cipher.

public
structure SubF (Bytes: Type) where
  sk: Bytes
  cipher: Bytes

instanceL83–85 ↗#

public
instance: ALaCarte.FunctorSizeOf SubF where
  sizeOf | {sk, cipher} => sizeOf sk + sizeOf cipher

instanceL87–97 ↗#

public
instance: ALaCarte.Representable SubF where
  CtorId := Unit
  ctors | () => { Data := Unit, nRec := 2 }
  toRepr | {sk, cipher} => { id := (), data := (), as := #v[sk, cipher] }
  fromRepr
  | {id, data, as} => { sk := as[0], cipher := as[1] }
  from_to | {sk, cipher} =>a✝:Typesk:a✝cipher:a✝⊢ (match
    match { sk := sk, cipher := cipher } with
    | { sk := sk, cipher := cipher } => { id := (), data := (), as := #v[sk, cipher] } with
  | { id := id, data := data, as := as } => { sk := as[0], cipher := as[1] }) =
  { sk := sk, cipher := cipher } bya✝:Typesk:a✝cipher:a✝⊢ (match
    match { sk := sk, cipher := cipher } with
    | { sk := sk, cipher := cipher } => { id := (), data := (), as := #v[sk, cipher] } with
  | { id := id, data := data, as := as } => { sk := as[0], cipher := as[1] }) =
  { sk := sk, cipher := cipher } rflAll goals completed! 🐙
  to_from
  | {id, data, as} =>a✝:Typeid:Unitdata:{ Data := Unit, nRec := 2 }.Dataas:Vector a✝ { Data := Unit, nRec := 2 }.nRec⊢ (match
    match { id := id, data := data, as := as } with
    | { id := id, data := data, as := as } => { sk := as[0], cipher := as[1] } with
  | { sk := sk, cipher := cipher } => { id := (), data := (), as := #v[sk, cipher] }) =
  { id := id, data := data, as := as } bya✝:Typeid:Unitdata:{ Data := Unit, nRec := 2 }.Dataas:Vector a✝ { Data := Unit, nRec := 2 }.nRec⊢ (match
    match { id := id, data := data, as := as } with
    | { id := id, data := data, as := as } => { sk := as[0], cipher := as[1] } with
  | { sk := sk, cipher := cipher } => { id := (), data := (), as := #v[sk, cipher] }) =
  { id := id, data := data, as := as } simp_alla✝:Typeid:Unitdata:{ Data := Unit, nRec := 2 }.Dataas:Vector a✝ { Data := Unit, nRec := 2 }.nRec⊢ #[as[0], as[1]] = as.toArray <;>a✝:Typeid:Unitdata:{ Data := Unit, nRec := 2 }.Dataas:Vector a✝ { Data := Unit, nRec := 2 }.nRec⊢ #[as[0], as[1]] = as.toArray grindAll goals completed! 🐙
  sizeOf_eq | {sk, cipher} =>a✝:Typeinst✝:SizeOf a✝sk:a✝cipher:a✝⊢ ALaCarte.FunctorSizeOf.sizeOf { sk := sk, cipher := cipher } =
  ALaCarte.FunctorSizeOf.sizeOf
    (match { sk := sk, cipher := cipher } with
    | { sk := sk, cipher := cipher } => { id := (), data := (), as := #v[sk, cipher] }) bya✝:Typeinst✝:SizeOf a✝sk:a✝cipher:a✝⊢ ALaCarte.FunctorSizeOf.sizeOf { sk := sk, cipher := cipher } =
  ALaCarte.FunctorSizeOf.sizeOf
    (match { sk := sk, cipher := cipher } with
    | { sk := sk, cipher := cipher } => { id := (), data := (), as := #v[sk, cipher] }) simp +arith [ALaCarte.FunctorSizeOf.sizeOf]All goals completed! 🐙

instanceL99 ↗#

public instance: ALaCarte.RepresentableDecidableEq SubF where

instanceL100 ↗#

public instance: ALaCarte.RepresentableOrd SubF where

instanceL101 ↗#

public instance: SubBytesFunctor SubF where

def SubF.lengthL103–105 ↗#

@[expose] public
def SubF.length [BytesFunctor]: Bytes.PartialLength SubF :=
  fun _ _ => 32

#combineL109–113 ↗#

#combine into BytesFunctor, BytesLength from
  Pk,
  Encap,
  SharedSecret,
  RejKey,

abbrev Pk.SubF.packL117 ↗#

public abbrev Pk.SubF.pack (x: Pk.SubF Bytes) := BytesView.pack x

abbrev Encap.SubF.packL118 ↗#

public abbrev Encap.SubF.pack (x: Encap.SubF Bytes) := BytesView.pack x

abbrev SharedSecret.SubF.packL119 ↗#

public abbrev SharedSecret.SubF.pack (x: SharedSecret.SubF Bytes) := BytesView.pack x

abbrev RejKey.SubF.packL120 ↗#

public abbrev RejKey.SubF.pack (x: RejKey.SubF Bytes) := BytesView.pack x

instanceL122–138 ↗#

public
instance: CanPQKem Bytes where
  kemPk sk := ({sk}: Pk.SubF Bytes).pack

  kemEncap pk entropy :=
    (({pk, entropy}: Encap.SubF Bytes).pack, ({pk, entropy}: SharedSecret.SubF Bytes).pack)

  kemDecap sk cipher :=
    match cipher.view? Encap.SubF with
    | some { pk, entropy } =>
      match pk.view? Pk.SubF with
      | some { sk := sk' } =>
        if sk = sk' then some ({pk, entropy}: SharedSecret.SubF Bytes).pack else none
      | none => none
    | none => none

  kemRejKey sk cipher := ({sk, cipher}: RejKey.SubF Bytes).pack

def invertKemPublicKeyL140–145 ↗#

Extracts sk from a kemPk sk term. Used only by the PQXDH state machine after BrokenKEM.

@[expose] public
def invertKemPublicKey (pk: Bytes): Err Bytes :=
  match pk.view? Pk.SubF with
  | some { sk } => some sk
  | none => none

def kemPk.attackerKnowledgeL147–149 ↗#

@[expose] public
def kemPk.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ sk, out = kemPk sk ∧ p sk

def kemEncapCipher.attackerKnowledgeL151–153 ↗#

@[expose] public
def kemEncapCipher.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ pk entropy rhs, (out, rhs) = kemEncap pk entropy ∧ p pk ∧ p entropy

def kemEncapSS.attackerKnowledgeL155–157 ↗#

@[expose] public
def kemEncapSS.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ pk entropy lhs, (lhs, out) = kemEncap pk entropy ∧ p pk ∧ p entropy

def kemDecap.attackerKnowledgeL159–161 ↗#

@[expose] public
def kemDecap.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ sk cipher, some out = kemDecap sk cipher ∧ p sk ∧ p cipher

def kemRejKey.attackerKnowledgeL163–165 ↗#

@[expose] public
def kemRejKey.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ sk cipher, out = kemRejKey sk cipher ∧ p sk ∧ p cipher

#combineL167–175 ↗#

#combine [BytesFunctor.Has SubF] into attackerKnowledge' from
  kemPk,
  kemEncapCipher,
  kemEncapSS,
  kemDecap,
  kemRejKey,

AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level

Kem.lean🔗