# IHVRK security invariants

Two models check these, written separately from the code that enforces them:

* **Z3** (`solver/ihvrk_solver.py`): the decision function `Decide(s)` over a typed fact state, plus a three-variable
  permit machine. Command: `python3 -m ihvrk.solver.ihvrk_solver`; result file `evidence/z3_proofs.json`.
* **TLA+** (`formal/IHVRK.tla`): the protocol with concurrency, a network attacker, crashes, expiry and fairness.
  Command: `formal/run_tlc.sh`; result `evidence/tlc_summary.json`.

How to read a Z3 result: each invariant is checked by asking Z3 for a state that **violates the requirement and is
still authorized**. `UNSAT` means no such state exists *in the model*. Every row also has a **sensitivity check**:
the guard that enforces it is removed and the same query must become `SAT` with a concrete counterexample. That
shows the proof depends on that guard, so it is not vacuous. A separate **control** query (`Decide(s) = AUTHORIZE`
is `SAT`) shows the model can authorize at all. A denied request is an ordinary `SAT` state whose decision is
`DENY`. `UNSAT` is never used to mean "attack detected".

What none of this proves: that the Python enforces the same rule (that is the job of the differential test
`test_differential_z3_vs_python`, the runtime cross-check in `decide()`, and the integration suites), or anything
about the kernel, Ed25519 implementation, SQLite, the network, or the person holding a verifier key.

Notation: `s` is a fact state (fields in `policy/authorization_policy.py: AuthzState`). `lo = now − u`,
`hi = now + u` where `u` is the declared clock uncertainty.

| # | Statement | Formal (Z3 query; expected UNSAT) | Assumptions | Sensitivity guard removed → SAT | Enforced in code | Tests |
|---|---|---|---|---|---|---|
| I1 | No execution without valid authorization | inductive: `Init ⇒ Inv`, `Inv ∧ Step ⇒ Inv'` where `Inv` ⊇ `permit≠NONE ⇒ authorized`, `executions>0 ⇒ permit=CONSUMED` | ISSUE is the only transition creating a permit | ISSUE without `Decide=AUTHORIZE` | `_issue_permit`, `ExecutionGate.execute` | integration, D1–D3, I9 |
| I2 | No authorization from an invalid signature | `(hvt_sig≠VALID ∨ cap_sig≠VALID) ∧ Decide=AUTHORIZE` | signature facts are computed by `verify_structure` | `hvt_signature`, `hvt_signature_indet` | `signature_verifier.verify_structure` | A1–A4, B1, signatures unit |
| I3 | No authorization from an untrusted issuer | `(hvt_issuer≠VALID ∨ cap_issuer≠VALID) ∧ AUTHORIZE` | enrollment keys pinned locally | `hvt_issuer`, `hvt_issuer_indet` | `VerifierRegistry.enroll/lookup`, capability issuer map | A2, A6, E2 |
| I4 | No authorization from an expired or revoked token | `(revoked ∨ verifier_status≠VALID ∨ hi ≥ hvt_exp ∨ hi ≥ cap_exp) ∧ AUTHORIZE` | status list fresh within `max_age` | `revoked` | `credential_status`, expiry checks | A8, A9, H6c, permit expiry |
| I5 | No authorization from an invalid or consumed challenge | `(challenge≠ISSUED ∨ ¬nonce_match) ∧ AUTHORIZE` | nonce state read in the same transaction that consumes it | `challenge` | `EpochRegistry.consume_challenge` | D6–D9 |
| I6 | No authorization when human approval is absent | `human≠APPROVE ∧ AUTHORIZE` | – | `human_decision` | approval `decision` field | human-deny tests |
| I7 | No authorization for a different digest or resource | `(appr_digest≠action_digest ∨ appr_res≠res) ∧ AUTHORIZE` | SHA-256 collision resistance | `digest` | approval binding + gate re-digest | C2–C4, D2 |
| I8 | No authorization outside capability scope/audience/subject/tenant | `(¬scope ∨ ¬aud ∨ ¬subject ∨ ¬tenant) ∧ AUTHORIZE` | – | `cap_scope` | `_capability_facts` | E3, D11 |
| I9 | No authorization with stale policy version or epoch | `(pv≠current ∨ epoch≠current ∨ appr_epoch≠epoch) ∧ AUTHORIZE` | policy version only increases | `policy_version` | service + gate | policy-bump test, D10 |
| I10 | No authorization when the solver is UNKNOWN / TIMEOUT | `solver≠OK ∧ AUTHORIZE` | – | `solver` | `ihvrk_solver.decide` | H1, H2, H9, formal suite |
| I11 | No permit reuse after atomic consumption | inductive (as I1); CONSUME requires `permit=ISSUED` | registry transaction is atomic | CONSUME without `permit=ISSUED` | `consume_permit` | D1, D3, I9 |
| I12 | No authorization when environmental trust fails | `(env≠VALID ∨ enforcement≠BLOCKED) ∧ AUTHORIZE` | attestation key pinned | `env`, `env_trust_indet` | `AttestationVerifier`, `enforcement_probe` | attestation & enforcement integration tests |
| I13 | No authorization with indeterminate identity, time or provenance | `(status=INDET ∨ issuer=INDET ∨ ¬time_trusted ∨ lo<hvt_exp≤hi) ∧ AUTHORIZE` | – | `time_untrusted` | `indeterminate_reasons` | H3, H4, boundary unit tests |
| I14 | No authorization from an agent-supplied approval claim | `(channel≠VERIFIER ∨ ¬independent) ∧ AUTHORIZE` | `channel` set by transport, not by message | `approval_channel` | `submit_approval(channel=…)`, independence check | B4, E1, E7 |
| I15 | No conflicting terminal outcomes for one request | inductive: `¬(completed ∧ denied)`, `denied ⇒ permit=NONE` | – | DENY without `¬completed` (+ CONSUME guard) | state machine `LEGAL`, CAS transitions | state-machine unit, D5 |

## TLA+ properties (formal/IHVRK.tla)

| Property | Kind | Design config | Broken variant that must violate it |
|---|---|---|---|
| `NoUnauthorizedExecution` | invariant | holds | `no_auth_check`, `no_digest_check` |
| `NoDoubleExecution` | invariant | holds | `permit_reuse` |
| `PermitBoundToAction`, `ChallengeUniqueness`, `DeniedNeverExecutes`, `TypeOK` | invariants | hold | – |
| `TerminalStable`, `ExecOnlyByConsume` | action properties | hold | – |
| `EventuallyResolved` | liveness, under weak fairness of the service and the clock only (no fairness for the human, agent or attacker) | holds | – |

Model bounds: 2 requests, 2 actions, 3 nonces, clock 0..3, TTL 2. Fault model: crash faults for the service, an
attacker who controls the network (drop, duplicate, reorder, replay, inject unauthenticated messages), a human who
may never answer, one logical clock. Byzantine replicas are not modelled. Results: `evidence/tlc_summary.json`.

Observation from the `no_nonce_consume` variant: the model shows no violation even with nonce consumption removed,
because the request-state compare-and-swap already stops a second acceptance. In this design, nonce consumption is
defence in depth. It would matter in a design where the request state could be reset.

## Gap between the models and the code

* Both models use abstract facts ("signature VALID"). The mapping from bytes to facts is the code under test.
* The Z3 model has one request. Concurrency is covered by TLA+ and by the race tests (threads and processes),
  not by Z3.
* TLA+ treats each registry transaction as one atomic step. That relies on SQLite `BEGIN IMMEDIATE` on a single file.
* Neither model covers the runtime gatekeeper or eBPF.