Language reference

Attacker

attacker[active]

The first declaration selects active or passive. Both attackers observe network messages and derive values using the symbolic primitive rules. An active attacker can also intercept, replace and inject traffic.

Principals and prior knowledge

principal Alice[
	knows private sk
	knows public context
	generates nonce
]

A principal block describes local operations. Later blocks with the same name continue that principal’s state. A knows private value is initially available only to principals that declare it; repeat the same declaration to model a shared secret. knows public makes a value known to every principal and the attacker. Prior knowledge stays shared across sessions.

Fresh values and leaks

principal Alice[
	generates nonce
	leaks sk
]

generates creates a fresh value, private until disclosed, with a distinct copy in each session. leaks discloses a value the principal already knows to the attacker. To model delayed compromise, put the leak in a later phase.

Names, assignments and outputs

k_send, k_receive = HKDF(nil, secret, context)
tag = MAC(k_send, HASH(message))

Names use ASCII letters, digits and underscores and are case-insensitive. Constants have a global namespace and cannot be reassigned. Assignments introduce new names and require a primitive expression on the right; x = y is invalid. Nested calls are allowed. Bind multiple outputs in order, using the counts specified below.

Each argument must be available to the principal. // starts a line comment; /* … */ encloses a block comment. There are no strings, general-purpose numeric data literals, loops, mutable variables or user-defined primitives.

nil and discarded outputs

_ = SIGNVERIF(pk, message, signature)?

nil is a built-in public constant, known to the attacker. Use it for an absent context or associated-data value; it is not a secret, fresh nonce or wildcard. _ discards the name of an output while still performing the computation and any check. Each underscore creates a separate anonymous output.

Messages and guards

Alice -> Bob: [pk], signature

Messages appear between principal blocks. The sender must know each named constant, and the recipient must not already know that field. Assign primitive expressions to names before sending them. ASCII -> and Unicode → arrows are accepted.

Brackets guard one transmitted value: the attacker can observe it but cannot replace the sender’s delivered copy. This assumes authentication provided by the deployment. A guarded relay can still forward an earlier attacker-substituted input; guarding a later hop does not authenticate the value’s original source.

Checked operations

_ = SIGNVERIF(pk, message, signature)?

A trailing ? halts the principal when a check fails. It is supported by ASSERT, SPLIT, AEAD_DEC, SIGNVERIF, RINGSIGNVERIF and KEM_DECAP. Place required checks before consuming the message.

DEC, PKE_DEC and UNBLIND cannot take this suffix. An unmatched unchecked call remains an unreduced symbolic term; it does not represent a real API returning that term as plaintext.

Phases and delayed compromise

phase[1]
principal Alice[
	leaks sk
]

The model starts in phase 0. Explicit phases increase by one. A later leak can reveal earlier recorded ciphertexts, but cannot justify an attacker action before the leak. Phases do not erase keys, clear attacker knowledge or provide wall-clock timing.

Peer scenarios

scenarios[
	Alice[gpeer = gb]
	Alice[gpeer = gm]
]

Place the optional scenarios block immediately before queries. Each entry binds one principal’s prior-knowledge placeholders to declared values. Every principal and message is cloned per scenario, with a shared attacker, before session replication. This lets an honest-peer run interact with a run involving a corrupt peer.

A binding must name a constant declared with knows by that principal; it cannot bind a field sent over the network. Multiple bindings in one entry are comma-separated. Only the listed peer configurations are analyzed. Open the Lowe attack example.

Confidentiality

confidentiality? secret

Contradicted when the attacker can obtain the value a reached principal’s copy resolves to in an explored execution. A substituted value can be attacker-known even while the original honest secret remains private. The qualifier [attacker-supplied value] distinguishes that case. Query the original secret when its disclosure is your concern, or use a precondition for an accepted key.

Authentication

authentication? Alice -> Bob: proof

Checks the origin and duplicate acceptance of a value Bob successfully uses. A contradiction means that the used value does not come from Alice’s unchanged delivery or a matching run, or that one sending is successfully used by two recipient runs.

The message must be received and used inside a primitive. Required checks determine successful use; an unrelated later halt does not automatically undo an earlier use. This is an injective use-origin test, not a claim of general agreement or protocol completion. [duplicate acceptance] identifies a replay, which need not involve a forgery.

Freshness

freshness? nonce_hash

Contradicted when a principal successfully uses the queried value and its resolved term contains no generated constant. This is a structural test: it does not establish recency or reject every replay. A replayed value can still contain an old run’s generated nonce. Use authentication queries and the protocol’s actual challenge checks to investigate duplicate acceptance.

Equivalence

equivalence? k_alice, k_bob

Compares two or more distinct named values after substitution and rewriting in a principal state that holds them all. It is contradicted if eligible values differ under the symbolic equations. Values not reached because of a failed check, and failed checked outputs, are excluded. A pass alone does not show that both parties completed. This compares terms, not observational equivalence between protocols.

Unlinkability

unlinkability? token1, token2

Searches for a link witness between observable values with an honest secret-dependent relationship. Witnesses include observed equality, a shared identifying check, reconstruction from a common secret origin, and recognition of a secret tied to the other value. Attacker-manufactured relationships are excluded.

Use two or more distinct named constants. A pass means none of the supported witnesses was found; it is not a proof of indistinguishability. The manual gives the precise observability and eligibility conditions.

Query preconditions

confidentiality? k_client[
	precondition[Client -> Server: request]
]

An option on any query, not a sixth query type. It restricts contradictions to executions in which the named sender reaches that send. Use a real message sent after the required checks to state a property on acceptance.

The event is the send, not receipt. The property’s failure and the send must occur in the same execution. Several preconditions require every named send. Adding a precondition can remove contradictions; it does not strengthen the unconditional property.

ASSERT

_ = ASSERT(expected, received)?

Inputs

2

Outputs

1

Checked

Yes: ?

Assumptions

None

Compares terms for equality. Use the question mark to stop on a mismatch; discard the output when only the check matters.

CONCAT

packet = CONCAT(header, payload)

Inputs

2–5

Outputs

1

Checked

No

Assumptions

None

Builds a structured tuple. Anyone holding it can extract its components. Boundaries and nesting are preserved; this does not model ambiguous byte concatenation.

SPLIT

header, payload = SPLIT(packet)?

Inputs

1

Outputs

1–5

Checked

Yes: ?

Assumptions

None

Selects tuple components in order. The input must resolve to a suitable CONCAT; a checked call stops on malformed input. It does not flatten nested tuples.

HASH

digest = HASH(message, context)

Inputs

1–5

Outputs

1

Checked

No

Assumptions

weak

Produces a symbolic hash of its arguments, in order. Holding an ideal hash does not reveal its preimage. Repeating the same inputs produces the same term.

MAC

tag = MAC(key, message)

Inputs

2

Outputs

1

Checked

No

Assumptions

forgeable

Computes a keyed authenticator. Check a received tag with ASSERT(MAC(key, message), tag)? using the expected key and message.

HKDF

k_send, k_receive = HKDF(salt, secret, context)

Inputs

3

Outputs

1–5

Checked

No

Assumptions

None

Derives distinct output positions from a salt, input key material and context, in that order. Identical calls produce identical outputs in the same positions; new names alone do not make new keys.

PUBKEY

pk = PUBKEY(sk)

Inputs

1

Outputs

1

Checked

No

Assumptions

weak

Derives a public key from a private value. It does not publish that key. Used for signatures, public-key encryption, Diffie–Hellman and KEMs. The input cannot already be a PUBKEY or DH_KEX term.

DH_KEX

shared = DH_KEX(peer_public, my_private)

Inputs

2

Outputs

1

Checked

No

Assumptions

None

Combines the peer’s public key with your private value. DH_KEX(PUBKEY(a), b) equals DH_KEX(PUBKEY(b), a). The second argument cannot be a public key, and DH_KEX cannot be nested inside itself.

ENC

ciphertext = ENC(key, message)

Inputs

2

Outputs

1

Checked

No

Assumptions

weak, malleable

A deterministic symbolic abstraction of symmetric encryption, without explicit nonce, padding or mode. Use the malleable assumption to grant the modeled plaintext-replacement capability.

DEC

message = DEC(key, ciphertext)

Inputs

2

Outputs

1

Checked

No

Assumptions

None

Reduces DEC(key, ENC(key, message)) to message. It has no checked-failure branch and cannot take a question mark.

AEAD_ENC

ciphertext = AEAD_ENC(key, nonce, message, ad)

Inputs

4

Outputs

1

Checked

No

Assumptions

weak, forgeable

Authenticated encryption with associated data. Use a distinct generated nonce for every encryption under one key. Two distinct ciphertexts made with a reused key/nonce pair reveal their plaintexts and enable forgery under that pair. Associated data is opaque inside this symbolic term; transmit it separately if it should be observable.

AEAD_DEC

message = AEAD_DEC(key, nonce, ciphertext, ad)?

Inputs

4

Outputs

1

Checked

Yes: ?

Assumptions

None

Authenticated decryption. Key, nonce and associated data must match the encryption. Use the question mark when failure must stop the principal. Attacker decryption also requires the nonce, so send it if the real protocol exposes it.

PKE_ENC

ciphertext = PKE_ENC(recipient_pk, message)

Inputs

2

Outputs

1

Checked

No

Assumptions

weak

Encrypts for a recipient public key; decryption needs the corresponding private value. Anyone holding the public key can encrypt, so this does not authenticate the sender. The symbolic call is deterministic and has no randomness argument.

PKE_DEC

message = PKE_DEC(sk, ciphertext)

Inputs

2

Outputs

1

Checked

No

Assumptions

None

Reduces PKE_DEC(sk, PKE_ENC(PUBKEY(sk), message)) to message. It cannot take a question mark; an unmatched call remains unreduced.

SIGN

signature = SIGN(sk, message)

Inputs

2

Outputs

1

Checked

No

Assumptions

forgeable

Signs a message using a private key. Verify against the corresponding PUBKEY(sk). Repeating the same inputs produces the same signature term.

SIGNVERIF

_ = SIGNVERIF(pk, message, signature)?

Inputs

3

Outputs

1

Checked

Yes: ?

Assumptions

None

Checks the signature against the given public key and message. On success it reduces to nil, not to the signed message. The question mark enforces rejection. Trust in the public key must be established separately.

RINGSIGN

signature = RINGSIGN(sk_a, pk_b, pk_c, message)

Inputs

4

Outputs

1

Checked

No

Assumptions

forgeable

Creates a three-member ring signature. The first argument is the actual signer’s private key; the next two are the other members’ public keys. Verification identifies membership of the ring without identifying which member signed.

RINGSIGNVERIF

_ = RINGSIGNVERIF(pk_a, pk_b, pk_c, message, signature)?

Inputs

5

Outputs

1

Checked

Yes: ?

Assumptions

None

Verifies with all three ring public keys. Their order may differ from the signing call, but the keys must correspond one-to-one to the signed ring. Add the question mark to stop on failure.

BLIND

blinded = BLIND(factor, message)

Inputs

2

Outputs

1

Checked

No

Assumptions

None

Blinds a message under a secret factor so that another principal can sign the blinded term without learning the message. Keep the factor secret.

UNBLIND

signature = UNBLIND(factor, message, blinded_signature)

Inputs

3

Outputs

1

Checked

No

Assumptions

None

Converts SIGN(sk, BLIND(factor, message)) to SIGN(sk, message). The blind signature is the third argument. Anyone holding the factor, message and blind signature can unblind it. This operation cannot be checked.

KEM_ENCAP

shared, ciphertext = KEM_ENCAP(recipient_pk, seed)

Inputs

2

Outputs

2

Checked

No

Assumptions

weak

Encapsulates to PUBKEY(sk) using an explicitly generated seed. Bind the shared secret first and ciphertext second. Reusing inputs repeats outputs. A KEM does not authenticate who encapsulated; authenticate the ciphertext separately when required.

KEM_DECAP

shared = KEM_DECAP(sk, ciphertext)?

Inputs

2

Outputs

1

Checked

Yes: ?

Assumptions

None

Recovers the shared secret with the corresponding private decapsulation key. A checked call stops on a mismatched ciphertext. This deterministic symbolic interface does not model ML-KEM’s implicit rejection or probabilistic behavior.

THRESHOLD_SPLIT

s1, s2, s3 = THRESHOLD_SPLIT[2](secret)

Inputs

1

Outputs

2–16

Checked

No

Assumptions

None

Splits a secret so any t distinct shares recover it and fewer reveal nothing. The required numeric bracket carries t, from 2 through the number of bound outputs. Shares can also be used with THRESHOLD_SIGN.

THRESHOLD_JOIN

secret = THRESHOLD_JOIN(s1, s3)

Inputs

2–16

Outputs

1

Checked

No

Assumptions

None

Combines at least t distinct shares of one split. Matching partial signatures combine into SIGN(secret, message), and public share keys combine into PUBKEY(secret). Too few pieces, repeated shares, or disagreeing signature contexts leave the call unreduced.

THRESHOLD_SIGN

partial = THRESHOLD_SIGN(share, nonce, commitments, message)

Inputs

4

Outputs

1

Checked

No

Assumptions

forgeable

Produces a FROST partial signature using one share and a fresh secret nonce. At least t partials over distinct shares with the same commitments and message combine through THRESHOLD_JOIN. Reusing a nonce under one share reveals that share.

Declared weakening assumptions

ciphertext = AEAD_ENC[weak from phase 2](key, nonce, message, ad)

Bracket annotations grant a specific attacker capability. weak removes the primitive’s modeled confidentiality guarantee; forgeable permits construction without its secret argument; malleable allows an attacker holding an ENC ciphertext to replace its plaintext with a constructible value.

Only the capabilities listed on each primitive are accepted. Separate capabilities with commas; from phase N delays the immediately preceding capability. The assumption list is part of the result: Verifpal does not establish that the real primitive is broken. THRESHOLD_SPLIT[2] uses a numeric threshold instead.

Sessions and search limits

verifpal verify model.vp --sessions 3

The default is two concurrent sessions per principal; the command line accepts 1–16, within expansion limits. Generated values are distinct per session, while values declared with knows remain shared. Scenarios multiply those copies. The Workbench uses the default session count.

Read every passing verdict’s search envelope, including session and term-depth limits and any incomplete-search qualifier. An attack needing more sessions can be missed. --saturate compares successive counts until neighboring result codes agree; this is not a proof that higher counts cannot change the answer.

Reading results

A result code records query types in order: c confidentiality, a authentication, f freshness, e equivalence and u unlinkability. A 0 means no contradiction was found; a 1 means the query was contradicted.

A contradiction describes the model and Verifpal’s query predicate. A pass describes the explored search. Neither alone establishes the security of an implementation or an unbounded protocol. Preserve the version, model, assumptions, verdict qualifiers and search limits when sharing a finding.

The fixed symbolic theory omits byte lengths, timing, arbitrary algebra, implementation bugs and general mutable state. The full manual explains the limits of replay semantics and its relationship to conventional concurrent execution.

Attack traces and reports

verifpal verify model.vp --format html > report.html

Read constructions, substitutions, checks and the final query violation together. A #2 suffix denotes another session; @2 denotes another scenario. Output positions such as |1 are report notation, not model syntax.

Keep diagnostic notes such as not causally ordered or not a minimized witness attached to the trace. The command line can export a self-contained HTML report or a LaTeX report with --format tex. View an example HTML report.