Secure Messaging

Blueprint Summary🔗

Overview
Total entries138completed: 57; deps incomplete: 0; sorries: 0; no proof: 48
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed57Local code and prerequisite closure are both complete.
Actionable priorities11Entries ready now and already unlocking downstream work.
Missing informal coverage15Entries with Lean code but missing an informal statement or proof block.
Ready next (11)
  • rkem_scheme(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 24downstream unlocks: 30
  • prf_prng_scheme(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 9downstream unlocks: 26
  • fs_aead_scheme(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 8downstream unlocks: 24
  • secure_messaging_double_ratchet_scheme(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 5downstream unlocks: 14
  • secure_messaging_scka_scheme(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 5
  • secure_messaging_triple_ratchet_scheme(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 5
  • spqr_chunked_spec(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 3
  • cka_from_lwe_spec(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 2
  • frodo_kem_scheme(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 2
  • mlkem_braid_spec(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 2
  • Show all 1 more priorities
    • opp_bikem_cka_spec(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 2
Missing informal coverage (15)
Entry index (138)
Definitions75completed: 42; deps incomplete: 0; sorries: 0; no proof: 0
Theorems63completed: 15; deps incomplete: 0; sorries: 0; no proof: 48
Informal-only entries81
Definition Index (75)
Theorem / Proposition / Lemma / Corollary Index (63)
By parent groups (26)
Module-Lattice Key Encapsulation Mechanism (ML-KEM, FIPS 203). (3)
CKA from KEM. (2)
Reed–Solomon erasure codes over arbitrary fields. (1)
The 16-coordinate parallel Reed–Solomon construction and its SPQR specialization. (2)
PRF-PRNG from PRP and PRG. (1)
Sparse Post-Quantum Ratchet (SPQR) ( ). (2)
RKEM from DDH (FS). (3)
CKA from DDH. (2)
FrodoKEM, a Learning-With-Errors key encapsulation mechanism ( ). (2)
Opp-UniKEM-CKA. (2)
Triple Ratchet SM. (4)
Katana RKEM (optimised). (3)
Double Ratchet SM - Signal. (4)
Opp-RKEM-CKA. (2)
Katana RKEM (plain). (3)
Encrypt-then-MAC. (2)
ML-KEM Braid ( ). (2)
Double Ratchet SM - Abstract. (4)
Incremental KEM from ML-KEM. (1)
Opp-BiKEM-CKA. (2)
FS-AEAD from AEAD and PRG. (2)
RKEM from KEM. (3)
CKA from LWE. (2)
SCKA SM. (4)
RKEM from DDH (non-FS). (2)
GCM. (2)
Dependency insights
Statement-used entries86Entries reused in statement dependencies.
Tracked parent groups36Grouped health rollups for parents with more than one child entry.
Most used in statements (86)
Group health (36)
  • Ratcheting Key Encapsulation Mechanism (RKEM).rkem
    Grouped view over entries sharing the same parent.
    total: 4closed: 0local-only: 0ready: 1blocked: 3incomplete Lean: 0unlock score: 47
    Next: rkem_scheme stage: statementdownstream unlocks: 30
  • Pseudorandom Function-Generator (PRF-PRNG).prf_prng
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 0ready: 1blocked: 1incomplete Lean: 0unlock score: 28
    Next: prf_prng_scheme stage: statementdownstream unlocks: 26
  • Forward-Secure AEAD (FS-AEAD).fs_aead
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 0ready: 1blocked: 1incomplete Lean: 0unlock score: 25
    Next: fs_aead_scheme stage: statementdownstream unlocks: 24
  • Double Ratchet.secure_messaging_double_ratchet
    Grouped view over entries sharing the same parent.
    total: 5closed: 0local-only: 0ready: 1blocked: 4incomplete Lean: 0unlock score: 17
    Next: secure_messaging_double_ratchet_scheme stage: statementdownstream unlocks: 14
  • SCKA SM.secure_messaging_scka
    Grouped view over entries sharing the same parent.
    total: 6closed: 0local-only: 0ready: 1blocked: 5incomplete Lean: 0unlock score: 12
    Next: secure_messaging_scka_scheme stage: statementdownstream unlocks: 5
  • Triple Ratchet SM.secure_messaging_triple_ratchet
    Grouped view over entries sharing the same parent.
    total: 6closed: 0local-only: 0ready: 1blocked: 5incomplete Lean: 0unlock score: 12
    Next: secure_messaging_triple_ratchet_scheme stage: statementdownstream unlocks: 5
  • Module-Lattice Key Encapsulation Mechanism (ML-KEM, FIPS 203).ml_kem
    Grouped view over entries sharing the same parent.
    total: 5closed: 4local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 8
    Next: no ready child currently unlocks downstream work.
  • ML-KEM Braid ( ).cka_protocols_mlkem_braid
    Grouped view over entries sharing the same parent.
    total: 4closed: 1local-only: 0ready: 1blocked: 2incomplete Lean: 0unlock score: 5
    Next: mlkem_braid_spec stage: statementdownstream unlocks: 2
  • CKA from LWE.cka_cka_from_lwe
    Grouped view over entries sharing the same parent.
    total: 3closed: 0local-only: 0ready: 1blocked: 2incomplete Lean: 0unlock score: 2
    Next: cka_from_lwe_spec stage: statementdownstream unlocks: 2
  • FrodoKEM, a Learning-With-Errors key encapsulation mechanism ( ).frodo_kem
    Grouped view over entries sharing the same parent.
    total: 3closed: 0local-only: 0ready: 1blocked: 2incomplete Lean: 0unlock score: 2
    Next: frodo_kem_scheme stage: statementdownstream unlocks: 2
  • Show all 26 more groups
    • GCM.aead_gcm
      Grouped view over entries sharing the same parent.
      total: 3closed: 2local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 2
      Next: no ready child currently unlocks downstream work.
    • Opp-BiKEM-CKA.cka_protocols_opp_bikem_cka
      Grouped view over entries sharing the same parent.
      total: 3closed: 0local-only: 0ready: 1blocked: 2incomplete Lean: 0unlock score: 2
      Next: opp_bikem_cka_spec stage: statementdownstream unlocks: 2
    • Opp-UniKEM-CKA.cka_protocols_opp_unikem_cka
      Grouped view over entries sharing the same parent.
      total: 3closed: 2local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 2
      Next: no ready child currently unlocks downstream work.
    • SCKA.cka_protocols_scka
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 47
      Next: no ready child currently unlocks downstream work.
    • Erasure Codes.erasure_codes
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 43
      Next: no ready child currently unlocks downstream work.
    • Online-Offline Key Encapsulation Mechanism (On-Off KEM).on_off_kem
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 22
      Next: no ready child currently unlocks downstream work.
    • Double Ratchet SM - Abstract.secure_messaging_abstract_protocol_double_ratchet
      Grouped view over entries sharing the same parent.
      total: 5closed: 0local-only: 0ready: 0blocked: 5incomplete Lean: 0unlock score: 18
      Next: no ready child currently unlocks downstream work.
    • Incremental Key Encapsulation Mechanism (Incremental KEM).incremental_kem
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 12
      Next: no ready child currently unlocks downstream work.
    • On-Off KEM from K-PKE.on_off_kem_from_kpke
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 9
      Next: no ready child currently unlocks downstream work.
    • Unchunked SPQR core.spqr_unchunked_core
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 8
      Next: no ready child currently unlocks downstream work.
    • Double Ratchet SM - Signal.secure_messaging_signal_protocol_double_ratchet
      Grouped view over entries sharing the same parent.
      total: 5closed: 0local-only: 0ready: 0blocked: 5incomplete Lean: 0unlock score: 7
      Next: no ready child currently unlocks downstream work.
    • Reed–Solomon erasure codes over arbitrary fields.erasure_codes_reed_solomon
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 7
      Next: no ready child currently unlocks downstream work.
    • CKA from DDH.cka_cka_from_ddh
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 5
      Next: no ready child currently unlocks downstream work.
    • The 16-coordinate parallel Reed–Solomon construction and its SPQR specialization.erasure_codes_spqr_reed_solomon
      Grouped view over entries sharing the same parent.
      total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 5
      Next: no ready child currently unlocks downstream work.
    • Katana RKEM (optimised).rkem_katana_rkem_optimised
      Grouped view over entries sharing the same parent.
      total: 4closed: 0local-only: 0ready: 0blocked: 4incomplete Lean: 0unlock score: 3
      Next: no ready child currently unlocks downstream work.
    • Katana RKEM (plain).rkem_katana_rkem_plain
      Grouped view over entries sharing the same parent.
      total: 4closed: 0local-only: 0ready: 0blocked: 4incomplete Lean: 0unlock score: 3
      Next: no ready child currently unlocks downstream work.
    • RKEM from DDH (FS).rkem_rkem_from_ddh_fs
      Grouped view over entries sharing the same parent.
      total: 4closed: 0local-only: 0ready: 0blocked: 4incomplete Lean: 0unlock score: 3
      Next: no ready child currently unlocks downstream work.
    • RKEM from KEM.rkem_rkem_from_kem
      Grouped view over entries sharing the same parent.
      total: 4closed: 0local-only: 0ready: 0blocked: 4incomplete Lean: 0unlock score: 3
      Next: no ready child currently unlocks downstream work.
    • CKA from KEM.cka_cka_from_kem
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 2
      Next: no ready child currently unlocks downstream work.
    • Encrypt-then-MAC.aead_encrypt_then_mac
      Grouped view over entries sharing the same parent.
      total: 3closed: 3local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 2
      Next: no ready child currently unlocks downstream work.
    • FS-AEAD from AEAD and PRG.fs_aead_fs_aead_from_aead_prg
      Grouped view over entries sharing the same parent.
      total: 3closed: 0local-only: 0ready: 0blocked: 3incomplete Lean: 0unlock score: 2
      Next: no ready child currently unlocks downstream work.
    • Opp-RKEM-CKA.cka_protocols_opp_rkem_cka
      Grouped view over entries sharing the same parent.
      total: 3closed: 0local-only: 0ready: 0blocked: 3incomplete Lean: 0unlock score: 2
      Next: no ready child currently unlocks downstream work.
    • RKEM from DDH (non-FS).rkem_rkem_from_ddh_non_fs
      Grouped view over entries sharing the same parent.
      total: 3closed: 0local-only: 0ready: 0blocked: 3incomplete Lean: 0unlock score: 2
      Next: no ready child currently unlocks downstream work.
    • Sparse Post-Quantum Ratchet (SPQR) ( ).cka_protocols_spqr
      Grouped view over entries sharing the same parent.
      total: 3closed: 0local-only: 0ready: 0blocked: 3incomplete Lean: 0unlock score: 2
      Next: no ready child currently unlocks downstream work.
    • Incremental KEM from ML-KEM.incremental_kem_incremental_kem_from_ml_kem
      Grouped view over entries sharing the same parent.
      total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 2
      Next: no ready child currently unlocks downstream work.
    • PRF-PRNG from PRP and PRG.prf_prng_prf_prng_from_prp_prg
      Grouped view over entries sharing the same parent.
      total: 2closed: 0local-only: 0ready: 0blocked: 2incomplete Lean: 0unlock score: 1
      Next: no ready child currently unlocks downstream work.
Metadata
Metadata audit
Missing owner138
Missing effort138
Untagged138
Missing owner (138)
Missing effort (138)
Untagged (138)
Structure and coverage
Informal-only81Statements with no associated Lean code yet.
Fully closed57Local code and ancestor closure are both complete.
Heaviest prerequisites (124)
No prerequisites (14)
No dependents (52)