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.
209 lines
12 KiB
Python
209 lines
12 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# pqckeyregistry_smt.py
|
|
#
|
|
# SMT proof (z3) of the SAFETY invariants of AerePQCKeyRegistry, the LIVE (mainnet
|
|
# chain 2800, deployed 2026-07-12) permissionless post-quantum public-key registry
|
|
# with on-chain proof-of-possession (PoP), at address
|
|
# 0x1eCa3c5ADcBD0b22636D8672b00faC6D89363691
|
|
#
|
|
# Contract: contracts/contracts/pqc/AerePQCKeyRegistry.sol
|
|
#
|
|
# Style follows formal-consensus/spokepool_smt.py (the model that surfaced the real
|
|
# SpokePool bond-accounting bug): each property is PROVED by showing the negation is
|
|
# UNSAT under the exact Solidity guards, and every proof is paired with a firing
|
|
# NEGATIVE CONTROL (a buggy variant whose violation is SAT) so the proofs are
|
|
# demonstrably non-vacuous -- the guard is load-bearing.
|
|
#
|
|
# TARGET INVARIANTS (from the build task):
|
|
# K1 PoP cannot be forged / replayed ACROSS IDENTITIES: the challenge a valid PoP
|
|
# commits to binds the owner, so a proof accepted for identity O is over a
|
|
# DIFFERENT message than the one required to register the same key under O'!=O.
|
|
# K2 PoP cannot be replayed by the SAME identity: the per-identity nonce is inside
|
|
# the challenge and advances (n -> n+1) before the key is stored, so the
|
|
# consumed proof's message differs from the next required message.
|
|
# K3 A REVOKED key NEVER verifies (verifyWithKey is fail-closed on REVOKED/NONE),
|
|
# regardless of what the precompile would return.
|
|
# K4 ROTATION preserves the OWNER BINDING: the successor key's owner equals the
|
|
# predecessor's owner (== msg.sender == old.owner), and the old key leaves
|
|
# ACTIVE (becomes ROTATED, so isActiveKey(old) is false).
|
|
#
|
|
# ASSUMPTIONS (these bound every PROVED result -- stated honestly):
|
|
# A1. SIGNATURE SOUNDNESS (out of scope, same class as the halmos precompile
|
|
# oracle): the live PQC precompile returns true for (pk, m, sig) ONLY when sig
|
|
# is a genuine signature by the holder of pk over EXACTLY m. Thus an actor who
|
|
# does not hold pk's secret cannot produce a valid sig over a message the holder
|
|
# never signed. The registry's job -- and what we prove here -- is the DOMAIN
|
|
# SEPARATION that makes the signed message identity/nonce-specific. Cryptographic
|
|
# soundness of Falcon/ML-DSA/SLH-DSA is covered by NIST KATs + live eth_call, not
|
|
# here.
|
|
# A2. keccak256(abi.encode(...)) is INJECTIVE (collision-free) -- standard EVM
|
|
# verification assumption. We model "challenge equal" as equality of the encoded
|
|
# tuple (all fields equal); K1/K2 rest on this.
|
|
# A3. Design math (this is a DESIGN model, not the compiled bytecode). The halmos
|
|
# bytecode layer (contracts/test/formal) is the complementary check.
|
|
# -----------------------------------------------------------------------------
|
|
from z3 import (Int, Bool, BitVec, Solver, And, Or, Not, Implies, If, sat, unsat)
|
|
|
|
# scheme / status constants (match the contract)
|
|
STATUS_NONE, STATUS_ACTIVE, STATUS_ROTATED, STATUS_REVOKED = 0, 1, 2, 3
|
|
|
|
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("### AerePQCKeyRegistry -- proof-of-possession domain separation, revoke, rotation\n")
|
|
|
|
# =============================================================================
|
|
# The proof-of-possession challenge (contract _popChallenge):
|
|
# keccak256(abi.encode(POP_DOMAIN, chainid, address(this), owner, scheme, pkHash, nonce))
|
|
# Under A2 (keccak injective) two challenges are EQUAL iff ALL seven encoded fields
|
|
# are equal. We model chainid, contract addr, and POP_DOMAIN as fixed (same registry),
|
|
# so a challenge is determined by (owner, scheme, pkHash, nonce).
|
|
# =============================================================================
|
|
def challenge_eq(o1, sc1, pk1, n1, o2, sc2, pk2, n2):
|
|
"""True iff the two _popChallenge inputs collide (== same signed message)."""
|
|
return And(o1 == o2, sc1 == sc2, pk1 == pk2, n1 == n2)
|
|
|
|
# ---- K1 cross-identity: distinct owners -> distinct challenge (message) -------
|
|
# A valid PoP that an attacker OBSERVED is a signature over challenge(O,sc,pk,n).
|
|
# To register the SAME key pk under a different identity O' != O the attacker would
|
|
# need a valid signature over challenge(O',sc,pk,n'). We prove those two messages
|
|
# can NEVER coincide when the owner differs -> under A1 the observed signature is
|
|
# useless for O' (it is a signature over a different message).
|
|
s = Solver()
|
|
o1, o2, sc, pk, n1, n2 = Int('ownerVictim'), Int('ownerAttacker'), Int('scheme'), Int('pkHash'), Int('nonceV'), Int('nonceA')
|
|
s.add(o1 != o2) # different identities
|
|
# adversary reuses the SAME key + scheme, any nonce it likes:
|
|
s.add(challenge_eq(o1, sc, pk, n1, o2, sc, pk, n2)) # claim: the messages collide
|
|
check("K1 cross-identity PoP replay impossible (owner-bound challenge cannot collide)", s)
|
|
|
|
# ---- NEG-CTRL K1: a challenge that OMITS the owner is cross-identity replayable --
|
|
def challenge_eq_NO_OWNER(sc1, pk1, n1, sc2, pk2, n2):
|
|
return And(sc1 == sc2, pk1 == pk2, n1 == n2) # BUG: owner not committed
|
|
s = Solver()
|
|
o1, o2, sc, pk, n = Int('ownerVictim'), Int('ownerAttacker'), Int('scheme'), Int('pkHash'), Int('nonce')
|
|
s.add(o1 != o2)
|
|
s.add(challenge_eq_NO_OWNER(sc, pk, n, sc, pk, n)) # same message for both owners -> replay
|
|
check("NEG-CTRL owner-less challenge lets a PoP be replayed under another identity", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- K2 same-identity replay: nonce advances before store, and is in challenge --
|
|
# _registerWithPoP sets identityNonce[owner] = nonce + 1 BEFORE pushing the key, so
|
|
# the NEXT registration for the same owner requires a signature over challenge(...,n+1),
|
|
# which differs from the just-consumed challenge(...,n).
|
|
s = Solver()
|
|
o, sc, pk, n = Int('owner'), Int('scheme'), Int('pkHash'), Int('nonce')
|
|
s.add(n >= 0)
|
|
# claim the consumed message (nonce n) equals the next required message (nonce n+1):
|
|
s.add(challenge_eq(o, sc, pk, n, o, sc, pk, n + 1))
|
|
check("K2 same-identity replay impossible (nonce n != n+1 -> challenge differs)", s)
|
|
|
|
# also: the nonce STRICTLY increases (monotone, no wrap in the design abstraction)
|
|
s = Solver()
|
|
n = Int('nonce'); s.add(n >= 0); s.add(Not(n + 1 > n))
|
|
check("K2b identity nonce strictly increases on each registration (n+1 > n)", s)
|
|
|
|
# ---- NEG-CTRL K2: a challenge that OMITS the nonce is same-identity replayable ---
|
|
def challenge_eq_NO_NONCE(o1, sc1, pk1, o2, sc2, pk2):
|
|
return And(o1 == o2, sc1 == sc2, pk1 == pk2) # BUG: nonce not committed
|
|
s = Solver()
|
|
o, sc, pk = Int('owner'), Int('scheme'), Int('pkHash')
|
|
s.add(challenge_eq_NO_NONCE(o, sc, pk, o, sc, pk)) # same message across registrations -> replay
|
|
check("NEG-CTRL nonce-less challenge lets the SAME identity replay a PoP", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- K3 a REVOKED (or NONE) key NEVER verifies via verifyWithKey ---------------
|
|
# verifyWithKey: if status in {REVOKED, NONE} return false; else return precompileResult.
|
|
# We let the precompile result be a FREE boolean (adversary picks it, per A1-adversarial
|
|
# modelling) and prove the function still returns false for REVOKED regardless.
|
|
def verifyWithKey(status, precompile_says):
|
|
exists = status != STATUS_NONE # a stored key is never NONE, but model the guard
|
|
gated_out = Or(status == STATUS_REVOKED, status == STATUS_NONE)
|
|
return And(exists, Not(gated_out), precompile_says)
|
|
|
|
s = Solver()
|
|
precompile_says = Bool('precompileSaysValid')
|
|
s.add(verifyWithKey(STATUS_REVOKED, precompile_says)) # claim a revoked key verified true
|
|
check("K3 REVOKED key never verifies (verifyWithKey fail-closed, any precompile output)", s)
|
|
|
|
# sanity: an ACTIVE key CAN verify iff the precompile says so (not vacuous)
|
|
s = Solver()
|
|
precompile_says = Bool('precompileSaysValid')
|
|
s.add(verifyWithKey(STATUS_ACTIVE, precompile_says)) # should be SAT (when precompile true)
|
|
check("K3-sanity ACTIVE key verifies exactly when the precompile accepts (reachable)", s,
|
|
expect_unsat=False, kind="SANITY")
|
|
|
|
# ---- NEG-CTRL K3: a gate that only checks NONE (forgets REVOKED) lets it verify --
|
|
def verifyWithKey_BUG(status, precompile_says):
|
|
return And(status != STATUS_NONE, precompile_says) # BUG: REVOKED not excluded
|
|
s = Solver()
|
|
precompile_says = Bool('precompileSaysValid')
|
|
s.add(verifyWithKey_BUG(STATUS_REVOKED, precompile_says), precompile_says == True)
|
|
check("NEG-CTRL a gate missing the REVOKED check lets a revoked key verify", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- K4 rotation preserves the OWNER BINDING -----------------------------------
|
|
# rotateKey(oldId,...): require old.owner == msg.sender; then _registerWithPoP(msg.sender,...)
|
|
# sets new.owner = msg.sender. So new.owner == old.owner ALWAYS. And old.status <- ROTATED
|
|
# (leaves ACTIVE), so isActiveKey(old) becomes false.
|
|
s = Solver()
|
|
old_owner, sender, new_owner = Int('oldOwner'), Int('msgSender'), Int('newOwner')
|
|
s.add(old_owner == sender) # rotateKey guard: NotKeyOwner unless old.owner == sender
|
|
s.add(new_owner == sender) # _registerWithPoP stores owner = msg.sender
|
|
s.add(Not(new_owner == old_owner)) # negate the binding
|
|
check("K4 rotation preserves owner binding (successor.owner == predecessor.owner)", s)
|
|
|
|
# old key leaves ACTIVE after rotation (becomes ROTATED) -> isActiveKey(old)=false
|
|
s = Solver()
|
|
old_status_after = Int('oldStatusAfterRotate')
|
|
s.add(old_status_after == STATUS_ROTATED)
|
|
s.add(old_status_after == STATUS_ACTIVE) # negate "no longer active"
|
|
check("K4b rotated predecessor is no longer ACTIVE (isActiveKey(old)=false)", s)
|
|
|
|
# ---- NEG-CTRL K4: a rotate that takes an arbitrary owner param breaks the binding -
|
|
s = Solver()
|
|
old_owner, sender, new_owner = Int('oldOwner'), Int('msgSender'), Int('newOwnerParam')
|
|
s.add(old_owner == sender)
|
|
# BUG: successor owner set from an attacker-supplied parameter, not msg.sender
|
|
s.add(new_owner != old_owner)
|
|
check("NEG-CTRL rotate using an arbitrary owner param CAN break the owner binding", 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("AerePQCKeyRegistry:")
|
|
if allok:
|
|
print(" PROVED (under A1 signature-soundness + A2 keccak-injectivity): the PoP")
|
|
print(" challenge binds BOTH the owner (K1: no cross-identity replay) and the")
|
|
print(" per-identity nonce (K2: no same-identity replay), REVOKED keys never verify")
|
|
print(" (K3, for any precompile output), and rotation preserves the owner binding")
|
|
print(" while retiring the old key from ACTIVE (K4). All four NEG-CTRLs fire,")
|
|
print(" confirming the owner field, the nonce field, the REVOKED gate, and the")
|
|
print(" msg.sender-owner assignment are each load-bearing.")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected result above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|