mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-03 19:53:43 +00:00
mrwulf
1086a3ba02
The 14-notebook course predated the post-quantum campaign entirely (coherence findings 10, 11). Now, authored in the GENERATOR and regenerated (AGENTS.md rule): - notebook 06: new section 'The second signature that actually shipped: SLH-DSA' — the deterministic co-signature since tree size 14, chosen because the log attests its own parameter set's verify path (leaf 18, 11 certs); absent-not-failed for older heads; determinism as an audit primitive; verify-only always. Plus a runnable keygen/sign/verify/ re-sign-byte-equality demo (honest skip below OpenSSL 3.5) and the --slhdsa-public-key consumer flag in the policy list. - notebook 09: the 'post-quantum line' is now three-legged — Ed25519 proven-verify dogfood, SLH-DSA shipped-and-attested, ML-DSA required- but-honest-unavailable — with the closing point that a slot stops being aspirational the day its verify path enters the log; stale 16/16 provenance count -> 44/44 (leaf 13 re-attestation). - notebook 07: policy exercise extended with the co-signature question; 00 course map goal updated; README course listing for 06/09. - GENERATOR DRIFT REPAIRED in passing: notebook 10's cockpit cell had been added to the .ipynb but never backported to the generator — regeneration would have silently dropped it; the cell is now IN the generator and round-trips (19 cells, content identical). Suite 157 green.
332 lines
15 KiB
Text
332 lines
15 KiB
Text
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"# Lecture 6: Merkle Transparency Logs\n",
|
|
"\n",
|
|
"Transparency logs make signed statements auditable. PACTA uses an RFC 9162-style Merkle accumulator over signed proof-check attestations. A provider signs the tree head, and an agent verifies an inclusion proof before acting on the attestation.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Learning Objectives\n",
|
|
"\n",
|
|
"- Implement leaf and node hashing with domain separation.\n",
|
|
"- Compute a Merkle root.\n",
|
|
"- Generate and verify inclusion proofs.\n",
|
|
"- Generate and verify consistency proofs.\n",
|
|
"- Explain Signed Tree Heads and signature policy.\n",
|
|
"- Explain why ML-DSA must fail closed when unavailable.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## RFC 9162 Hash Shape\n",
|
|
"\n",
|
|
"PACTA follows the Certificate Transparency hash structure:\n",
|
|
"\n",
|
|
"- Empty tree hash: `SHA256(\"\")`\n",
|
|
"- Leaf hash: `SHA256(0x00 || leaf_input)`\n",
|
|
"- Node hash: `SHA256(0x01 || left || right)`\n",
|
|
"\n",
|
|
"The prefix bytes prevent a leaf value from being confused with an internal node value.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"from pathlib import Path\n",
|
|
"import sys\n",
|
|
"\n",
|
|
"repo_root = Path.cwd()\n",
|
|
"if not (repo_root / \"src\" / \"pacta\").exists():\n",
|
|
" repo_root = repo_root.parent\n",
|
|
"sys.path.insert(0, str(repo_root / \"src\"))\n",
|
|
"\n",
|
|
"from pacta.transparency import (\n",
|
|
" leaf_hash,\n",
|
|
" node_hash,\n",
|
|
" merkle_root,\n",
|
|
" inclusion_proof,\n",
|
|
" verify_inclusion,\n",
|
|
" consistency_proof,\n",
|
|
" verify_consistency,\n",
|
|
")\n",
|
|
"\n",
|
|
"leaves = [f\"attestation-{i}\".encode() for i in range(1, 6)]\n",
|
|
"root = merkle_root(leaves)\n",
|
|
"print(root.hex())\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"for index, leaf in enumerate(leaves):\n",
|
|
" proof = inclusion_proof(leaves, index)\n",
|
|
" ok = verify_inclusion(leaf, index, len(leaves), proof, root)\n",
|
|
" print(index, ok, [node.hex()[:12] for node in proof])\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Consistency Proofs\n",
|
|
"\n",
|
|
"An inclusion proof answers: \"Is this leaf in this tree?\"\n",
|
|
"\n",
|
|
"A consistency proof answers: \"Is the newer tree an append-only extension of the older tree?\"\n",
|
|
"\n",
|
|
"Both are needed for a monitored transparency system. Inclusion is enough for one agent to bind one attestation to one signed tree head. Consistency lets monitors detect equivocation or tree rewrites across time.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"old_size = 3\n",
|
|
"old_root = merkle_root(leaves[:old_size])\n",
|
|
"new_root = merkle_root(leaves)\n",
|
|
"proof = consistency_proof(leaves, old_size)\n",
|
|
"print(\"old:\", old_root.hex())\n",
|
|
"print(\"new:\", new_root.hex())\n",
|
|
"print(\"proof:\", [node.hex()[:12] for node in proof])\n",
|
|
"print(\"consistent:\", verify_consistency(old_size, len(leaves), old_root, new_root, proof))\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Signed Tree Heads\n",
|
|
"\n",
|
|
"A Signed Tree Head records:\n",
|
|
"\n",
|
|
"- log ID,\n",
|
|
"- tree size,\n",
|
|
"- timestamp,\n",
|
|
"- root hash,\n",
|
|
"- hash algorithm,\n",
|
|
"- signatures.\n",
|
|
"\n",
|
|
"PACTA signs the canonical JSON STH payload with Ed25519 through OpenSSL. It also records an ML-DSA-65 slot. On this host, if no real ML-DSA backend is present, the slot is `unavailable`.\n",
|
|
"\n",
|
|
"Policy matters:\n",
|
|
"\n",
|
|
"- `require-signatures ed25519`: verify Ed25519 and allow ML-DSA to be unavailable.\n",
|
|
"- `require-signatures both`: require Ed25519 and ML-DSA verified. If ML-DSA is unavailable, fail closed.\n",
|
|
"- `--slhdsa-public-key <pem>`: additionally verify the second (post-quantum) SLH-DSA co-signature on the head; heads before tree size 14 report `absent` (allowed), a present-but-wrong signature fails closed.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"from pacta.postquantum import detect_ml_dsa\n",
|
|
"\n",
|
|
"capability = detect_ml_dsa()\n",
|
|
"print(capability.available)\n",
|
|
"print(capability.backend)\n",
|
|
"print(capability.reason)\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Why Ed25519 and ML-DSA Together?\n",
|
|
"\n",
|
|
"Ed25519 is useful because it is widely deployed, fast, and directly relevant to the Ed25519 proof corpus. That creates a deliberate \"eat your own dogfood\" loop: the proof-checking ecosystem signs evidence using a primitive whose implementation family is under formal scrutiny.\n",
|
|
"\n",
|
|
"ML-DSA adds post-quantum robustness for the accumulator signature layer. But it must be a real signature, not an aspirational label. If a host lacks ML-DSA, the correct result is an explicit blocker.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## The second signature that actually shipped: SLH-DSA\n",
|
|
"\n",
|
|
"Since tree size 14, every head of the LIVE log carries a second,\n",
|
|
"deterministic **SLH-DSA-SHA2-128s** (FIPS 205) signature beside the\n",
|
|
"required Ed25519 one. This is not the ML-DSA slot above - it is a\n",
|
|
"hash-based scheme, and it was chosen because the estate has PROVEN\n",
|
|
"its verify path (eleven certificates, log leaf 18): the log\n",
|
|
"co-signs with the parameter set whose verification path it itself\n",
|
|
"attests. Three design facts worth internalizing:\n",
|
|
"\n",
|
|
"1. Heads published before size 14 carry no co-signature, and\n",
|
|
" verifiers report them `ABSENT` rather than failing them - an\n",
|
|
" append-only log keeps the history of its own signature-scheme\n",
|
|
" upgrades.\n",
|
|
"2. The co-signature is deterministic on purpose: re-signing the\n",
|
|
" same payload is byte-comparable, so \"same input, same\n",
|
|
" signature\" becomes a diff you can run, not an assurance you\n",
|
|
" must trust.\n",
|
|
"3. Signing is still never proven - here, as everywhere in this\n",
|
|
" estate, certificates cover the VERIFY path only.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"# Runnable where OpenSSL >= 3.5 is present; honest skip otherwise.\n",
|
|
"import tempfile\n",
|
|
"from pathlib import Path\n",
|
|
"\n",
|
|
"from pacta import slhdsa\n",
|
|
"\n",
|
|
"tmp = Path(tempfile.mkdtemp(prefix=\"nb06-slhdsa-\"))\n",
|
|
"try:\n",
|
|
" slhdsa.generate_slhdsa_keypair(tmp / \"slh.key\", tmp / \"slh.pub\")\n",
|
|
"except Exception as exc:\n",
|
|
" print(\"SLH-DSA unavailable on this host (OpenSSL >= 3.5 needed):\", exc)\n",
|
|
"else:\n",
|
|
" payload = b\"canonical STH payload bytes\"\n",
|
|
" block = slhdsa.slh_dsa_signature_block(payload, tmp / \"slh.key\", tmp / \"slh.pub\")\n",
|
|
" ok, err = slhdsa.verify_payload_slhdsa(payload, block[\"signature_base64\"], tmp / \"slh.pub\")\n",
|
|
" print(\"co-signature verifies:\", ok, err or \"\")\n",
|
|
" block2 = slhdsa.slh_dsa_signature_block(payload, tmp / \"slh.key\", tmp / \"slh.pub\")\n",
|
|
" print(\"deterministic (byte-equal re-sign):\",\n",
|
|
" block[\"signature_base64\"] == block2[\"signature_base64\"])\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Two domains, two notebooks - by design\n",
|
|
"\n",
|
|
"Everything above is the shared VOCABULARY. The system itself has\n",
|
|
"exactly two roles, and the next two notebooks separate them on\n",
|
|
"purpose: **6a - the provider** (a singleton: builds every leaf via\n",
|
|
"Lean replay, builds the tree, signs the root with the merkleized\n",
|
|
"library, and Merkle-verifies its own signing library's leaf before\n",
|
|
"signing), and **6b - the agent** (one of many: the provider's\n",
|
|
"public key, the evidence files, ~25 lines of hashing, and nothing\n",
|
|
"else - explicitly NO Lean). Keep the mirror in mind as you drill\n",
|
|
"the primitives below; each drill belongs to one side.\n",
|
|
"\n",
|
|
"## Split Views: why a receipt is not enough\n",
|
|
"\n",
|
|
"Everything above verifies ONE receipt against ONE signed tree head. A malicious provider can maintain TWO trees - one shown to you, one shown to the world - and both views verify perfectly in isolation. This is EQUIVOCATION, and the defense is memory: pin every tree head you accept, and demand that every later tree head be CONSISTENT with your pin (same size -> same root; larger size -> a verified consistency proof from your pinned size; smaller size -> rollback, reject forever).\n",
|
|
"\n",
|
|
"pacta implements this as a local STH pin store. Run the whole attack and its detection, napkin-size:\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"# NAPKIN: pin a 2-leaf view, then let the log grow honestly - and then\n",
|
|
"# let a SPLIT VIEW present a different root at the pinned size.\n",
|
|
"import tempfile\n",
|
|
"from pathlib import Path as _P\n",
|
|
"from pacta.sthstore import check_sth_against_store\n",
|
|
"from pacta.transparency import consistency_proof, merkle_root, proof_to_hex\n",
|
|
"\n",
|
|
"honest = [b\"attestation-A\", b\"attestation-B\", b\"attestation-C\"]\n",
|
|
"evil = [b\"attestation-A\", b\"attestation-EVIL\", b\"attestation-C\"]\n",
|
|
"\n",
|
|
"with tempfile.TemporaryDirectory() as tmp:\n",
|
|
" store = _P(tmp) / \"sth-store.json\"\n",
|
|
" sth = lambda size, leaves: {\n",
|
|
" \"log_id\": \"demo-log\", \"tree_size\": size,\n",
|
|
" \"root_hash\": merkle_root(leaves[:size]).hex(),\n",
|
|
" \"timestamp\": \"2026-07-06T00:00:00Z\",\n",
|
|
" }\n",
|
|
" print(\"pin: \", check_sth_against_store(sth(2, honest), store).diagnostics[0])\n",
|
|
" grown = check_sth_against_store(\n",
|
|
" sth(3, honest), store,\n",
|
|
" consistency_proof_hex=proof_to_hex(consistency_proof(honest, 2)),\n",
|
|
" )\n",
|
|
" print(\"grow: \", grown.diagnostics[0])\n",
|
|
" attack = check_sth_against_store(sth(3, evil), store)\n",
|
|
" print(\"attack ok?\", attack.ok)\n",
|
|
" print(\"verdict: \", attack.diagnostics[0][:120], \"...\")\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"At real scale the same check runs on every `pacta receipt-verify --sth-store ...` and `pacta agent --sth-store ...` invocation; receipts embed a consistency anchor from the previous tree size, the provider serves proofs from arbitrary pinned sizes (`pacta_provider log-consistency --from-size N`), and `pacta_provider log-audit` is the monitor's self-check. A freshness policy (`--max-sth-age-seconds`) closes the stale-root hole: an old-but-valid tree head could hide later entries.\n",
|
|
"\n",
|
|
"### The real thing\n",
|
|
"\n",
|
|
"The `evidence/` directory holds four REAL receipts from the shipped transparency log (tree size 8 - the first four leaves honestly record a failed audit run; read `evidence/README.md`). Verify all four cryptographically and watch a fresh pin store handle them:\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"import tempfile\n",
|
|
"from pathlib import Path as _P\n",
|
|
"from pacta.sthstore import check_sth_against_store\n",
|
|
"from pacta.transparency import verify_receipt\n",
|
|
"from pacta.yamlio import load_data as _load\n",
|
|
"\n",
|
|
"log_key = repo_root / \"evidence\" / \"provider.ed25519.pub\"\n",
|
|
"with tempfile.TemporaryDirectory() as tmp:\n",
|
|
" store = _P(tmp) / \"pins.json\"\n",
|
|
" for fork in [\"dalek\", \"anza\", \"risc0\", \"betrusted\"]:\n",
|
|
" att = _load(repo_root / \"evidence\" / f\"{fork}-ed25519.attestation.yaml\")\n",
|
|
" receipt = _load(repo_root / \"evidence\" / f\"{fork}-ed25519.receipt.yaml\")\n",
|
|
" result = verify_receipt(att, receipt, log_key)\n",
|
|
" pin = check_sth_against_store(receipt[\"sth\"], store, consistency_from=receipt.get(\"consistency\"))\n",
|
|
" print(f\"{fork}: receipt accepted={result.accepted} backend={result.signatures.get('ed25519_backend')} pin={pin.action}\")\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Exercises\n",
|
|
"\n",
|
|
"- Tamper with one leaf and show that inclusion verification fails.\n",
|
|
"- Explain why the tree head signature must cover tree size as well as root hash.\n",
|
|
"- Napkin, then real: run the split-view drill above; then initialize a real provider log (`pacta_provider log-init`), append two attestations, and verify the second receipt with `--sth-store` - watch the pin advance with a verified consistency proof.\n",
|
|
"- Why must the consistency anchor's ROOT (not just its size) be checked against the pin? Construct the lie that a size-only check would miss.\n",
|
|
"- Write a policy for when an autonomous agent should require `both` signatures.\n",
|
|
"- Research checkpoint: compare PACTA's pin store to production Certificate Transparency monitor/gossip requirements - what does gossip add that a single pin store cannot?\n"
|
|
]
|
|
}
|
|
],
|
|
"metadata": {
|
|
"kernelspec": {
|
|
"display_name": "Python 3",
|
|
"language": "python",
|
|
"name": "python3"
|
|
},
|
|
"language_info": {
|
|
"name": "python",
|
|
"pygments_lexer": "ipython3"
|
|
}
|
|
},
|
|
"nbformat": 4,
|
|
"nbformat_minor": 5
|
|
}
|