Documentation / Writing security queries

Writing security queries

Write queries for the properties your protocol needs, including when a message is accepted and whether it can be replayed.

The reference defines the five queries and their syntax. This guide explains how authentication queries handle message use and matching runs, what counts as a link between values, and how to write claims that depend on acceptance.

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

An authentication query checks whether the recipient successfully uses a value and whether it came from a matching sender run.

For authentication? Alice -> Bob: e1, let $U$ be the set of Bob’s computed slots whose values contain e1 at any depth. A slot stores a local value. 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.

A failed checked use does not count. If execution stops before a later use of the same value, acceptance fails too. An unrelated later failure need not cancel an earlier successful use. Put required checks before the operation that consumes the message, and use precondition if the claim should apply only after a later send.

A matching run is a run of Alice that represents the same actor with the same peer binding and, in the same execution, actually sends the delivered value in the corresponding message toward a run of Bob, directly or through principals that forward it. Session clones of one principal are always candidates; scenario bindings distinguish candidates only for values that depend on those bindings (Scenarios). Because every run takes part in the same execution, what a matching run sends already reflects the messages that Bob’s runs delivered to it.

Routing Alice’s challenge to a second session of Bob and returning that session’s answer is therefore not an attack: Alice has one matching Bob run; no message was forged or accepted twice. What a result establishes explains what such an execution does and does not show.

A value that Alice would have sent counts only if a matching run actually sent it. If the attacker diverts or halts Alice’s run, or never starts it, and delivers that value to Bob itself, Bob’s acceptance fails the query even though the value is the honest one. Reflection fails for the same reason: when another session of Bob answers Bob’s own challenge and the attacker delivers that answer to Bob as Alice’s response, no run of Alice sent it.

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] marks a replay. If the signed or encrypted message contains no value generated by the recipient, the trace adds no recipient-generated context. This often happens with an opening message: two recipient runs can accept it before either has sent a challenge. The attacker may also leave one of the sender’s sessions unstarted, so a value that is the same in every session, such as a MAC over long-term constants, can be accepted by two recipient runs although only one sender run sent it. If the protocol promises replay resistance only after a later step, use a send after that step as the precondition.

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. Against an active attacker the query also fails when two runs of one principal accept the same delivered value, such as a signed nonce replayed from another session. 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 recovered from a transmitted value also counts, as does a tuple built from observed components. A value the attacker can compute is not necessarily observable: for example, a hash of a leaked seed that nobody published does not count. 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 meets all of the following conditions and has 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 exclude links created solely by the attacker, such as supplying the same value twice or transmitting a common origin. An active attack must reveal a relationship already present in the honest values. The query also excludes some values produced after attacker interference, so a pass does not establish general unlinkability.

For an eligible pair, Verifpal reports the first of these four witnesses that it finds:

• 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.

The example below shows three 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. The primitive rules define this distinction.

A pass means Verifpal found none of these four witnesses. It does not rule out every way to distinguish executions; Verifpal does not analyze observational equivalence.

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. The failed query concerns the discarded key. 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 a precondition, you would need to query a value derived after the check, such as request, then explain separately what that result implies about 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. If Alice stopped before sending m2, this execution would not satisfy the precondition and would not fail the query.

The guard on m2 prevents substitution on the way to Carol, but says nothing about the earlier authentication of e. The precondition lets the query check that earlier authentication in runs where Alice sends m2.

Checks, trusted keys and replay

The client asks the server to sign a fresh challenge, then sends its own signed attestation. Start with unchecked signatures, then add signature checks and a trusted key:

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 replays attestation (Client to Server) from another
| session, where it is attestation#2.
| 2. Attacker replays signed (Client to Server) from another
| session, where it is SIGN(c, attestation#2).
| 3. Server's SIGNVERIF(gc, attestation#2, SIGN(c,
| attestation#2))? passes — the attacker controls one of its
| inputs.
> 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, proof (sent by Server to Client) with
| PUBKEY(nil), SIGN(nil, nonce). (gs was PUBKEY(s); proof was
| SIGN(s, nonce))
| 5. 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 5 is a gate: a checked primitive that passed on attacker-controlled input. Because gs is unguarded in the same message, step 4 substitutes the attacker’s 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 replays attestation (Client to Server) from another
| session, where it is attestation#2.
| 2. Attacker replays signed (Client to Server) from another
| session, where it is SIGN(c, attestation#2).
| 3. Server's SIGNVERIF(gc, attestation#2, SIGN(c,
| attestation#2))? passes — the attacker controls one of its
| inputs.
> 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 one-session analysis passes because it cannot represent this replay. The two-session analysis fails because it can. Always keep the session count with the result. See sessions and execution histories for the other limits.

Sources