PQXDH in Lean

Blueprint Summary🔗

Overview
Total entries66completed: 61; deps incomplete: 0; sorries: 5; no proof: 0
Ready now5Entries whose next formalization step is currently unblocked.
Fully closed61Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Current blockers5Missing external or incomplete Lean declarations.
Missing informal coverage7Entries with Lean code but missing an informal statement or proof block.
Current blockers (5)
Missing informal coverage (7)
Entry index (66)
Definitions55completed: 55; deps incomplete: 0; sorries: 0; no proof: 0
Theorems11completed: 6; deps incomplete: 0; sorries: 5; no proof: 0
Definition Index (55)
Theorem / Lemma / Corollary Index (11)
By parent groups (4)
Passive message secrecy game, DDH reduction, and tight security bound under the Random Oracle Model. (1)
Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024). (1)
PQXDH protocol definitions and roadmap from X3DH to full post-quantum security. (6)
Core X3DH definitions and end-to-end correctness results. (3)
Dependency insights
Statement-used entries12Entries reused in statement dependencies.
Proof-used entries3Entries reused in proof-only dependencies.
Tracked parent groups6Grouped health rollups for parents with more than one child entry.
Most used in statements (12)
  • kdf_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 8
    Associated lean decls (1)
  • x3dh_agree(Theorem)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 1direct uses: 4downstream unlocks: 9
    Associated lean decls (1)
  • dh_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
    Associated lean decls (1)
  • x3dh_session_key_agree(Theorem)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 8
    Associated lean decls (1)
  • aead_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
    Associated lean decls (1)
  • x3dh_handshake_correct(Theorem)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
    Associated lean decls (1)
  • ddh_reduction(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    Associated lean decls (1)
  • kdf_random_oracle(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    Associated lean decls (1)
  • kem_spec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    Associated lean decls (1)
  • peer_auth(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    Associated lean decls (1)
  • Show all 2 more statement-used entries
    • x3dh_alice(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • x3dh_bob(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
Most used in proofs (3)
  • x3dh_agree(Theorem)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 1statement uses: 3direct uses: 4downstream unlocks: 9
    Associated lean decls (1)
  • x3dh_session_key_agree(Theorem)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 8
    Associated lean decls (1)
  • passive_secrecy_advantage(Definition)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
    Associated lean decls (1)
Group health (6)
  • PQXDH protocol definitions and roadmap from X3DH to full post-quantum security.pqxdh_core
    Grouped view over entries sharing the same parent.
    total: 12closed: 7local-only: 0ready: 5blocked: 0incomplete Lean: 5unlock score: 0
    Next: no ready child currently unlocks downstream work.
  • Core X3DH definitions and end-to-end correctness results.x3dh_core
    Grouped view over entries sharing the same parent.
    total: 8closed: 8local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 27
    Next: no ready child currently unlocks downstream work.
  • Core interface for deterministic and random-oracle key derivation.kdf_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.
  • Formal security definitions and assumptions for PQXDH, following Bhargavan et al. (USENIX Security 2024).security_defs_core
    Grouped view over entries sharing the same parent.
    total: 22closed: 22local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 2
    Next: no ready child currently unlocks downstream work.
  • Passive message secrecy game, DDH reduction, and tight security bound under the Random Oracle Model.passive_secrecy_core
    Grouped view over entries sharing the same parent.
    total: 7closed: 7local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 2
    Next: no ready child currently unlocks downstream work.
  • Custom tactic for automatic distributional equivalence proofs.perm_draws_core
    Grouped view over entries sharing the same parent.
    total: 12closed: 12local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 0
    Next: no ready child currently unlocks downstream work.
Metadata
Tags in use16Distinct tags currently attached to blueprint entries.
Tag rollups (16)
  • tag: pqxdh
    entries: 6actionable: 0quick wins: 0linked PRs: 0
  • tag: security
    entries: 5actionable: 0quick wins: 0linked PRs: 0
  • tag: agreement
    entries: 4actionable: 0quick wins: 0linked PRs: 0
  • tag: x3dh
    entries: 4actionable: 0quick wins: 0linked PRs: 0
  • tag: classical
    entries: 2actionable: 0quick wins: 0linked PRs: 0
  • tag: kem
    entries: 2actionable: 0quick wins: 0linked PRs: 0
  • tag: aead
    entries: 1actionable: 0quick wins: 0linked PRs: 0
  • tag: auth
    entries: 1actionable: 0quick wins: 0linked PRs: 0
  • tag: ddh
    entries: 1actionable: 0quick wins: 0linked PRs: 0
  • tag: handshake
    entries: 1actionable: 0quick wins: 0linked PRs: 0
  • Show all 6 more tags
    • tag: kdf
      entries: 1actionable: 0quick wins: 0linked PRs: 0
    • tag: postquantum
      entries: 1actionable: 0quick wins: 0linked PRs: 0
    • tag: pq
      entries: 1actionable: 0quick wins: 0linked PRs: 0
    • tag: rom
      entries: 1actionable: 0quick wins: 0linked PRs: 0
    • tag: sh-cr
      entries: 1actionable: 0quick wins: 0linked PRs: 0
    • tag: symbolic
      entries: 1actionable: 0quick wins: 0linked PRs: 0
Metadata audit
Missing owner66
Missing effort55
Untagged55
Missing owner (66)
Missing effort (55)
Untagged (55)
Structure and coverage
Ready to formalize5Entries whose next step is currently unblocked.
Fully closed61Local code and ancestor closure are both complete.
Heaviest prerequisites (14)
  • x3dh_handshake_correct(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 1direct uses: 1downstream unlocks: 8
    Associated lean decls (1)
  • x3dh_session_key_agree(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 1direct uses: 3downstream unlocks: 8
    Associated lean decls (1)
  • passive_secrecy_le_ddh(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 1proof deps: 1direct uses: 0downstream unlocks: 0
    Associated lean decls (1)
  • kdf_spec(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 8
    Associated lean decls (1)
  • pqxdh_agree(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    Associated lean decls (1)
  • x3dh_sk_alice(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    Associated lean decls (1)
  • x3dh_sk_bob(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    Associated lean decls (1)
  • aead_spec(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 8
    Associated lean decls (1)
  • kem_internal_hash_rom(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    Associated lean decls (1)
  • peer_auth_pq(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    Associated lean decls (1)
  • Show all 4 more heaviest-prerequisite entries
    • pqxdh_sk_alice(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
      Associated lean decls (1)
    • pqxdh_sk_bob(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
      Associated lean decls (1)
    • x3dh_agree(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 9
      Associated lean decls (1)
    • x3dh_keypair(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
      Associated lean decls (1)
No prerequisites (52)
No dependents (53)
Proof debt hotspots (1)
  • PQXDH protocol definitions and roadmap from X3DH to full post-quantum security.pqxdh_core
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 5incomplete decls: 5missing decls: 0total debt: 5