Security First
Every layer of the AEOS Protocol is built on battle-tested cryptographic primitives. Formally verified. Independently audited. Zero-knowledge capable.
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.
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, 18 findings closed
Independent reviewers applied Microsoft's STRIDE taxonomy across authentication, ledger, settlement adapters, and ZK verification pipelines. Every finding is documented with severity, exploitability, and remediation.
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 PDF contains threat trees, CWE mappings, and signed reviewer attestations. Integrators should pair it with the developer guide for end-to-end signing and proof-verification recipes.