6cb0140fae
The public history carried kat/__pycache__/mlkem768_reference.cpython-314.pyc, a compiled Python artifact embedding the operator's absolute local path. Text secret scanners do not read compiled binaries, which is exactly how it slipped through, and removing it from the tip would have left it reachable through the old root commits. So this repository is republished from a single clean root. This root also carries, from the previously unpublished line of work: - corrected LICENSE year, LICENSING.md, VERIFY-POLICY.md, and CITATIONS-UNRESOLVED.md remeasured 2026-08-11 (101 paths, README aligned) - O-018: run_consensus_verification.py ran 19 of 29 models and reported PASS; it now runs all 29, and computemarket_smt.py gains resolveByTimeout / reclaimUnsettled cases plus a negative control - O-006: the word 'audited' removed from next to Bouncy Castle, twice, after a concurrent edit resurrected it - O-014: prior art named and dated - Algorand's native falcon_verify shipped about ten months before AERE's precompiles; the primacy claim is withdrawn where it was implied - bench/ scripts parametrized so they actually run for an outsider (the earlier textual sanitization left $STAGING unexpanded inside Python strings) - AIP-2/AIP-3 errata with measured figures, spec remeasurements at 2026-08-01, and the spec-zk-stack retractions (owner is an operational key, not the Foundation; 'maximally sound' withdrawn; aggregator V1 deprecated) The redacted bench-host environment files from the sanitized line are kept exactly as published; the unredacted local variants are not carried.
168 lines
8.5 KiB
Python
168 lines
8.5 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# agentdid_session_smt.py
|
|
#
|
|
# SMT proof (z3) of the SESSION AUTHORIZATION invariants for AereAgentDID: the
|
|
# per-session cumulative SPEND CAP, the expiry / revocation / root-lifecycle
|
|
# gating, and the anti-replay action nonce.
|
|
#
|
|
# Contract: contracts/contracts/pqc/AereAgentDID.sol (authorize / issueSession /
|
|
# revokeSession / _isSessionLive)
|
|
#
|
|
# This is a hot-key authorization surface: a leaked secp256k1 session key must be
|
|
# contained by (a) a cumulative spend cap it can never exceed, (b) an expiry after
|
|
# which it stops working, (c) an on-chain revocation, (d) its root Falcon key still
|
|
# being ACTIVE, and (e) a strictly-increasing action nonce so a captured signature
|
|
# cannot be replayed. We model authorize() as an inductive transition system on
|
|
# (spent, actionNonce) with the exact Solidity guards.
|
|
#
|
|
# Per session:
|
|
# cap = spendCap (immutable at issuance)
|
|
# spent = cumulative spend recorded so far
|
|
# n = actionNonce
|
|
# live = exists AND NOT revoked AND now <= expiry AND rootActive AND rootFalcon
|
|
#
|
|
# authorize(amount) Solidity guards, then effects:
|
|
# require live (_isSessionLive)
|
|
# require scope == scopeHash (scope gate)
|
|
# require spent+amount >= spent AND spent+amount <= cap (overflow + CAP gate)
|
|
# require ecrecover(...) == sessionAddr (sig gate)
|
|
# s.actionNonce = n + 1; s.spent = spent + amount
|
|
#
|
|
# SPEND-CAP INVARIANT (task target): spent <= cap, ALWAYS.
|
|
# NONCE INVARIANT (anti-replay): actionNonce strictly increases on every
|
|
# successful authorize, so no two successful actions share a digest.
|
|
# GATING INVARIANT: a non-live session (revoked / expired / root-inactive) can
|
|
# NEVER record spend (authorize reverts, state unchanged).
|
|
#
|
|
# Method: PROVED = negation UNSAT under guards. NEG-CTRL = buggy variant's
|
|
# violation SAT (real counterexample => guard is load-bearing).
|
|
#
|
|
# ASSUMPTIONS (bound every PROVED):
|
|
# A1. ecrecover is a sound signature oracle: it returns sessionAddr ONLY for a
|
|
# genuine session-key signature over the exact digest. Its cryptographic
|
|
# soundness is out of scope (same class as the halmos precompile-oracle
|
|
# assumption). We model the sig gate as a boolean the adversary can only
|
|
# satisfy with a real signature; the cap/nonce/gating proofs hold for BOTH
|
|
# branches (sig ok / not ok), i.e. regardless of what ecrecover returns.
|
|
# A2. spendCap is fixed at issuance and never mutated (confirmed: no setter).
|
|
# A3. Design math (unbounded Ints). Solidity 0.8 checked add on spent+amount is
|
|
# modelled by the explicit overflow guard already present in the source.
|
|
# -----------------------------------------------------------------------------
|
|
from z3 import Int, Bool, Solver, And, Or, Not, If, sat, unsat
|
|
|
|
results = []
|
|
def check(name, s, expect_unsat=True, kind="PROOF"):
|
|
r = s.check()
|
|
if expect_unsat:
|
|
ok = (r == unsat); tag = "PROVED" if ok else "FAILED"
|
|
else:
|
|
ok = (r == sat); tag = "CEX-FOUND" if ok else "FAILED"
|
|
results.append((name, tag, ok, kind))
|
|
print(f"[{tag:9}] ({kind}) {name}: z3={r} (expected {'unsat' if expect_unsat else 'sat'})")
|
|
if r == sat:
|
|
m = s.model()
|
|
wit = {}
|
|
for d in m.decls():
|
|
try: wit[str(d)] = m[d].as_long()
|
|
except Exception:
|
|
try: wit[str(d)] = bool(m[d])
|
|
except Exception: wit[str(d)] = "?"
|
|
print(" witness:", wit)
|
|
return ok
|
|
|
|
print("### AereAgentDID -- session spend-cap / gating / anti-replay\n")
|
|
|
|
# ---- BASE CASE: a freshly issued session. issueSession sets spent=0, and
|
|
# InvalidSessionParams requires expiry > block.timestamp, so cap>=0 and
|
|
# spent(0) <= cap holds at birth. ------------------------------------------
|
|
s = Solver()
|
|
cap = Int('cap')
|
|
s.add(cap >= 0)
|
|
s.add(Not(0 <= cap))
|
|
check("base case (freshly issued session) satisfies spent<=cap", s)
|
|
|
|
# ---- C1 SPEND CAP inductive: authorize() preserves spent <= cap ---------------
|
|
# Guards: overflow guard (spent+amount does not wrap) AND spent+amount <= cap.
|
|
# The Solidity condition is: revert IF (spent+amount < spent) OR (spent+amount > cap).
|
|
# So the SUCCESS path requires: spent+amount >= spent AND spent+amount <= cap.
|
|
s = Solver()
|
|
cap, spent, amount = Int('cap'), Int('spent'), Int('amount')
|
|
s.add(spent >= 0, spent <= cap, amount >= 0) # INV(pre) + amount is a uint
|
|
s.add(spent + amount >= spent, spent + amount <= cap) # authorize success guard
|
|
spent2 = spent + amount
|
|
s.add(Not(spent2 <= cap)) # negate INV(post)
|
|
check("C1 authorize() preserves spend cap (spent <= cap inductive)", s)
|
|
|
|
# ---- C2 GATING: a non-live session can never record spend --------------------
|
|
# _isSessionLive must be TRUE to reach the effects. If the session is revoked OR
|
|
# expired OR its root is not ACTIVE Falcon, authorize reverts (no state change).
|
|
# We show: (NOT live) AND (reached effects) is infeasible -- the guard blocks it.
|
|
s = Solver()
|
|
revoked, expired, rootInactive, reachedEffects = Bool('revoked'), Bool('expired'), Bool('rootInactive'), Bool('reachedEffects')
|
|
live = And(Not(revoked), Not(expired), Not(rootInactive))
|
|
# reachedEffects can only be true when live is true (that is the guard).
|
|
s.add(reachedEffects == live)
|
|
s.add(Or(revoked, expired, rootInactive)) # session is NOT live
|
|
s.add(reachedEffects) # but we claim spend was recorded
|
|
check("C2 gating: revoked/expired/root-inactive session cannot record spend", s)
|
|
|
|
# ---- C3 ANTI-REPLAY: actionNonce strictly increases on each successful authorize
|
|
# (n -> n+1), so two successful actions never share the signed digest. ------
|
|
s = Solver()
|
|
n = Int('n')
|
|
s.add(n >= 0)
|
|
n2 = n + 1
|
|
s.add(Not(n2 > n)) # negate strict-increase
|
|
check("C3 anti-replay: actionNonce strictly increases (n+1 > n)", s)
|
|
|
|
# ---- C4 EXPIRY monotonic: once now > expiry the session is dead forever (expiry
|
|
# is immutable and now is non-decreasing across blocks). ------------------
|
|
s = Solver()
|
|
expiry, now1, now2 = Int('expiry'), Int('now1'), Int('now2')
|
|
s.add(now2 >= now1, now1 > expiry) # already expired at now1, time advances
|
|
s.add(Not(now2 > expiry)) # can it become un-expired later?
|
|
check("C4 expiry is terminal: now>expiry stays true as time advances", s)
|
|
|
|
# ---- NEG-CTRL 1: a BUGGY cap gate that checks the PER-ACTION amount against the
|
|
# cap (amount <= cap) instead of the CUMULATIVE spent+amount. Over several
|
|
# actions the cumulative spent blows past cap. z3 finds the overshoot. ------
|
|
s = Solver()
|
|
cap, spent, amount = Int('cap'), Int('spent'), Int('amount')
|
|
s.add(spent >= 0, spent <= cap, amount >= 0)
|
|
s.add(amount <= cap) # BUG: per-action check only
|
|
spent2 = spent + amount
|
|
s.add(spent2 > cap) # cumulative exceeds cap
|
|
check("NEG-CTRL per-action cap check CAN let cumulative spent exceed cap", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL 2: a BUGGY gate that OMITS the liveness check (records spend even
|
|
# when revoked). z3 finds a revoked session recording spend. ---------------
|
|
s = Solver()
|
|
revoked = Bool('revoked')
|
|
reachedEffects = Bool('reachedEffects')
|
|
s.add(reachedEffects == True) # BUG: effects reached unconditionally
|
|
s.add(revoked == True) # session revoked
|
|
s.add(reachedEffects, revoked) # revoked session still spends
|
|
check("NEG-CTRL missing-liveness gate CAN let a revoked session record spend", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ------------------------------------------------------------------------------
|
|
print("\n=== SUMMARY ===")
|
|
allok = True
|
|
for name, tag, ok, kind in results:
|
|
print(f" {tag:9} [{kind}] {name}")
|
|
allok = allok and ok
|
|
print()
|
|
print("AereAgentDID session authorization:")
|
|
if allok:
|
|
print(" PROVED the spend cap is inductive (C1: spent<=cap for any sequence of actions),")
|
|
print(" non-live sessions cannot spend (C2: revoked/expired/root-inactive all blocked),")
|
|
print(" the action nonce strictly increases (C3: no signature replay), and expiry is")
|
|
print(" terminal (C4). Two NEG-CTRLs confirm the CUMULATIVE cap check and the liveness")
|
|
print(" gate are load-bearing. Signature soundness of ecrecover is assumed (A1).")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected CEX above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|