Security

WalletPair is designed so that a compromised relay cannot read, forge, or replay application data. The protocol's security properties have been formally verified.

Cryptographic Stack

LayerAlgorithmNotes
Key exchangeX25519Ephemeral keypairs, all-zero/low-order rejection (RFC 7748 §6)
Key derivationHKDF-SHA256Channel ID as salt, domain-separated info strings
EncryptionChaCha20-Poly1305AEAD with type-byte AAD (0x01/0x02/0x03)
Nonce derivationHMAC-SHA256HMAC(traffic_key, seq_bytes)[0:12]
JSON canonical.RFC 8785 (JCS)Deterministic serialization with SHA-256 test vectors
FingerprintSHA256 mod 10000SHA256(prefix || channel_id || dapp_pubkey) mod 10000

Formal Verification

Protocol security is proven with ProVerif under a Dolev-Yao attacker model — the attacker controls the relay and the entire network.

#PropertyResult
1Request confidentiality (dApp → Wallet)Proven
2Response confidentiality (Wallet → dApp)Proven
3Event confidentiality (Wallet → dApp)Proven
4Request authentication (dApp → Wallet)Proven
5Response authentication (Wallet → dApp)Proven
6Event authentication (Wallet → dApp)Proven
7Sealed join handshake authenticationProven

Threat Model

What the relay cannot do:

  • Read encrypted payloads
  • Determine request success or failure
  • Forge peer messages (it lacks traffic keys)
  • Replay messages (sequence counters prevent this)
  • Substitute the wallet's key without detection (sealed join decryption fails)

What the relay can do:

  • Deny service (drop or delay messages)
  • Observe metadata (timing, message sizes, public keys)
  • See dApp meta in plaintext (name, URL, icon)
  • Forge adapter-level messages (e.g., terminate)

Mitigations

  • MITM prevention: The dApp's public key is delivered via QR code (out-of-band physical channel). Session fingerprints provide visual verification.
  • Replay prevention: Monotonic per-peer sequence counters. Write-ahead persistence ensures counter state survives crashes.
  • Reflection attacks: Directional keys (dApp-to-wallet key ≠ wallet-to-dApp key) make reflection impossible.
  • Cross-type confusion: Type-byte AAD (0x01/0x02/0x03) in AEAD prevents a response from being interpreted as a request.
  • Duplicate requests: Wallet idempotency cache keyed on request ID and params hash.