Repository navigation
0.5.228: add a device — a new device joins its owner's identity peer to peer (#177) - #786
Merged
Merged
Conversation
…-contact plane) model-checked with TLC Models a new device B joining as an occurrence of its owner's identity through the owner's existing device A, peer to peer on edge's first-contact opaque plane (CIRISEdge#683, kind 0x0000_0002), against an adversary with unlimited fresh keys that sees every request and injects any answer but cannot forge signatures. Five configurations: safety (8 invariants, 211,849 states, no error), careless owner (Inv_NoAttackerOwned violated — the receiver-derived matching code is load-bearing), liveness (holds), sybil flood without fair admission (liveness violated — availability-only residual), sybil with fair eviction (holds). Found: an answered request must free its pending slot, or a denied flood starves B. README records verdicts and the implementation requirements. For CIRISConstitution review (Eric's ask, 2026-10-16). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WW3mUN8f2rUCYJVmyLwHGb
…, the code's load is the normative receiver derivation), owner presence named as the liveness assumption, a closed window refuses with no answer (CC review) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WW3mUN8f2rUCYJVmyLwHGb
…he owner consents on the existing device (CIRISServer#177) The first-run wizard's "Add device" on B takes the person's fedID (QR, long form or short form) and sends a device-join request over edge's first-contact opaque plane (CIRISEdge#683, kind 0x0000_0002), signed by B's node key. A holds it only while the owner has opened "Add a device"; both screens show a matching code A derives from (B's key, challenge). On approve, the owner pen on A signs owner -> B and B's occurrence (persist's content-only form), records both and re-wraps the self DEKs to B. B applies the binding through its own /v1/setup/root (its claim PIN still proves local presence) and stores the occurrence. B mints its own keys; no key material crosses. - FSD/ADD_DEVICE.md: flow, N1-N6, surfaces, refusal ids. - src/add_device.rs: wire types, A's answerer and owner routes, B's setup routes and poll; per-sender, ceiling and closed-window refusals; a decided request frees its slot at once (TLC finding, formal/add_device). - compose: edge gets the federation directory. First contact was dead in the server without it. - owner capsule: an active occurrence of the owner opens it, so B's self room and owner flows work on the occurrence key. - B's device keys use the default device custody (ML-DSA half sealed), so its pen opens through the normal signer path. - harness: `python -m harness.native add_device` passes end to end: closed window refused, two requesters with distinct codes, approve B, B applied and in session, occurrence on both nodes, A's self file opens on B, the stranger denied. - the eleven add_device.* ids are queued for the client bundle; ratchet 19 -> 30. approve is named in SESSION_CLAIMS §2.3 as a re-wrap caller. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WW3mUN8f2rUCYJVmyLwHGb
…784), the contacts batch (#785) Cargo.toml names the next tag (v0.5.227 is on 21869a6); the evidence rows follow it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WW3mUN8f2rUCYJVmyLwHGb
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
…gned occurrence at millisecond precision, like compose's Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WW3mUN8f2rUCYJVmyLwHGb
# Conflicts: # Cargo.toml # harness/native/scenarios.py
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add a device (CIRISServer#177)
A new device joins its owner's identity, peer to peer. The owner consents on the existing device. Spec:
FSD/ADD_DEVICE.md. Model:formal/add_device(TLC, five configs).0x0000_0002), signed by its node key. No owner is needed to send it./v1/setup/root, so its claim PIN still proves local presence.Also fixed
Release
add_device.*refusal ids are queued for the client bundle, with their English in the FSD. The ratchet goes from 19 to 30.Tests
python -m harness.native add_devicepasses end to end. The closed window refuses, two requesters get distinct codes, B is approved, applied and in session, the occurrence exists on both nodes, A's self file opens on B, and the stranger is denied.-D warningsall pass locally.🤖 Generated with Claude Code
https://claude.ai/code/session_01WW3mUN8f2rUCYJVmyLwHGb