How Verifpal Finds a 3-of-5 Threshold-Signature Forgery

Verifpal 1.4.4 adds direct support for threshold cryptography. The most useful way to explain it is through one of the models that shipped with the release: threshold_sign_three_of_five_two_oracles.vp.

The model sits exactly on a 3-of-5 boundary. A dealer splits a signing key into five shares. Alice, Bob and Carol participate in one signing session. A fourth share has leaked. An active network attacker can turn Alice and Bob into signing oracles, but Carol’s signing request is authenticated. Neither failure is enough on its own: one leaked share is below the threshold, and two oracle-produced partial signatures are below the threshold. Together they make three.

Verifpal finds a valid signature on the attacker’s message while still reporting that both the group key and Alice’s share remain confidential:

PASS + confidentiality? k
PASS + confidentiality? s1
FAIL x authentication? Coordinator -> Verifier: sig

That separation is the point of the model. The attacker does not recover the private key and does not steal three shares. It obtains three distinct contributions to one signature.

A five-share key with a threshold of three

The model starts with an active attacker and a trusted dealer:

attacker[active]

principal Dealer[
	knows private psk_a
	knows private psk_b
	knows private psk_c
	generates k
	pk = PUBKEY(k)
	s1, s2, s3, s4, s5 = THRESHOLD_SPLIT[3](k)
	generates nd_a
	ea = AEAD_ENC(psk_a, nd_a, s1, pk)
	generates nd_b
	eb = AEAD_ENC(psk_b, nd_b, s2, pk)
	generates nd_c
	ec = AEAD_ENC(psk_c, nd_c, s3, pk)
	leaks s4
]

The number in THRESHOLD_SPLIT[3] is the threshold. The number of outputs on the left is the total number of shares, so this assignment is 3-of-5. Any three distinct shares can reconstruct k; two reveal nothing. Verifpal accepts thresholds from two up to the number of shares, with at most sixteen shares in one split.

This replaces the old SHAMIR_SPLIT primitive, which only represented a fixed 2-of-3 split. The threshold is now part of the term’s identity. A share from THRESHOLD_SPLIT[2](k) and one from THRESHOLD_SPLIT[3](k) are not interchangeable, even when both splits name the same secret. Repeating one share does not increase the count either.

The dealer gives s1, s2 and s3 to Alice, Bob and Carol under separate pre-shared keys:

Dealer -> Alice: [pk], nd_a, ea
Dealer -> Bob: [pk], nd_b, eb
Dealer -> Carol: [pk], nd_c, ec
Dealer -> Coordinator: [pk]
Dealer -> Verifier: [pk]

Square brackets make a value guarded: the attacker sees pk but cannot replace it in transit. The shares themselves are inside authenticated encryption, and the group public key is associated data. Binding each encrypted share to pk prevents a share package from being replayed into a different group-key setup. The pre-shared keys stand in for the mutually authenticated secure channel required by RFC 9591’s trusted-dealer procedure.

The deliberate compromise is leaks s4. The attacker now owns one valid signing share. s5 is neither distributed nor leaked. At this point the group key remains safe: one share is still two short of the reconstruction threshold.

Round one: nonce commitments

Each active participant opens their share package, generates a fresh nonce and publishes a commitment:

principal Alice[
	knows private psk_a
	sa = AEAD_DEC(psk_a, nd_a, ea, pk)?
	generates na
	ca = PUBKEY(na)
]

principal Bob[
	knows private psk_b
	sb = AEAD_DEC(psk_b, nd_b, eb, pk)?
	generates nb
	cb = PUBKEY(nb)
]

principal Carol[
	knows private psk_c
	sc = AEAD_DEC(psk_c, nd_c, ec, pk)?
	generates nc
	cc = PUBKEY(nc)
]

Alice -> Coordinator: ca
Bob -> Coordinator: cb
Carol -> Coordinator: cc

The ? on each AEAD_DEC makes successful decryption a condition for continuing. A forged share package does not become a malformed share inside the signing protocol; the participant stops.

In FROST, a participant generates a hiding nonce and a binding nonce, then publishes their two commitments in round one. Verifpal compresses that pair into one secret nonce and represents its public commitment as PUBKEY(nonce). The nonces remain local; ca, cb and cc can travel over the public network.

These commitments matter to the symbolic rule. Partial signatures combine only when they refer to distinct shares from the same split and agree on both the commitment list and the message. A partial from another signing session cannot simply be added to the set.

Two participants become signing oracles

The coordinator chooses a message and distributes the round-two inputs:

principal Coordinator[
	generates m
]

Coordinator -> Alice: m, cb, cc
Coordinator -> Bob: m, ca, cc
Coordinator -> Carol: [m], [ca], [cb]

The asymmetry is intentional. Carol receives the message and the other commitments in brackets, so the active attacker cannot replace them. Alice and Bob receive the same values without guards. The attacker can therefore choose what Alice and Bob are asked to sign while Carol continues to see the coordinator’s real message.

This is an application-level authorization assumption, not a claim that FROST makes the message secret. RFC 9591 says that applications should validate inputs so that participants do not become signing oracles for arbitrary messages. In this model, the brackets express that validation or an authenticated delivery mechanism; their absence expresses what happens without it.

The participants assemble the same ordered commitment list and produce their partial signatures:

principal Alice[
	cl_a = CONCAT(ca, cb, cc)
	pa = THRESHOLD_SIGN(sa, na, cl_a, m)
]

principal Bob[
	cl_b = CONCAT(ca, cb, cc)
	pb = THRESHOLD_SIGN(sb, nb, cl_b, m)
]

principal Carol[
	cl_c = CONCAT(ca, cb, cc)
	pc = THRESHOLD_SIGN(sc, nc, cl_c, m)
]

THRESHOLD_SIGN(share, nonce, commitments, message) is the new partial-signature primitive. In the honest execution, all three partials agree on m and on the commitment list, so they can be joined.

In the attack execution, Alice and Bob receive the attacker-known value nil in place of m. Their outputs resolve to partials over nil. Carol’s message is guarded, so her partial remains bound to the honest m and cannot be combined with theirs. The commitment list is also part of every partial, preventing the attacker from mixing otherwise unrelated signing sessions.

Calling Alice and Bob “oracles” does not mean their shares have leaked. The attacker supplies a signing request and receives a partial signature in response. It still cannot extract s1 from Alice’s partial or s2 from Bob’s.

The leaked share supplies the third partial

The attacker now has two partial signatures on nil, one under s1 and one under s2. It also has s4, the share leaked by the dealer. Because the commitment values and the chosen message are public, it can produce its own third partial under that share. In Verifpal’s abstraction, that term is THRESHOLD_SIGN(s4, nil, cl_a, nil).

The nonce position is allowed to differ across partials; the share, commitment list and message are what determine whether they form a valid threshold set. A concrete FROST participant would generate fresh nonce material and place the corresponding commitment in the participant list, which Alice and Bob’s unguarded commitment inputs allow the attacker to do. The minimized symbolic trace uses nil for attacker-chosen nonce material because its actual value does not affect the protocol-level result.

There are now three contributions tied to three distinct outputs of the same split:

THRESHOLD_JOIN performs the symbolic Lagrange interpolation. Since the threshold is three and all three partials agree on the commitment list and message, the join reduces to the ordinary signature SIGN(k, nil). The attacker obtains that signature without first obtaining k.

The core of Verifpal’s trace is explicit:

Attacker observes THRESHOLD_SIGN(s1, na, cl_a, nil) on the wire.
Attacker observes THRESHOLD_SIGN(s2, nb, cl_a, nil) on the wire.
Attacker is handed s4 by a leaks declaration.
Attacker constructs cl_a from the public commitments.
Attacker combines SIGN(k, nil) out of the partial signatures
THRESHOLD_SIGN(s1, na, cl_a, nil),
THRESHOLD_SIGN(s2, nb, cl_a, nil), and
THRESHOLD_SIGN(s4, nil, cl_a, nil).

The honest coordinator would normally aggregate Alice, Bob and Carol’s partials, check the result, and publish it:

principal Coordinator[
	sig = THRESHOLD_JOIN(pa, pb, pc)
	_ = SIGNVERIF(pk, m, sig)?
]

Coordinator -> Verifier: m, sig

principal Verifier[
	_ = SIGNVERIF(pk, m, sig)?
]

Instead, the attacker replaces the final pair with nil, SIGN(k, nil). The verifier evaluates SIGNVERIF(pk, nil, SIGN(k, nil))?, which succeeds. A joined threshold signature is deliberately the same symbolic value as a signature produced directly under k; the verifier does not need a separate algorithm and does not learn which subset of shares produced it.

This contradicts authentication? Coordinator -> Verifier: sig because the accepted signature came from the attacker, not the coordinator. Both confidentiality queries still pass. A signature under k does not disclose k, and the oracle partial under s1 does not disclose s1.

The two counterexamples that do not cross the threshold

Two companion models pin the boundary from either side:

The first two rows are Pass results under Verifpal’s bounded analysis at the default two sessions per principal. They mean that the search found no attack within that envelope, not that the protocols are proved secure. The third row is a concrete attack witness. Repeating either oracle’s partial does not help, because THRESHOLD_JOIN counts distinct shares, and a partial from a different split or over a different message does not join.

What else the threshold primitives cover

The same rules extend beyond this example. THRESHOLD_JOIN has three related meanings:

• Enough distinct raw shares reconstruct the shared secret.
• Enough PUBKEY(share) values interpolate to PUBKEY(k), which models deriving the group public key from public verification shares.
• Enough THRESHOLD_SIGN values over the same commitments and message produce SIGN(k, message).

Nonce failure is modeled too. If one participant uses the same nonce with the same share for two different partial signatures, Verifpal gives that share to the attacker. The separate threshold_sign_nonce_reuse.vp model exercises that rule; its fresh-nonce counterpart does not report the compromise. This follows RFC 9591’s nonce-reuse warning, represented through the same one-nonce abstraction used in the signing model.

The boundary of the claim matters. Verifpal is not implementing a FROST ciphersuite, checking curve arithmetic, or verifying code. THRESHOLD_SPLIT models dealer-based sharing rather than the algebra of a distributed key-generation ceremony, and one symbolic nonce stands for FROST’s hiding-and-binding pair. What the model can test is the protocol composition around those operations: share distribution, message authorization, commitment agreement, signing-oracle access, aggregation, leakage and reuse.

That is what makes this example useful. A leaked share and an exposed signing oracle are different failures, and neither breaks this 3-of-5 design alone. The attack appears only when those capabilities are counted together. Verifpal 1.4.4 can now do that counting itself and return the signature that crosses the threshold.