Documentation / Writing security queries

Writing security queries

Choose precise security claims, understand acceptance and replay, and interpret the five Verifpal queries.

The reference defines the five queries and their syntax. This guide develops successful use and matching runs, gives the exact unlinkability witness conditions, and works through acceptance and replay examples.

For a confidentiality claim, distinguish the original secret from a received or computed replacement. The accepted-key example shows why a query on a discarded key can fail while the key actually used by the client remains secret.

Successful use and matching runs

The authentication predicate depends on two precise notions: successful use by the recipient and a matching sender run.

For authentication? Alice -> Bob: e1, let $U$ be the set of slots that Bob himself computes whose value mentions e1 at any depth. Bob successfully uses e1 when the explored execution reaches every slot in $U$ and at least one of them carries a primitive that has no rewrite rule, is left unchecked, or rewrote successfully on the delivered value. This is a use-based condition, not a blanket rule that every later halt cancels every earlier use. A failed checked use does not count; an unreached later use of the queried value prevents acceptance. An unrelated later failure need not do so. Put the required checks before the operation that consumes the message, and use precondition when the claim should apply only after a later send. A defeated check (Active Search) is not a use either.

A matching run is a run of Alice that represents the same actor with the same peer binding, owns the corresponding sending, and emits the delivered value once Bob’s own outgoing messages are routed into it. Session clones of one principal are always candidates; scenario bindings distinguish candidates only for values that depend on those bindings (Scenarios). Verifpal confirms a match by re-executing the candidate run. Routing Alice’s challenge to a second session of Bob and returning that session’s answer is therefore not an attack: Alice ends with one matching Bob run, nothing was forged and no sending was accepted twice. The matching-run procedure and its relation to conventional agreement properties are discussed in What a Result Establishes.

This query is an injective use-origin test. It is not Lowe’s injective agreement (Lowe 1997), and it is not a correspondence anchored at the completion of a run. Verifpal evaluates it at the point of use, so a responder that successfully processes an attacker-supplied first message fails the query even if it never completes the run. Conversely, a value the recipient never uses cannot fail it. The duplicate-acceptance search uses sibling runs introduced by sessions or scenarios; with --sessions 1 and no scenarios block, only origin failures can be detected (Sessions and Execution Histories). A trace labels an origin failure as a replacement and a duplicate acceptance as a replay (Reading an Attack Trace).

The label [duplicate acceptance] distinguishes a replay from a replacement. If the signed or encrypted flight contains no value generated by the recipient, the label adds no recipient-generated context. This often occurs on an opening message: two recipients can accept the same valid flight before either has contributed a challenge. Decide whether the protocol promises replay resistance at that point. A later acceptance event may be the appropriate claim.

A freshness experiment

In this model, ha = HASH(a) depends only on a static key and Bob uses it in ASSERT, so the first query fails. hb = HASH(b) contains a generated value and Alice uses it in a further hash, so the second query passes. Bob’s unused copy does not contribute a violation. See the freshness predicate for the successful-use condition and its limits.

attacker[active]

principal Alice[
	knows private a
	generates b
	ha = HASH(a)
	hb = HASH(b)
	_ = HASH(hb)
]

Alice -> Bob: ha, hb

principal Bob[
	knows private a
	_ = ASSERT(ha, HASH(a))
]

queries[
	freshness? ha
	freshness? hb
]

Which links count

Verifpal searches for a link witness: an equality, check or reconstruction that links two observed values. An observable value must be available to the attacker through a public declaration, leak or transmission. A component exposed by opening a transmitted container also counts, as does a tuple assembled from observed components. Merely being derivable is insufficient: a hash of a leaked seed that nobody ever published is not an observed token. A value is secret-dependent if it contains a generated or private constant.

unlinkability? c1, ..., cn (over two or more distinct constants) is contradicted if and only if some pair of the queried values passes the following gates and admits at least one of the four witnesses below:

1. each value in the pair is observable; and

2. neither queried value is marked as attacker-controlled; and

3. the honest values are equal or share a secret-dependent subterm. An equality witness must also be an equality of the honest values, and the identifying origin must not have been supplied by the attacker.

These conditions prevent an attacker from manufacturing a link by supplying the same value twice or placing a common origin on the wire. An active attack must expose a relation that the honest values already carry. The query also excludes some values emitted after attacker steering; this is one reason a passing verdict is weaker than a general unlinkability proof.

For a pair that meets those conditions, Verifpal recognizes four witnesses, and reports the first that applies:

• Observed equality. The attacker holds two equal values that depend on a secret. Equality links them directly. The secret dependency matters because a public value common to every principal, such as a hash of public constants, identifies no one.

• Identifying check. Both values satisfy the same checked primitive under a secret-dependent identifier available to the attacker. Two signatures that verify under one public key, for example, identify the same signer. The attacker can perform the check even if no principal does so in the model.

• Common secret origin. The attacker can reconstruct both values from one secret-dependent value it holds. Verifpal tests reconstruction while withholding the observed values themselves; receipt alone does not establish a common origin.

• Recognized secret. The attacker holds at least one of the values and can run a check that identifies a secret-dependent term inside it, and that term is tied to the other value by the same kind of check or as a leaf of its reconstruction. This witness links values the attacker can recognize but cannot rebuild, such as a blind signature whose blinding factor became public.

Unlinkability Queries illustrates these outcomes. The first query passes because h1, h2 and h3 depend on a, which the attacker does not obtain. The second is contradicted because the leaked c is the common origin of h4, h5 and h6. The third is contradicted because p1 and p2 both resolve to the observed value PUBKEY(d).

attacker[active]

principal Alice[
	generates b
]

Alice -> Bob: b

principal Bob[
	knows private a
	generates c
	generates d
	leaks c
	h1, h2, h3 = HKDF(a, b, nil)
	h4, h5, h6 = HKDF(c, c, nil)
	p1 = PUBKEY(d)
	p2 = PUBKEY(d)
]

Bob -> Alice: h1, h2, h3, h4, h5, h6, p1, p2

queries[
	unlinkability? h1, h2, h3
	unlinkability? h4, h5, h6
	unlinkability? p1, p2
]

Authentication may conflict with unlinkability. Two signatures verifiable under the same public key are linkable to the same signer. By contrast, a ring signature identifies only a member of the ring, not a particular member, so it does not create this witness. This distinction comes from the primitive specifications rather than a query-specific exception.

The four witnesses describe concrete attacker procedures; they do not define observational equivalence, which Verifpal does not analyze (What a Result Establishes). A passing query means that Verifpal found none of these witnesses, not that no distinguishing strategy exists.

Properties on acceptance

A precondition can tie secrecy to a send after the necessary checks. Here the client derives its session key before verifying the server’s signature, then encrypts and sends a request only after verification:

attacker[active]

principal Server[
	knows private server_sk
	server_pk = PUBKEY(server_sk)
]

Server -> Client: [server_pk]

principal Client[
	generates c
	gc = PUBKEY(c)
]

Client -> Server: gc

principal Server[
	generates s
	gs = PUBKEY(s)
	sig = SIGN(server_sk, gs)
	k_server = DH_KEX(gc, s)
]

Server -> Client: gs, sig

principal Client[
	k_client = DH_KEX(gs, c)
	_ = SIGNVERIF(server_pk, gs, sig)?
	generates request, n_req
	req = AEAD_ENC(k_client, n_req, request, nil)
]

Client -> Server: n_req, req

principal Server[
	_ = AEAD_DEC(k_server, n_req, req, nil)?
]

queries[
	confidentiality? k_client
	confidentiality? k_client[
		precondition[Client -> Server: req]
	]
]

The first query is contradicted. The attacker replaces gs with its own public key, so the client computes a key the attacker knows, and then halts at the signature check without using it. This is a true statement about a value the client discarded. The second query holds: in every execution in which the client goes on to send req, the signature verified, so gs was the server’s and the key is a two-party secret. Without the option, the only way to ask this is to query a value derived after the check, such as request, and to argue separately that the answer carries back to the key.

An equivalence query can use precondition to require completion. For example, a model with a later Server -> Client: response message could use that send as its precondition when comparing k_client and k_server. The preceding model has no such response; add the actual protocol action before querying it. The option can also condition an authentication query on the recipient’s onward action. In the following model, the intended property is that Alice sends m2 to Carol only after authenticating Bob’s ciphertext:

attacker[active]

principal Bob[
	knows private psk
	generates m
	e = ENC(psk, m)
	h = MAC(psk, e)
]

Bob -> Alice: e, h

principal Alice[
	knows private psk
	_ = ASSERT(MAC(psk, e), h)?
	m2 = DEC(psk, e)
]

Alice -> Carol: [m2]

principal Carol[
	_ = HASH(m2)
]

Add the option to the authentication query for e:

queries[
	authentication? Bob -> Alice: e[
		precondition[Alice -> Carol: m2]
	]
]

The query is contradicted if Alice accepts an unauthenticated e and still sends m2 to Carol. In this model, the attack that Verifpal reports is a duplicate acceptance: the attacker replays e and h from Bob’s other session, Alice’s MAC check passes because the pre-shared key is the same in both sessions, and Alice forwards the replayed plaintext. The trace ends with a line stating that Alice still sends m2 to Carol, so the failure counts. Had Alice halted before sending m2, the execution would fall outside the precondition and contradict nothing.

Here, m2 is guarded in transit to Carol, so a query on that message alone would not reveal the earlier failure. The precondition relates the guarded onward action to the authentication of e.

Checks, trusted keys and replay

The client asks the server to sign a fresh challenge, then sends its own signed attestation. Compare the unchecked, checked and checked-with-trusted-key variants:

attacker[active]

principal Server [
	knows private s
	gs = PUBKEY(s)
]

principal Client[
	knows private c
	gc = PUBKEY(c)
	generates nonce
]

Client -> Server: nonce

principal Server[
	proof = SIGN(s, nonce)
]

Server -> Client: gs, proof

principal Client[
	valid = SIGNVERIF(gs, nonce, proof)
	generates attestation
	signed = SIGN(c, attestation)
]

Client -> Server: [gc], attestation, signed

principal Server[
	storage = SIGNVERIF(gc, attestation, signed)?
]

queries[
	authentication? Server -> Client: proof
	authentication? Client -> Server: signed
]

Verifpal reports the following results:

Fail ✗ authentication? Server -> Client: proof
Attack trace:
| 1. Attacker observes nonce on the wire.
| 2. Attacker constructs SIGN(nil, nonce).
| 3. Attacker replaces proof (sent by Server to Client) with
| SIGN(nil, nonce). (proof was SIGN(s, nonce))
> proof (SIGN(nil, nonce)), sent by Attacker and not by Server,
is successfully used in SIGNVERIF(gs, nonce, proof) within
Client's state.
Fail ✗ authentication? Client -> Server: signed
[duplicate acceptance: no recipient-generated context]
Attack trace:
| 1. Attacker observes attestation#2 on the wire.
| 2. Attacker observes signed#2 on the wire, where it is
| SIGN(c, attestation#2).
| 3. Attacker replays attestation (Client to Server) from
| another session, where it is attestation#2.
| 4. Attacker replays signed (Client to Server) from another
| session, where it is SIGN(c, attestation#2).
| 5. Server's SIGNVERIF(gc, attestation#2, SIGN(c, attestation#2))?
| passes — the attacker controls one of its inputs.
| 6. Attacker knows nil: it is public.
> signed (SIGN(c, attestation#2)), which Client sent in another
session and not in this one, is successfully used in
SIGNVERIF(gc, attestation, signed)? within Server's state:
Client sent it once, Server accepts it twice, so agreement
is not injective.

Fail ✗ 2 of 2 queries failed.

The first trace is an origin failure. Its conclusion identifies the violated condition: Client successfully used the attacker’s proof, rather than Server’s, in SIGNVERIF. Steps 1–3 explain the construction. The attacker observes nonce, signs it with the known private value nil and substitutes the resulting signature for proof. The parenthetical term records the honest value that was replaced. The forged signature does not verify under gs, but Client does not check SIGNVERIF: it computes valid and continues regardless of the outcome, so any value counts as used.

Adding ? to the verification alone does not repair the protocol. Client now stops on an invalid signature, and the attacker instead replaces the key together with the signature:

Fail ✗ authentication? Server -> Client: proof
Attack trace:
| 1. Attacker constructs PUBKEY(nil).
| 2. Attacker observes nonce on the wire.
| 3. Attacker constructs SIGN(nil, nonce).
| 4. Attacker replaces gs (sent by Server to Client) with
| PUBKEY(nil). (gs was PUBKEY(s))
| 5. Attacker replaces proof (sent by Server to Client) with
| SIGN(nil, nonce). (proof was SIGN(s, nonce))
| 6. Client's SIGNVERIF(PUBKEY(nil), nonce, SIGN(nil, nonce))?
| passes — the attacker controls one of its inputs.
> proof (SIGN(nil, nonce)), sent by Attacker and not by Server,
is successfully used in SIGNVERIF(gs, nonce, proof)? within
Client's state.

Step 6 is a gate: a checked primitive that passed on attacker-controlled input. Because gs is unguarded in the same message, the attacker substitutes its own public key and a signature under the matching private value. Backward search derives the key substitution from the requirement that the check succeed; it does not enumerate pairs of replacements (Active Search). Guarding gs models Client having authenticated Server’s signing key before this exchange. Guarding the key without checking the signature also fails, because an unchecked Client accepts nil in place of proof.

After guarding gs and checking SIGNVERIF, the first query passes and the second still fails:

Pass ✓ authentication? Server -> Client: proof  [search exhausted at 2 sessions]
Fail ✗ authentication? Client -> Server: signed
[duplicate acceptance: no recipient-generated context]
Attack trace:
| 1. Attacker observes attestation#2 on the wire.
| 2. Attacker observes signed#2 on the wire, where it is
| SIGN(c, attestation#2).
| 3. Attacker replays attestation (Client to Server) from
| another session, where it is attestation#2.
| 4. Attacker replays signed (Client to Server) from another
| session, where it is SIGN(c, attestation#2).
| 5. Server's SIGNVERIF(gc, attestation#2, SIGN(c, attestation#2))?
| passes — the attacker controls one of its inputs.
| 6. Attacker knows nil: it is public.
> signed (SIGN(c, attestation#2)), which Client sent in another
session and not in this one, is successfully used in
SIGNVERIF(gc, attestation, signed)? within Server's state:
Client sent it once, Server accepts it twice, so agreement
is not injective.

Fail ✗ 1 of 2 queries failed.

The remaining trace is a duplicate acceptance. The attacker forges nothing. It records the attestation and signature that Client sent in its second session, whose values carry the #2 suffix, and delivers them to the first session of Server. The signature verifies because gc is long-term and shared by both sessions. Client sent this attestation once, and two Server sessions accept it. The protocol as modeled does not bind the attestation to the server’s session: nothing that Client signs depends on a value chosen by Server, so any Server session accepts a recorded attestation.

A single-session analysis cannot represent this execution because it has no second Client session to record from:

Pass ✓ authentication? Server -> Client: proof  [search exhausted at 1 session]
Pass ✓ authentication? Client -> Server: signed  [search exhausted at 1 session]

Pass ✓ All 2 queries pass.

The two verdicts for the second query do not conflict. Each is relative to its envelope, and the one-session envelope excludes every attack that needs two runs of a role (Sessions and Execution Histories). Compare a passing verdict with its envelope before drawing a conclusion from it.

Sources