| tags | cyber, cip |
|---|---|
| crystal-type | entity |
| crystal-domain | cyber |
| status | draft |
security properties and formal guarantees of [[nox]]
SOUNDNESS: Invalid transactions rejected with probability ≥ 1 - 2^(-128)
PRIVACY: Cannot distinguish transactions with same public structure
CONSERVATION: Σ(energy) = initial + minted - burned (mathematically enforced)
QUANTUM RESIST: Hash-based security only, ~128-bit post-quantum (Grover limit)
Attack │ Defense
────────────────┼─────────────────────────────────────────────
Double Spend │ Nullifier set prevents reuse
Inflation │ Circuit enforces conservation
Front-Running │ Privacy hides transaction contents
Sybil │ Focus proportional to stake
DoS │ Focus-based metering limits computation
Eclipse │ Namespace completeness proofs
Replay │ Nonces and nullifiers ensure uniqueness
Forgery │ ZK proofs unforgeable without witness
Theorem: nox is Turing-complete. Proof: Construct encoding of arbitrary Turing machine M via patterns 0-4, 9. ∎
Theorem: nox is confluent. Proof: Orthogonal rewrite system by Huet-Levy (1980). ∎
Theorem: Cost is identical across all reduction orders and implementations. Proof: By structural induction on formula. ∎
Theorem:
Theorem: A valid ZK proof implies all circuit constraints are satisfied with probability
Theorem: Same record cannot be spent twice. Proof:
- Each record has unique (nonce, owner_secret) pair
- Nullifier = H(nonce, owner_secret) is deterministic
- Same record → same nullifier
- Nullifier set is append-only
- Transaction rejected if nullifier already in set ∎
┌─────────────────────┬───────────────┬───────────────┬───────────────┬───────────────┐
│ Operation │ Traditional │ Blockchain │ Database │ nox │
│ │ (RAM model) │ (Ethereum) │ (SQL/NoSQL) │ │
├─────────────────────┼───────────────┼───────────────┼───────────────┼───────────────┤
│ Equality check │ O(n) compare │ O(n) compare │ O(n) compare │ O(1) hash │
│ Membership proof │ O(n) scan │ O(log n) MPT │ O(log n) index│ O(log² n) poly│
│ Completeness proof │ impossible │ impossible │ impossible │ O(log² n) poly│
│ Computation verify │ O(n) re-exec │ O(n) re-exec │ N/A │ O(log n) stark│
│ Recursive verify │ O(n) re-exec │ O(n) re-exec │ N/A │ O(1) composed │
│ Privacy + verify │ incompatible │ incompatible │ incompatible │ O(1) ZK proof │
├─────────────────────┼───────────────┼───────────────┼───────────────┼───────────────┤
│ Cost determinism │ ✗ cache-dep │ ~ gas approx │ ✗ query-dep │ ✓ structural │
│ Parallel safety │ ✗ explicit │ ✗ sequential │ ✗ locks │ ✓ confluent │
└─────────────────────┴───────────────┴───────────────┴───────────────┴───────────────┘
see [[cyber/nox]] for the execution model, [[cyber/bbg]] for the ZK privacy architecture, [[zheng]] for proof verification