Roots ZKA

The analysis found a key-substitution attack available to a malicious server, which the design named as its primary adversary. The original documents state that the server cannot impersonate users, yet every public key is submitted to and served by that same server with no out-of-band verification. During member onboarding a malicious server can substitute its own key, the admin wraps the family key under it, and the server recovers the key and reads all family content. No member is compromised in the attack.

The envelope construction meets its confidentiality goal, shown two independent ways. The failure is in key distribution. A strengthened handoff, named Heirloom, adds a key-transparency log and authenticated delivery, and it is machine-verified to close both variants of the attack (extraction and injection, detailed below).

Messaging protocols like Signal are designed for forward secrecy: someone who joins a conversation should not be able to read messages sent before they arrived, and keys are discarded once they are no longer needed. Roots has the opposite requirement. It gives family members a permanent archive, so a member who joins in 2030 is expected to read photos shared in 2024. Its key distribution therefore has to hand new members the keys to content that predates them. Much of this analysis concerns what that requirement costs and whether the original design met it securely.

Content is protected with envelope encryption. Each post is sealed with its own fresh key, and that key is wrapped under a per-family epoch key that rotates to a new epoch when a member leaves. The epoch key is guarded by a master key, and the master key is recovered from a mnemonic, with a password unlocking a stored copy.

The design composes standard primitives (X25519 key agreement, Ed25519 signatures, AES-GCM and AES-KW, Argon2id for the password path). Nothing cryptographically novel is invented; the risk, and the subject of this analysis, lives in the composition and key distribution.

The server never holds any of this in the clear. It stores and routes ciphertext, wrapped key bundles, and blind-index tags, and can read none of them. That is what "zero-knowledge" means here: the server has zero knowledge of content, the vendor sense of the term rather than zero-knowledge proofs.

The break is in how a new member receives the family key. In v1 the admin takes the newcomer's public key from the server with no verification, so a malicious server can substitute its own key (extraction) or forge a handoff to an honest newcomer (injection). Both attacks need no member to be compromised.

Heirloom, the strengthened handoff, fixes this in two parts: the newcomer's key is taken from an append-only transparency log the newcomer can audit, and the handoff is signed and verified against the admin's logged key. Authenticating only the newcomer's key is not enough, and that insufficiency is itself machine-checked, so both parts are necessary.

Every claim is machine-checked in Tamarin, and the envelope core is also covered by a hand-written game-based reduction. The reconstructed v1 is left broken on purpose; the v2 rows are the Heirloom fix. The Tamarin results hold in the symbolic model, which assumes the primitives are perfect; the game-based reduction covers the envelope core computationally but is hand-written, not mechanized.

The v1 attack and the v2 defense run as ordinary tests. One test asserts that the attack succeeds; the others show the same adversary failing against Heirloom.

cd impl
cargo test          # 14 tests: standard vectors, envelope obligations, attack, fix

The proofs re-check with Tamarin 1.12 or later.

tamarin-prover --prove model/v1_core.spthy                  # envelope confidentiality
tamarin-prover --prove=handoff_key_secrecy model/v1.spthy   # the break (falsified)
tamarin-prover --prove model/v2.spthy                       # the fix (verified)

An independent formal-methods study of a system I designed. The encryption layer was fully designed and partially built for Roots, then scrapped before the primitives were implemented for real. This project reconstructs it precisely, states its security goals as formal claims, and either proves them or breaks them. It contains no application code and no secrets, and it is an analysis artifact rather than audited cryptographic software.