4a0b48588c
Aere Network public source. Everything here can be checked against the live chain (chain id 2800, https://rpc.aere.network). Scope note, stated up front rather than buried: consensus on chain 2800 is classical secp256k1 ECDSA QBFT. The post-quantum work in this repository is at the signature, precompile, account and transport layers. Nothing here makes the consensus post-quantum, and no document in it should be read as claiming so.
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)
|