Documentation / How analysis works

How analysis works

How Verifpal executes a model, derives attacker knowledge and searches for attacks.

A result depends on the attacker’s capabilities, the executions searched and the conditions under which a failure is recorded. This guide explains each of these. The companion paper (Kobeissi 2026) gives formal definitions of the language, the primitive rules and the queries.

From model to result

Verifpal processes a model in four stages:

1. Read the source. The parser identifies declarations, assignments, messages, phases, scenarios and queries. It reports a source location when the syntax is invalid.

2. Expand the runs. Scenarios create copies with different peer bindings. Session replication creates the requested number of runs of each principal. Generated values become distinct in each copy; long-term knowledge stays shared.

3. Check the model. Verifpal checks names, knowledge, message uses, primitive arguments, query options and phase numbers. It also evaluates the baseline computations. A failed checked primitive in a run that is honest when the check runs is a model error; a corrupt-peer run may halt legitimately.

4. Analyze and report. The engine executes the protocol honestly and computes what the attacker learns from it. When the attacker is active, it then searches for permitted message substitutions, running each candidate as a complete execution of the model. Queries are evaluated on every execution. A contradicted query receives a trace of the execution that contradicts it; a passing query receives a description of the search limits.

A parse or validation error means Verifpal could not analyze the model. Fix the error and run it again. A valid model can still describe an insecure protocol.

Attacker knowledge and search

An analysis combines three activities. Execution runs every principal of the model, in every session and scenario copy, under a chosen set of attacker substitutions. Deduction computes what the attacker can learn from what that execution discloses. Search chooses which substitutions to execute. Only an execution can contradict a query; search decides which executions to try.

Execution

An execution runs each principal copy at most once, performing its actions in the order the model declares them. The attacker may leave a copy unstarted, as though that session never began. Principals advance whenever they can, so their actions interleave. Phases are barriers: no principal performs a phase 1 action until every principal that can still move has finished phase 0.

• A computation applies the primitive rules to the values the principal holds. A failed checked primitive halts that principal, so its later values and messages do not exist in this execution.

• A send records the values the principal actually holds, and the attacker learns them.

• A guarded receive takes exactly what the sender sent. If the sender halted or has not yet reached that send, the recipient waits; if the send never happens, it waits for the rest of the execution.

• An unguarded receive takes the sender’s value unless a substitution targets it. A substituted value is delivered only when the attacker can derive it, at that moment, from what this execution has already disclosed. Until then, the recipient waits.

Queries are evaluated at the end of every phase, on the state every principal copy has reached by then and the attacker knowledge of that phase. Because each copy runs at most once and every substituted value is derived from earlier disclosures in the same execution, a later output cannot justify an earlier delivery, and the attacker cannot combine what two incompatible runs of the same principal would have revealed. No separate check has to reconstruct a consistent history afterward: the execution is that history.

Deduction

The attacker starts with public values and learns every value a principal sends or leaks during the execution. It then applies the primitive deduction rules to the available terms.

New knowledge can enable another rule: a leaked key opens a ciphertext, its plaintext supplies a hash input, and that hash may be another decryption key. Deduction continues until another pass adds nothing. This is the fixed point or knowledge closure.

The set of terms the attacker could construct is infinite: it could keep hashing public values, for example. Verifpal uses a finite set of relevant terms and checks whether others can be constructed as needed. It records how it obtained each value; the attack trace is built from these records. Knowledge belongs to one execution. What the attacker learns in one execution cannot be spent in another.

A passive attacker changes no messages. Its analysis therefore needs only the honest execution, including the declared session and scenario copies. Later phases may disclose keys that open previously recorded traffic.

Active search

An active attacker can replace permitted network inputs. Verifpal first analyzes the honest execution, then works backward from queries that remain unresolved. For a confidentiality query on an encrypted message, the search may ask how the attacker could obtain the decryption key. If the key comes from an unauthenticated Diffie–Hellman exchange, that question suggests replacing a public key.

The solver represents inputs the attacker can control as variables, then looks for values to assign to them. Some replacements must be made together: replacing an identity key without its signature would fail the recipient’s check. A compatible set of replacements is a proposal, and each proposal is run as an execution.

The search also tries patterns that a single backward goal may miss: changing one field while leaving others honest, rebuilding the inputs of a check that stopped an execution, forwarding related fields together from another session, filling in the rest of a partly replaced message, leaving one copy of a sender unstarted so that another copy’s value can be delivered in its place, and building a tuple from values the attacker already holds. If replacing an input with a variable hides a useful honest computation, a refinement restores that input and tries again. These methods can find more attacks, but still miss some.

The search pools what the attacker learned across the executions it has tried, but only to choose new proposals. A proposed value that only another execution produced is not delivered on that basis: the search runs the two sets of substitutions together, and the value is delivered only if the combined execution actually produces it first. Search ends when every query has a contradiction or when a complete round teaches the pool nothing new. Finding one counterexample is enough to fail a query; the report is not a catalog of every possible attack on it.

An execution delivers a proposed replacement only when:

• the replaced value is an unguarded network input of the receiving principal;

• the attacker can derive the replacement from what the execution has disclosed so far, subject to the primitive rules and declared assumptions; and

• the replacement satisfies the term restrictions and the depth bound.

A replacement that never becomes derivable leaves its recipient waiting. The principal’s ordinary computations and checks then determine what happens. For example, a signature the attacker cannot construct is never delivered, even if it would pass the recipient’s check.

What each principal sees

Each principal keeps its own copy of the values it knows. If the attacker changes a message from Alice to Bob, Alice retains what she sent and Bob receives the replacement. A name such as e can therefore resolve differently in their states.

The engine calls each stored local value a slot. A slot records the value before and after rewriting, which principal sent it, and whether the attacker supplied it, either directly or through an honest principal that forwarded a value it received from the attacker.

These distinctions explain several query results. A confidentiality query may concern a received replacement rather than the original secret. An authentication query asks about the accepted sending, so an honestly forwarded value must retain its sender. An equivalence query compares values that were actually reached in the same execution.

A slot is controllable only if it is an eligible received value in the phase being analyzed. Locally generated secrets cannot be replaced directly. The search considers received values used in computations and values named by equivalence queries, even when those queried values have no later primitive use.

Search limits

The active search uses these limits to keep the number of terms and executions finite:

• Session and scenario counts. The model supplies finitely many runs and peer configurations. More runs may expose an attack; no finite count establishes security for all counts.

• Term depth. Each received slot has a model-derived bound on the nesting of injected terms. The bound accounts for the depth of protocol terms and the layers the receiving principal removes from that slot. Some proposals can therefore be deeper than any honest message. Still deeper attacks remain outside the search.

• A finite term basis. The solver builds candidate terms from protocol terms, values the attacker holds and supported construction patterns. It may miss attacks that need a different term structure.

• Fixed atoms and primitives. The attacker combines constants that exist in the model; it does not invent a fresh atomic name. Each primitive has a fixed range of input and output counts. Most accept at most five; threshold splitting and joining allow up to sixteen shares or pieces.

• Search choices. Which proposals the solver generates, which executions the search keeps as sources for later proposals, and the order in which it tries them can leave possible attacks unexplored. Their effect is not measured by the session count alone.

When a proposal exceeds the depth bound, a diagnostic identifies the affected term and slot. Every query still unresolved at that point carries [search truncated: term depth] if it passes. The flag does not mean that the rejected proposal would have affected that query. A query unresolved when the solver runs out of variables carries [search truncated: solver variables] instead.

Otherwise, a pass includes a note such as [search exhausted at 2 sessions]. This means Verifpal finished its search, not that it checked every symbolic execution at two sessions. It can miss an attack requiring an unsupported term structure without issuing a truncation warning.

Reading an attack trace

A trace narrates the execution that contradicts the query and ends with the condition it violates. Read the conclusion first to identify the claimed failure, then follow the steps that support it. Substitutions appear in the order the execution delivered them, each after the observations and deductions that let the attacker build it; the deductions behind the final violation come last.

• Observations and leaks show which values the attacker obtains. A leak names the principal copy whose leaks declaration disclosed the value.

• Constructions and decompositions show what the attacker computes or opens. A step that uses a weakening assumption names it. Terms are written with the model’s names. When a named value differs in this execution from its honest value, the step also spells it out, as in constructs gab, where it is DH_KEX(gb, nil).

• Replacements identify the delivery, the substituted value and the honest value it displaced. If the substituted value equals the honest one, the note instead gives what the sender actually sent in this execution, or states that it did not send the message.

• Replays deliver a value that another session or scenario copy actually sent in the same execution. The signature or ciphertext may be perfectly valid; the failure is accepting one sending twice.

• Unstarted copies are stated first, as in Alice#2 never starts a session in this execution. A copy that never runs sends nothing, so a value that another copy sent can be replayed in its place.

• Gates mark a checked operation that passed on an attacker-influenced input, at the point where the principal performed it.

• Resolutions, receipts and static values explain term inequality, a value’s origin or the absence of generated material. These findings may need no attacker action.

HTML and LaTeX reports also show these steps in an attack diagram, with the same numbers as the text trace. The compact result code records only pass or fail; it omits the explanation and any subtype qualifier.

Reducing a trace

The execution that first contradicts a query may carry substitutions it does not need, such as changes made for another query. Before reporting a failure, Verifpal removes one substitution at a time, or two from the same message, runs the execution again and keeps each removal while the same query still fails in the same phase. It repeats until nothing more can be removed, then narrates the resulting execution.

The reported trace is minimal only with respect to these removals; a different set of substitutions might explain the same failure more simply. The chosen execution and its step order may change between versions even when the same query fails.

What a result establishes

A reported failure is a violation of the query’s defined condition in one execution of the model: each principal copy ran at most once, and every substituted value was derivable from what that execution had already disclosed. The trace narrates that execution. Only the query evaluator, applied to an execution, records a failure. The solver can miss attacks, but a solver defect alone cannot report one.

A result can still be wrong if the parser, primitive rules, executor or query definitions contain defects. The model can also misrepresent the implementation: an execution of the model is a symbolic execution of what the model says, not of the deployed code.

Sessions and execution histories

Session replication gives each run its own generated values and shares long-term knowledge. Assignments with different session names may still compute equal terms from shared inputs.

In one execution, each session copy runs at most once with its own generated values; nothing restarts a run or reuses its nonce in a second history, and a copy the attacker leaves unstarted takes no action at all. The attacker can route messages between copies: an unguarded receive may take a value that another copy sent, and the trace labels such a delivery a replay. Copies of the same principal share long-term keys, so one copy can supply a value, or reach a leak, that another copy needs. The search tries many executions, but a finding always comes from one of them.

Check a finding by reconstructing each participant’s actions from the trace, including which copy sent and received each value, and comparing them with the query’s exact condition.

For choosing a session count and comparing successive counts, see the command-line guide.

What the model leaves out

The language also limits what a model can represent:

• The fixed primitive theory cannot express arbitrary XOR equations, pairings, nested group exponents, invalid-curve behavior or user-defined cryptography.

• The language does not model byte lengths or impose a type discipline. A symbolic type-confusion attack may depend on substituting values whose concrete encodings are incompatible. Represent relevant tags and checks, and compare the trace with the actual wire format.

• Ideal primitives omit timing, probabilities, implementation bugs and most details of randomness generation. Explicit nonce reuse and weakening assumptions cover specified failures, not every failure of the real primitive.

• A model contains no general loop, mutable database, replay cache or key-erasure command. Write the relevant bounded actions explicitly, and disclose only the state that a modeled compromise actually exposes.

If you need an unbounded proof, behavioral equivalence or algebra outside Verifpal’s language, use a verifier that supports it. To compare results across tools, first check that their models, assumptions and queries mean the same thing.

Sources