Summary
auths_verifier::duplicity::detect_duplicity is correct and well-tested, but in the default
verification path — and even under --require-witnesses — it is fed a single view of a KEL,
where it structurally cannot fire. True cross-observer equivocation is only detected on the opt-in
cross-source path (--remote) or by ad-hoc local scanning (auths status).
This is a defense-in-depth / assurance gap, not a crypto vulnerability, and it is adjacent to the
documented kt=1 accepted risk. But the mitigation language in docs/architecture/multi_device_accepted_risks.md
("detect_duplicity surfaces the divergence") overstates what happens by default: a duplicity detector
only does work when two independent views are brought together, which the default and witnessed paths
do not do.
Formal background (Lean 4 proofs)
A short series of machine-checked proofs (developed alongside this analysis; currently local artifacts
under network_proof/ and timeline_proof/, could be committed for posterity) pins down why two views
are required. Each builds clean with lake build, zero sorry, and surfaces its trust base via
#print axioms:
timeline_proof/TimelineProof/Ordering.lean
signature_insufficiency (Thm 1): no detector that sees only a single observation can decide
whether an equivocation occurred — the same observed event lives in both an honest world [c] and an
equivocating one [c, c']. #print axioms → [propext] only.
dag_detects_fork / link_necessary (Thm 2): a hash-linked log makes a fork detectable on
comparison of two views, clock-free and ledger-free; flat (issuer, seq) data conflates histories
the hash-link separates.
timeline_proof/TimelineProof/Prevention.lean
no_blind_rule_prevents (zero axioms): a purely-local rule cannot prevent split-brain.
selector_prevents: prevention becomes possible only with a shared canonical selector — i.e. a witness.
timeline_proof/TimelineProof/Synchrony.lean
echo_prevents_split_brain / async_echo_still_splits: under synchrony + peer echo you can prevent
without a trusted witness, but without the timing assumption you are back to needing one.
network_proof/ — transferable_needs_signature: signatures are the minimal primitive for offline,
third-party authenticity (the layer below this issue, already satisfied by auths).
Operative consequence: detection is a function of comparing two views; one view can never detect a fork.
What the code does today
-
Commit path — the check cannot fire. crates/auths-verifier/src/commit_kel.rs:
verify_commit_against_kel_witnessed_at replays the root KEL first (~line 613) and returns
RootKelInvalid on failure; detect_duplicity runs afterward, inside authorize_commit (~line 784),
on that same, already-linearized KEL. A KEL that survived replay is linear, so this call cannot
return Diverging.
-
Credential path — a guard, not a detector. crates/auths-verifier/src/credential.rs:297 runs
detect_duplicity before replay, so it can fire — but only if the issuer KEL blob handed in is
already internally forked. It never fetches a second view, so it catches "this KEL is internally
inconsistent," not "this identity equivocated to a different observer." It is fail-closed
(IssuerKelDuplicitous), a verdict largely unreachable in single-source verification.
-
Org bundle — flag on a single source. crates/auths-verifier/src/org_bundle/verify.rs:287 flags
duplicity on the single org_kel; same single-view limitation.
-
The only genuine cross-observer check is opt-in. crates/auths-sdk/src/keri/resolver.rs:251
(cross_source_fork) merges local + remote and runs detect_duplicity over the union — correct and
fail-closed — but only when --remote is supplied.
-
--require-witnesses counts, it does not compare. The witness gate (commit_kel.rs:627-663)
decides on collected >= required receipts stored locally. It proves "M-of-N designated witnesses
signed this event"; it does not fetch an independent witness view and check whether witnesses
signed a different event at the same sequence. The watcher/monitor that would do that
(auths-monitor) exists as a standalone service but is not wired into verification.
Why it matters
multi_device_accepted_risks.md frames the kt=1 fork risk as "mitigated: detect_duplicity surfaces
the divergence." In practice the divergence is surfaced only when two independent views are deliberately
combined — neither the default path nor --require-witnesses does this. A user enabling witnesses could
reasonably believe they are protected against equivocation when they are getting receipt-quorum /
availability, not cross-view fork detection.
Proposed work (ranked)
- Close the second-view loop for witnessed verification (highest leverage). When
--require-witnesses
is on, fetch an independent witness/watcher view of the relevant KEL and run detect_duplicity
across the two views — turning "witnesses are available" into "witnesses agree." This is the change
the formal result points directly at, and it makes the detector do real work for users who opt into
witnesses.
- Resolve the dead / near-dead in-path calls. Move the commit-path
detect_duplicity before replay
(so it can fire on a forked input) or remove it; document the credential-path call as an
internal-consistency guard, not equivocation detection. Dead defensive code that reads as protection is
a false-assurance hazard.
- Tighten the accepted-risk doc to state precisely when divergence is surfaced (cross-source
--remote / accumulated local refs / witnessed-with-second-view), so the mitigation is not overstated.
Scope / non-goals
- Not a crypto vulnerability; the detector, signature checks, and replay logic are correct.
- Consistent with the documented "no witnesses by default" accepted risk — this issue is about closing the
gap between that doc's mitigation language and the implemented behavior, and making duplicity detection
real for users who opt into witnesses.
- The Byzantine version of "two views meet" lands on a permissioned witness quorum, not a blockchain;
keeping witnessing permissioned is the relevant invariant (open membership would import Sybil resistance,
which is what would force a chain).
Confidence
- High (read directly from source): the commit-path call is post-replay and cannot return
Diverging;
--require-witnesses is a receipt count, not a cross-view comparison.
- Inferred (worth a quick confirm before acting): the credential-path
issuer_kel cannot arrive
multi-source in normal verification.
Summary
auths_verifier::duplicity::detect_duplicityis correct and well-tested, but in the defaultverification path — and even under
--require-witnesses— it is fed a single view of a KEL,where it structurally cannot fire. True cross-observer equivocation is only detected on the opt-in
cross-source path (
--remote) or by ad-hoc local scanning (auths status).This is a defense-in-depth / assurance gap, not a crypto vulnerability, and it is adjacent to the
documented
kt=1accepted risk. But the mitigation language indocs/architecture/multi_device_accepted_risks.md("
detect_duplicitysurfaces the divergence") overstates what happens by default: a duplicity detectoronly does work when two independent views are brought together, which the default and witnessed paths
do not do.
Formal background (Lean 4 proofs)
A short series of machine-checked proofs (developed alongside this analysis; currently local artifacts
under
network_proof/andtimeline_proof/, could be committed for posterity) pins down why two viewsare required. Each builds clean with
lake build, zerosorry, and surfaces its trust base via#print axioms:timeline_proof/TimelineProof/Ordering.leansignature_insufficiency(Thm 1): no detector that sees only a single observation can decidewhether an equivocation occurred — the same observed event lives in both an honest world
[c]and anequivocating one
[c, c'].#print axioms→[propext]only.dag_detects_fork/link_necessary(Thm 2): a hash-linked log makes a fork detectable oncomparison of two views, clock-free and ledger-free; flat
(issuer, seq)data conflates historiesthe hash-link separates.
timeline_proof/TimelineProof/Prevention.leanno_blind_rule_prevents(zero axioms): a purely-local rule cannot prevent split-brain.selector_prevents: prevention becomes possible only with a shared canonical selector — i.e. a witness.timeline_proof/TimelineProof/Synchrony.leanecho_prevents_split_brain/async_echo_still_splits: under synchrony + peer echo you can preventwithout a trusted witness, but without the timing assumption you are back to needing one.
network_proof/—transferable_needs_signature: signatures are the minimal primitive for offline,third-party authenticity (the layer below this issue, already satisfied by auths).
Operative consequence: detection is a function of comparing two views; one view can never detect a fork.
What the code does today
Commit path — the check cannot fire.
crates/auths-verifier/src/commit_kel.rs:verify_commit_against_kel_witnessed_atreplays the root KEL first (~line 613) and returnsRootKelInvalidon failure;detect_duplicityruns afterward, insideauthorize_commit(~line 784),on that same, already-linearized KEL. A KEL that survived replay is linear, so this call cannot
return
Diverging.Credential path — a guard, not a detector.
crates/auths-verifier/src/credential.rs:297runsdetect_duplicitybefore replay, so it can fire — but only if the issuer KEL blob handed in isalready internally forked. It never fetches a second view, so it catches "this KEL is internally
inconsistent," not "this identity equivocated to a different observer." It is fail-closed
(
IssuerKelDuplicitous), a verdict largely unreachable in single-source verification.Org bundle — flag on a single source.
crates/auths-verifier/src/org_bundle/verify.rs:287flagsduplicity on the single
org_kel; same single-view limitation.The only genuine cross-observer check is opt-in.
crates/auths-sdk/src/keri/resolver.rs:251(
cross_source_fork) merges local + remote and runsdetect_duplicityover the union — correct andfail-closed — but only when
--remoteis supplied.--require-witnessescounts, it does not compare. The witness gate (commit_kel.rs:627-663)decides on
collected >= requiredreceipts stored locally. It proves "M-of-N designated witnessessigned this event"; it does not fetch an independent witness view and check whether witnesses
signed a different event at the same sequence. The watcher/monitor that would do that
(
auths-monitor) exists as a standalone service but is not wired into verification.Why it matters
multi_device_accepted_risks.mdframes thekt=1fork risk as "mitigated:detect_duplicitysurfacesthe divergence." In practice the divergence is surfaced only when two independent views are deliberately
combined — neither the default path nor
--require-witnessesdoes this. A user enabling witnesses couldreasonably believe they are protected against equivocation when they are getting receipt-quorum /
availability, not cross-view fork detection.
Proposed work (ranked)
--require-witnessesis on, fetch an independent witness/watcher view of the relevant KEL and run
detect_duplicityacross the two views — turning "witnesses are available" into "witnesses agree." This is the change
the formal result points directly at, and it makes the detector do real work for users who opt into
witnesses.
detect_duplicitybefore replay(so it can fire on a forked input) or remove it; document the credential-path call as an
internal-consistency guard, not equivocation detection. Dead defensive code that reads as protection is
a false-assurance hazard.
--remote/ accumulated local refs / witnessed-with-second-view), so the mitigation is not overstated.Scope / non-goals
gap between that doc's mitigation language and the implemented behavior, and making duplicity detection
real for users who opt into witnesses.
keeping witnessing permissioned is the relevant invariant (open membership would import Sybil resistance,
which is what would force a chain).
Confidence
Diverging;--require-witnessesis a receipt count, not a cross-view comparison.issuer_kelcannot arrivemulti-source in normal verification.