Skip to content

Commit 756e3c4

Browse files
claudeclaude
committed
proofs(attestation): unforgeability of the intent->evidence->seal chain (Idris2)
PROOF-PROGRAMME §3.2. New src/abi/AttestationUnforgeability.idr models the seal (chain_hash = H(intent||evidence||report), Ed25519-signed) with the cryptographic facts as a `parameters` block — hypotheses, NOT `postulate` (PA021 bans escape hatches), so it is an honest conditional theorem. Under `%default total` it Qed-closes: - integrity tampering any phase invalidates the seal - authenticity a verifying seal comes from the matching secret key - nonRepudiation a genuine seal verifies (publicly checkable) plus 2 corollaries. Conditional on chain-hash collision-resistance + Ed25519 EUF-CMA (message- and signer-binding) + signature correctness. Typechecks under Idris2 0.8.0. PROOF-NEEDS ledger updated (also records the §3.1 hexad round-trip that landed in #122). Closes #123. https://claude.ai/code/session_01K2TJLeQSyz4tpydZ18aRcb
1 parent cfc892f commit 756e3c4

3 files changed

Lines changed: 145 additions & 2 deletions

File tree

‎CHANGELOG.md‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,20 @@
22

33
## [Unreleased]
44

5+
### Added — attestation unforgeability proof (Idris2, PROOF-PROGRAMME §3.2)
6+
7+
- **`src/abi/AttestationUnforgeability.idr`**: Idris2 proof that the
8+
intent→evidence→seal attestation chain is unforgeable. Models
9+
`chain_hash = H(intent‖evidence‖report)` + the Ed25519 signature with the
10+
cryptographic facts (chain-hash collision-resistance, Ed25519 EUF-CMA
11+
message- and signer-binding, signature correctness) as a `parameters`
12+
block — hypotheses, **not** `postulate` (PA021 bans escape hatches), so it
13+
is an honest *conditional* theorem. Under `%default total` it Qed-closes
14+
`integrity` (tampering any phase invalidates the seal), `authenticity`
15+
(a verifying seal comes from the matching key), and `nonRepudiation`
16+
(a genuine seal verifies), plus two corollaries. Typechecks under Idris2
17+
0.8.0. Closes #123.
18+
519
### Added — `assay` / `assimilate` / `aggregate` proof-integration subcommands
620

721
Three new a-themed subcommands that wire panic-attack into the

‎PROOF-NEEDS.md‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
## Current State
44

5-
- **src/abi/*.idr**: 4 files — `Types.idr`, `PatternCompleteness.idr` (PA1 ✅ 2026-04-11), `ClassificationSoundness.idr` (PA2 ✅ 2026-04-11), `Stripping.idr` (PROOF-PROGRAMME Layer 1.0 line-comment slice ✅ 2026-06-02 — multi-comment semantics + slash-slash closure both Qed via mutual-recursive `bodyIsFixedPoint`)
5+
- **src/abi/*.idr**: 5 files — `Types.idr`, `PatternCompleteness.idr` (PA1 ✅ 2026-04-11), `ClassificationSoundness.idr` (PA2 ✅ 2026-04-11), `Stripping.idr` (PROOF-PROGRAMME Layer 1.0 line-comment slice ✅ 2026-06-02 — multi-comment semantics + slash-slash closure both Qed via mutual-recursive `bodyIsFixedPoint`), `AttestationUnforgeability.idr` (PROOF-PROGRAMME §3.2 ✅ 2026-06-04 — conditional unforgeability from Ed25519 EUF-CMA + chain-hash collision-resistance hypotheses)
66
- **Dangerous patterns**: 0 in own code (3 references are in the analyzer that DETECTS believe_me in other repos); 282 `unwrap()` calls
77
- **LOC**: ~31,700 (Rust)
88
- **ABI layer**: Idris2 with completeness + soundness proofs + Layer-1.0 stripping foundation
@@ -14,14 +14,15 @@
1414
| PA1 Pattern detection completeness | `src/abi/PatternCompleteness.idr` | All 49 `Lang` constructors have an analyzer; all 20 `WPCategory` constructors have at least one detector; cross-language checks applied unconditionally to all languages. `completeScanForAll` is the top-level theorem. |
1515
| PA2 Classification soundness | `src/abi/ClassificationSoundness.idr` | Severity (Low/Medium/High/Critical) is totally ordered (`LTE`); `maxSeverity` is commutative and idempotent; numeric ABI encoding preserves the ordering. |
1616
| Layer 1.0 line-comment idempotence | `src/abi/Stripping.idr` | **2026-06-02 close-out (issue #113)**: corrects PR #111's single-comment model to multi-comment via mutual recursion (`stripLineComments ↔ stripLineCommentBody` — body calls back into main after each preserved newline). Qed-closes `stripLineCommentsIdempotent` for ALL cases including the slash-slash inductive via the load-bearing `bodyIsFixedPoint` lemma proved by mutual induction with the main theorem. 7 sanity-check theorems including the two-comments-on-different-lines case PR #111 silently mis-stripped. |
17+
| Attestation chain unforgeability | `src/abi/AttestationUnforgeability.idr` | **PROOF-PROGRAMME §3.2 (2026-06-04, issue #123)**: models the intent→evidence→seal chain (`chain_hash = H(intent‖evidence‖report)`, Ed25519-signed) with the cryptographic facts as a `parameters` block (hypotheses, **not** `postulate`). Under `%default total` Qed-closes `integrity` (tampering any phase invalidates the seal), `authenticity` (a verifying seal comes from the matching secret key), `nonRepudiation` (a genuine seal verifies), plus 2 corollaries. Conditional on chain-hash collision-resistance + Ed25519 EUF-CMA (message- and signer-binding) + signature correctness. |
18+
| Hexad↔Octad persistence round-trip | `src/storage/mod.rs` (proptest) | **PROOF-PROGRAMME §3.1 (2026-06-04, #122)**: `hexad_json_roundtrip_is_identity` proves the on-disk serde round-trip (`write_*_hexad` → `load_hexad_dir`) is the identity on the hexad JSON. The gateway octad projection is lossy by design, so the faithful integrity property is the persistence round-trip, not the literal hexad↔octad map. |
1719

1820
## What Still Needs Proving
1921

2022
| Component | What | Why |
2123
|-----------|------|-----|
2224
| **Layer 1.0 — stripBlockComments + Strings + Composition + Position-Preservation** (issue #114) | Block-comment (`/* */`) and string-literal (`"..."`) strippers with same mutual-recursive shape; composition theorem proving the full pipeline is idempotent given each component is; position-preservation theorem justifying analyzer location-reporting against the stripped view as if it were original-source. | Four slices: `Stripping_Block.idr`, `Stripping_Strings.idr`, `Stripping_Composition.idr`, `Stripping_PositionPreservation.idr`. |
2325
| Bridge reachability soundness | Reachability analysis is sound (no reachable dep wrongly classified as phantom) | Unreachable code marked reachable wastes effort; reachable missed = security gap |
24-
| Attestation chain unforgeability | Intent/evidence/seal triple is cryptographically bound; tampering detectable | Tampered attestations break trust chain |
2526
| Kanren taint analysis | Taint propagation tracks all tainted data flows | Missed taint flow means missed vulnerability |
2627

2728
## Recommended Prover

‎src/abi/AttestationUnforgeability.idr‎

Lines changed: 128 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,128 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
4+
||| Attestation-chain unforgeability (PROOF-PROGRAMME §3.2).
5+
|||
6+
||| Mirrors `src/attestation/{intent,evidence,seal}.rs`. The seal binds the
7+
||| three attestation phases via
8+
|||
9+
||| chain_hash = H(intent_hash || evidence_hash || report_hash)
10+
|||
11+
||| and optionally signs that chain hash with Ed25519.
12+
|||
13+
||| The cryptographic facts the seal relies on are taken as explicit
14+
||| HYPOTHESES — a `parameters` block, NOT `postulate` (panic-attack's own
15+
||| ProofDrift detector, PA021, bans `postulate` / `believe_me` / `Admitted`).
16+
||| This therefore proves a *conditional* theorem: GIVEN the standard
17+
||| cryptographic assumptions, the chain is unforgeable. The assumptions are:
18+
|||
19+
||| * `chainCR` — collision resistance of the chain hash, in the
20+
||| idealised injective form (distinct phase triples
21+
||| hash apart). Matches the SHA-256 `chain_hash`.
22+
||| * `sigCorrect` — a genuine Ed25519 signature verifies.
23+
||| * `sigBindsMessage` — EUF-CMA (message-binding facet): a signature made
24+
||| over `d` only verifies against `d`.
25+
||| * `sigOnlySigner` — EUF-CMA (signer-binding facet): a verifying
26+
||| signature comes from the matching secret key.
27+
|||
28+
||| From these — with no further assumptions, every lemma `Qed`-closes — we
29+
||| derive the three properties of PROOF-PROGRAMME §3.2:
30+
|||
31+
||| 1. `integrity` — tampering with any phase invalidates the seal.
32+
||| 2. `authenticity` — a verifying seal comes from the matching key.
33+
||| 3. `nonRepudiation` — a genuine seal is publicly verifiable.
34+
module PanicAttack.ABI.AttestationUnforgeability
35+
36+
%default total
37+
38+
-- ═══════════════════════════════════════════════════════════════════════
39+
-- Abstract chain + signature model, with the cryptographic assumptions as
40+
-- module parameters (hypotheses, not postulates).
41+
-- ═══════════════════════════════════════════════════════════════════════
42+
43+
parameters
44+
(Bytes, Digest, SecretKey, PublicKey, Sig : Type)
45+
(chainHash : Bytes -> Bytes -> Bytes -> Digest)
46+
(pubKey : SecretKey -> PublicKey)
47+
(sign : SecretKey -> Digest -> Sig)
48+
(verify : PublicKey -> Digest -> Sig -> Bool)
49+
(chainCR : (i, e, r, i', e', r' : Bytes) ->
50+
chainHash i e r = chainHash i' e' r' ->
51+
((i, e, r) = (i', e', r')))
52+
(sigCorrect : (sk : SecretKey) -> (d : Digest) ->
53+
verify (pubKey sk) d (sign sk d) = True)
54+
(sigBindsMessage : (sk : SecretKey) -> (d, d' : Digest) ->
55+
verify (pubKey sk) d' (sign sk d) = True -> d = d')
56+
(sigOnlySigner : (pk : PublicKey) -> (d : Digest) -> (s : Sig) ->
57+
verify pk d s = True ->
58+
(sk : SecretKey ** (pk = pubKey sk, s = sign sk d)))
59+
60+
||| The seal over the three phases: sign the chain hash.
61+
seal : SecretKey -> Bytes -> Bytes -> Bytes -> Sig
62+
seal sk i e r = sign sk (chainHash i e r)
63+
64+
||| Public validity check (anyone with the public key can run it).
65+
valid : PublicKey -> Bytes -> Bytes -> Bytes -> Sig -> Bool
66+
valid pk i e r s = verify pk (chainHash i e r) s
67+
68+
-- ─────────────────────────────────────────────────────────────────────
69+
-- 1. INTEGRITY: tampering with any phase invalidates the seal.
70+
-- ─────────────────────────────────────────────────────────────────────
71+
72+
||| If the phase triple is tampered (differs from the sealed one), a seal
73+
||| produced over the original phases fails to verify against the tampered
74+
||| ones. Proof: were it to verify, message-binding would force the chain
75+
||| hashes equal and collision-resistance the triples equal — contradiction.
76+
integrity : (sk : SecretKey) ->
77+
(i, e, r, i', e', r' : Bytes) ->
78+
Not ((i, e, r) = (i', e', r')) ->
79+
verify (pubKey sk) (chainHash i' e' r') (sign sk (chainHash i e r)) = False
80+
integrity sk i e r i' e' r' neq
81+
with (verify (pubKey sk) (chainHash i' e' r') (sign sk (chainHash i e r))) proof prf
82+
integrity sk i e r i' e' r' neq | True =
83+
absurd (neq (chainCR i e r i' e' r'
84+
(sigBindsMessage sk (chainHash i e r) (chainHash i' e' r') prf)))
85+
integrity sk i e r i' e' r' neq | False = Refl
86+
87+
-- ─────────────────────────────────────────────────────────────────────
88+
-- 2. AUTHENTICITY: a verifying seal comes from the matching secret key.
89+
-- ─────────────────────────────────────────────────────────────────────
90+
91+
||| A seal that verifies under `pk` must have been produced by the holder
92+
||| of the secret key whose public key is `pk`, signing exactly this
93+
||| chain hash. Direct from the signer-binding facet of EUF-CMA.
94+
authenticity : (pk : PublicKey) -> (i, e, r : Bytes) -> (s : Sig) ->
95+
verify pk (chainHash i e r) s = True ->
96+
(sk : SecretKey ** (pk = pubKey sk, s = sign sk (chainHash i e r)))
97+
authenticity pk i e r s ok = sigOnlySigner pk (chainHash i e r) s ok
98+
99+
-- ─────────────────────────────────────────────────────────────────────
100+
-- 3. NON-REPUDIATION: a genuine seal is publicly verifiable.
101+
-- ─────────────────────────────────────────────────────────────────────
102+
103+
||| A seal produced by `sk` over `(i, e, r)` always verifies under the
104+
||| corresponding public key, so the signer cannot deny a seal that checks
105+
||| out — verification is a deterministic public function. (= correctness.)
106+
nonRepudiation : (sk : SecretKey) -> (i, e, r : Bytes) ->
107+
verify (pubKey sk) (chainHash i e r) (sign sk (chainHash i e r)) = True
108+
nonRepudiation sk i e r = sigCorrect sk (chainHash i e r)
109+
110+
-- ─────────────────────────────────────────────────────────────────────
111+
-- Corollaries (sanity).
112+
-- ─────────────────────────────────────────────────────────────────────
113+
114+
||| The seal/valid wrappers agree with the underlying signature ops: a
115+
||| freshly produced seal is `valid`. Ties the readable API to property 3.
116+
sealValid : (sk : SecretKey) -> (i, e, r : Bytes) ->
117+
valid (pubKey sk) i e r (seal sk i e r) = True
118+
sealValid sk i e r = sigCorrect sk (chainHash i e r)
119+
120+
||| Two phase triples that share a verifying seal under one key are equal
121+
||| (no two distinct attestations collide under the same seal).
122+
sealNoCollision : (sk : SecretKey) -> (i, e, r, i', e', r' : Bytes) ->
123+
verify (pubKey sk) (chainHash i e r) (sign sk (chainHash i e r)) = True ->
124+
verify (pubKey sk) (chainHash i' e' r') (sign sk (chainHash i e r)) = True ->
125+
((i, e, r) = (i', e', r'))
126+
sealNoCollision sk i e r i' e' r' _ tampered =
127+
chainCR i e r i' e' r'
128+
(sigBindsMessage sk (chainHash i e r) (chainHash i' e' r') tampered)

0 commit comments

Comments
 (0)