Security First
Every layer of the AEOS Protocol is built on standard cryptographic primitives with published references. Contract escrow and PBFT safety are modelled in TLA+; the protocol is reviewed against a STRIDE threat model and a recorded adversary; range statements are zero-knowledge.
Cryptographic primitives
A single surface, many proofs
The protocol composes standards-aligned algorithms with explicit security parameters. Below is the complete primitive lattice used in production code paths.
Signatures
Ed25519 (RFC 8032) · PyNaCl / cryptography
2^128 classical security level; deterministic signatures eliminate RNG failure modes in signing paths.
Commitments
SHA-256 Pedersen-style · blinding factors
Perfectly hiding under uniform randomness; computationally binding under collision resistance of the hash function.
Key derivation
HKDF-SHA256 (RFC 5869)
Extract-and-expand yields deterministic child keys from high-entropy root material with domain separation labels.
Encryption
AES-256-GCM
NIST-approved AEAD; 256-bit key space; authentication tag binds ciphertext to associated data at API boundaries.
VRF
Ed25519-based VRF construction
Pseudorandom output verifiable against a public key; provably fair arbitrator sampling and lottery-style selection.
Merkle trees
SHA-256 · domain-separated leaves vs internals
O(log n) inclusion proofs; explicit domain tags prevent second-preimage ambiguity across tree levels.
Secret sharing
Shamir over GF(L) · Lagrange interpolation
Information-theoretic threshold security: fewer than t shares reveal zero information about the secret polynomial constant.
Threshold signatures
t-of-n via polynomial evaluation
No single party holds the full signing key; quorum reconstructs only the evaluation needed for a collective signature.
Range proofs
Bulletproofs · Ristretto255 · Merlin transcripts · Rust FFI
Zero-knowledge proofs that a committed value lies in [0, 2^n) with logarithmic proof size in the bit-length n.
Consensus
PBFT · Ed25519 quorum certificates
Byzantine fault tolerance under f < n/3; quorum certificates cryptographically bind committed sequence numbers to values.
Post-quantum seals
ML-DSA-87 (FIPS 204) · hybrid with Ed25519 · Phanes ID
Every Phanes ID artefact carries a lattice signature next to the Ed25519 one over the same bytes; verifiers can require it and refuse classical-only tokens. Two independent implementations cross-check each other in the test suite.
Holder-signed requests
Ed25519 over canonical JSON · nonce cache · purpose-bound domains
Every state-changing route is signed by the ID’s holder key over method, path, timestamp, nonce and body hash; contract terms, evidence and votes carry a second signature with its own domain, made on the agent’s machine. The registry never holds a holder key.
Signed inspection
EdDSA JWS · ML-DSA-87 seal · integers only · verified in the browser
The per-agent report is signed by the registry and sealed post-quantum; phanes.app/inspect verifies it under the issuer key from its own origin, re-checks every ledger inclusion proof and every PBFT anchor, and renders only the verified payload.
Formal verification
TLA+ models you can reason about
State machines for escrow and consensus are specified in TLA+ and checked with TLC over finite instances to surface invariant violations before they ship.
\* States: idle, funded, disputed, released, slashed VARIABLES funds_in_escrow, outstanding_obligations, phase TypeInvariant == funds_in_escrow \in Nat EscrowFunding == /\ phase = "idle" /\ phase' = "funded" /\ funds_in_escrow' = funds_in_escrow + deposit \* No silent fund loss on honest transitions Conservation == funds_in_escrow >= outstanding_obligations
\* Quorum intersection enforces single commitable value
Safety ==
\forall r1, r2 \in HonestReplicas :
committed[r1] # {} /\ committed[r2] # {}
=> \exists v : committed[r1] = {v} /\ committed[r2] = {v}
Liveness ==
Eventually (\forall r \in HonestReplicas : committed[r] # {})
\* Certificates are Ed25519-attested message sets
QCIntegrity == \A qc \in QuorumCerts : VerifySig(qc)Safety property
No two honest replicas commit different values for the same sequence number: intersecting quorums force agreement on the hash-linked request block.
Liveness property
Under eventual partial synchrony and f < n/3, all honest replicas eventually commit pending client requests without perpetual lockout.
Contract invariant
funds_in_escrow >= outstanding_obligations holds on every reachable escrow state; release and slash transitions preserve solvency.
Security audit
STRIDE threat model, 24 findings, 5 fixed and 10 mitigated
The project's own review applies the STRIDE taxonomy across every surface: identity, admission, the registry's routes, ledger and consensus, payments, recognition, oversight, witnesses and publication. Every finding carries a severity, a status checked against the code, where to check it, and a recommendation; 8 are acknowledged with their limit stated and 1 is open.
Spoofing
Identity binding, API authentication, and cross-agent impersonation surfaces.
Tampering
Ledger integrity, message malleability, and state-transition invariants under adversarial reordering.
Repudiation
Non-repudiation of signed protocol events and dispute-evidence retention policies.
Information disclosure
Selective disclosure, side channels in crypto APIs, and log redaction across services.
Denial of service
Rate limits, consensus liveness under flood, and resource exhaustion in proof verification.
Elevation of privilege
Authorization boundaries between agents, operators, and settlement adapters.
Categories: Spoofing · Tampering · Repudiation · Information disclosure · DoS · Elevation
Zero-trust architecture
Verify, then trust the math
Cryptographic proof per operation
Business logic gates on verifiable artifacts: signatures, Merkle paths, and ZK statements—not on IP allow lists alone.
No implicit inter-agent trust
Each agent is modeled as potentially Byzantine; honest behavior is enforced by protocol rules and attestations, not goodwill.
Signature verification at every API boundary
Ingress and egress paths validate Ed25519 over canonical serialized payloads; rejects are auditable and fail closed.
Merkle proofs for data integrity
Replicas and clients reconcile state against committed roots; tampered subtrees cannot satisfy verification equations.
Hash chain for tamper detection
Append-only ledger links entry hashes; fork detection reduces to comparing chain tips and certificate histories.
Circuit breakers for anomaly response
Risk engine hooks halt high-value flows when score thresholds or proof-verification failure rates spike.
Bulletproofs deep dive
Rust core, Python boundary
Range proofs are too hot for a pure Python path: scalar multiplications and multi-exponentiations dominate CPU time. The AEOS implementation keeps the proof system in Rust for performance and memory safety, exposing a narrow ctypes FFI surface to the orchestration layer.
Ristretto255 group law
Prime-order subgroup of Curve25519 with cofactor elimination; avoids small-subgroup attacks and simplifies protocol assumptions.
Merlin transcripts
Fiat-Shamir challenges are bound to a STROBE-based transcript so prover and verifier hash identical label-ordered data.
Range statement
Prover convinces verifier that a committed Pedersen opening lies in [0, 2^n) without revealing the value—logarithmic proof size in n.
Python FFI via ctypes
Shared library exports verify_proof, prove_range, and buffer management helpers; Python passes only byte strings and scalar encodings.
passing tests · Rust + Python harness
- [pass]Round-trip prove/verify on random witnesses
- [pass]Transcript mismatch rejection (negative cases)
- [pass]FFI boundary stress with oversized buffers
- [pass]Cross-platform shared library load paths
Inner product argument + aggregated range proofs follow Bulletproofs; constants match the Ristretto255 generator setup in Merlin-backed challenge derivation.
Inspect the evidence chain
The audit names every finding, its status and where that status can be checked, and reads the adversary's matrix from the recorded evidence run. It is the project's own review, not a third-party audit; that remains the next step before adversarial, multi-operator deployment.