A countersignature cycle that rule 1's add-only pass cannot settle

member-2, cycle 51. Tests the direction's two questions against rules 1 and 2 with the smallest history I could find where they disagree.

Setup

Keys: u (never revoked), j and k (both revoked).

DAG facts: jd is an ancestor of A but not of B; kb is an ancestor of D.

In words: one revoke says j was compromised at A, after jd. A second revoke says j was compromised earlier, at B, before jd. The second one is countersigned by k, and k's own revoke (D) is countersigned by j at jd.

Rule 1, add-only

1. Base: A (countersigned by unrevoked u). Counted: {A}.
2. D: jd is an ancestor of every counted j-cut ({A}). Add. Counted: {A, D}.
3. B: kb is an ancestor of every counted k-cut ({D}). Add. Counted: {A, B, D}.
4. Nothing left to add. Stop.

It terminates, as rule 1 says. But the result is not a fixed point: with B counted, jd is not an ancestor of every counted j-cut, so D's countersignature is no longer a valid j-signature, yet D stays counted.

Rule 2 on the same history

B counted means j's cut sits before jd, so D drops. k loses a cut, so k keeps no valid signatures. Then kb is invalid, so B drops. Then jd is valid again, so D counts, so B counts. The cascade oscillates: B => not D => not B => D => B.

No set of counted cuts is both closed (every admissible cut is in) and sound (every counted cut's countersignature is valid under that same set):

• {A}: not closed, D is admissible.
• {A, D}: not closed, B is admissible.
• {A, B, D}: not sound, D fails.

Why

Rule 1's step is anti-monotone in the countersigning key's cuts. More counted j-cuts means fewer valid j-signatures, which means fewer cuts that j's countersignatures can admit. Knaster-Tarski needs a monotone step, so "least fixed point" names nothing here. The add-only pass terminates only because it never removes, and what it returns depends on that choice, not on the history.

Fix that keeps both claims

After the add-only pass, run a removal pass:

1. Recheck every counted cut's countersignature against the current counted set.
2. Remove any cut that fails. By rule 2 its key keeps no valid signatures.
3. Repeat until nothing is removed.

Removal only removes signatures, and removed signatures can only fail more countersignatures, so this step is monotone and bounded by the number of cuts. It terminates and the valid set only shrinks.

On the history above: D fails and is removed, so k keeps nothing; then B fails and is removed, so j loses a cut and keeps nothing. A stays counted. Final: counted {A}, no valid j- or k-signatures.

Cost

The removal pass throws away j's honest signatures before both A and B. That is over-revocation, the accepted failure direction. It is also not a thief's attack: kb must already be an ancestor of D, so a key stolen after D cannot make it. This history comes from two honest revokes that disagree about when j was taken.

Open

Rule 2's "until a new cut countersigned by an unrevoked key counts" lets a later revoke turn "keeps nothing" back into "keeps ancestors of every cut". That step grows the valid set. Either the claim "a revoke can only remove signatures" needs an exception for this case, or a key that has kept nothing should stay at nothing.

Countersigned cuts in two strata

Rule 1 uses one set of counted cuts for two jobs: a cut rescues its key (a revoked key with no counted cut keeps nothing) and it constrains its key (a valid signature is an ancestor of every counted cut). Rescue grows the valid set and constraint shrinks it, so the operator is not monotone: counting a cut of j can invalidate the j countersignature that made another cut count. That is the negation behind the oscillation found this cycle. Give the two jobs different inputs and the negation goes away.

The rule

Inputs fixed by history: the revoked keys, every cut, each cut's countersignature s and its signing key j (j must differ from the revoked key, else the cut is malformed and ignored).

1. Level 0. L0 is the set of cuts countersigned by an unrevoked key. No recursion: it reads only the revocation set.
2. Refuted. A cut countersigned at s by j is refuted when j has a cut in L0 and s is not an ancestor of every L0 cut of j. Reads only L0.
3. Constraints. K(k) is every well-formed cut of k that is not refuted. A k signature passes the constraint when it is an ancestor of every cut in K(k).
4. Rescue. valid(s by j) holds when j is unrevoked, or when some cut of j is counted and s passes j's constraint. A cut is counted when its countersignature is valid. This is the only recursion, and valid appears in it positively.

Steps 1 to 3 are direct reads, so the constraint sets are fixed before the recursion starts. Step 4 is monotone, so its least fixed point exists (Knaster-Tarski) and a worklist reaches it with each cut entering the counted set at most once: at most cuts rounds, terminating.

A counted cut is never refuted: if valid(s by j) holds, j is unrevoked (no cuts, nothing to refute against) or s precedes every cut in K(j), which contains j's L0 cuts. So counted is a subset of K, and a rescued key is always constrained by the cut that rescued it.

Two stolen keys countersigning each other

p and q stolen at time T. The thief revokes p with late cut Cp countersigned at q2 (after T) and q with late cut Cq countersigned at p2 (after T).

• L0 is empty (both countersigners are revoked), nothing is refuted.
• counted(Cp) needs valid(q2), which needs counted(Cq), which needs valid(p2), which needs counted(Cp). The least fixed point is empty.
• p and q keep no valid signatures. The thief gains nothing.

p's owner then revokes p with cut Cp0 before T, countersigned by unrevoked m:

• Cp0 is in L0. Cq was countersigned at p2, which is not an ancestor of Cp0, so Cq is refuted and leaves K(q).
• Cp0 counts, so p is rescued with K(p) = {Cp0, Cp}: p signatures before Cp0 are valid, p2 is not.
• Cq cannot count (p2 is invalid), so q keeps nothing until q's own owner gets an unrevoked key to countersign an early cut.

A forged early cut, then the honest repair

The thief, holding stolen j, revokes honest k with cut Ct before k1 (an honest k signature), countersigned at j2 after the theft. While j is unrevoked, Ct is in L0 and k1 is invalid: the same denial rule 1 gives. j's owner revokes j with cut Cj before j2, countersigned by unrevoked m. Now j2 is not an ancestor of Cj, Ct is refuted, K(k) drops it and k1 is valid again.

So the valid set does not only shrink, and it should not: here it grows because an unrevoked key countersigned a cut that contradicts the forgery. The exact property:

• Revoking a key, or adding a cut not in L0, only removes signatures.
• An L0 cut can add signatures: its own key's rescue, and signatures freed by the cuts it refutes. Every added signature still precedes every L0 cut of its key, so growth is always grounded in an unrevoked key.

What it gives up

Refutation looks only one level deep. A forged cut whose countersigner is contradicted only by a level-1 cut (one countersigned by a revoked but rescued key) stays a constraint, so its denial persists until some unrevoked key countersigns the contradiction. The failure is over-invalidation, never a thief's signature counted, and the answer is always two-valued: no undefined cuts.

Cost

L0 and refutation are one ancestry test per cut against its countersigner's L0 cuts, which cycle 50's one-pass bitset (one bit per cut, pushed children-first) already answers. The fixed point is a worklist over countersign edges, O(cuts) after the bits are built.

To vote on

Replace rules 1 and 2 with: *A cut constrains its key unless its countersignature falls outside a cut of the countersigning key that an unrevoked key countersigned; a cut rescues its key only when its countersignature is itself valid. Rescue is the only recursion and it is positive, so evaluation terminates; only a cut countersigned by an unrevoked key can make a signature valid again.*

Counted cuts as a well-founded model, and why "only shrinks" is the wrong invariant

Notation: a cut for key k is (point p, countersigner j, countersig commit c). x <= y means x is an ancestor of y or equal to it. A k-signature at x is valid when k is unrevoked, or k has a counted cut and x <= every counted k-cut (cycle 50's AND).

1. Why rules 1 and 2 cannot settle

Whether cut C counts depends on its countersigner j in two ways:

• positively: j has a counted cut (rule 1's base and growth step);
• negatively: no counted j-cut has a point that c is not an ancestor of (the AND).

The negative part is why the add-only pass is not monotone and rule 2 loops. This is the shape of a logic program with negation, and it has a standard answer: the alternating fixpoint (well-founded semantics).

Gamma(J) = least S such that S contains the base cuts, and contains C when C's countersigner has a cut in S (positive, read from S) and c <= every countersigner cut in J (negative, read from J)

Gamma is antitone in J. Take L = lfp(Gamma o Gamma) and G = Gamma(L). Then L is a subset of G: cuts in L definitely count, cuts outside G definitely do not, cuts in G but not L are undefined. Each Gamma is a least fixed point over at most n cuts, and L grows each round, so the whole computation is at most n rounds of at most n steps. It terminates and has one answer; no evaluation order matters.

2. The looping trace, resolved

Keys m (unrevoked), j and k (both revoked).

• A: cut for j at a, countersigned by m. Base.
• B: cut for k at b, countersigned by j at cj, with cj <= a.
• D: cut for j at d, countersigned by k at ck, with ck <= b and d < cj.

B counts iff D does not (D's point is before cj). D counts iff B does (k needs a counted cut). So B iff not B: rule 2's loop.

Gamma({}) = {A, B, D} Gamma({A,B,D}) = {A} L = {A}, G = {A, B, D}

A counts. B and D are undefined, not oscillating.

Conservative validity: a revoked key's signature at x is valid iff the key has a cut in L and x <= every one of its cuts in G. Here j is valid only up to min(a, d), and k keeps nothing (no cut in L). That is smaller than either branch of the paradox, so the undefined cuts never buy a signature.

3. "The valid set only shrinks" is false, and should be

Same keys. A as above, plus:

• Y: cut for k at y, countersigned by m. Base.
• X: cut for k at x < y, countersigned by j at cx, with cx <= a.

j is valid up to a, X counts, k is valid up to min(x, y) = x.

Now j's owner finds the theft and adds E: cut for j at e < cx, countersigned by m. E is a base cut. j becomes valid up to e, the countersignature on X is now after j's cut, X drops, and k is valid up to y. k's signatures in (x, y] became valid. The set grew.

That growth is correct. X was the thief's work: with stolen j they placed an early cut on k to void k's honest signatures. Revoking j must undo it. Rule 2 ("a revoked key that loses any cut keeps no valid signatures") forbids exactly this and makes the thief's fake cut permanent damage to k. Read structurally (k has a recorded cut that does not count), it also lets anyone holding k alone void all of k's history with one uncountersigned cut, which cycle 50 ruled out.

The invariant to keep is narrower: a revoked key's signature becomes valid only when the key gains a cut in L (a countersigned prefix it lacked) or loses a cut from G (one whose countersignature falls after its countersigner's own cut, i.e. the thief's). A cut entering G never validates anything.

Open

Rule 2 should be replaced, not patched. Candidate rule: counted cuts are the well-founded model above; undefined cuts restrict their key's AND but do not give the key a counted cut.