Documentation / How analysis works

How analysis works

Follow attacker deduction, active search and validation, and understand the evidence and limits of a Verifpal result.

A Verifpal report answers a question about a model. To judge the answer, you need to know what the attacker was allowed to do, which executions the search considered, and what evidence supports each failure. This guide explains those points. The companion paper (Kobeissi 2026) gives the formal definitions.

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 an honest run is a model error; a corrupt-peer run may halt legitimately.

4. Analyze and report. The engine computes what the attacker can learn, searches for permitted message substitutions when the attacker is active, and evaluates the queries. A contradicted query receives a trace; a passing query receives a description of the search limits.

A parse or validation error is different from an attack. It means the model could not be analyzed as written. Conversely, a well-formed model may describe an insecure protocol: finding that insecurity is the purpose of analysis.

Attacker Knowledge and Search

Verifpal separates deduction from the search for message substitutions. Deduction asks what follows from information already available. Search asks which changes to a protocol execution might reveal more information or contradict a query. The following sections explain how deduction, search and validation interact.

Deduction

The attacker starts with public values, recorded traffic and reached leaks, 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.

A fixed point does not mean that the engine has written down every term the attacker could ever construct. There are infinitely many hashes of public values. Verifpal works with a finite set of relevant terms and tests construction as needed. Each deduction records where its inputs came from so that later validation and the attack trace can follow the dependency.

A passive attacker changes no messages. Its analysis therefore needs only the baseline execution at each phase, 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 runs the passive analysis, 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.

During this backward reasoning, controllable inputs are variables. A solution assigns concrete terms to some of them. Several assignments may be needed together: replacing an identity key without also replacing its signature would fail the recipient’s check. The solver combines compatible assignments into a proposal.

The search also tries useful patterns that a single backward goal may miss: changing one field while leaving others honest, satisfying a recipient’s checks, carrying a sibling session’s related fields together, 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 choices improve coverage; they do not enumerate every possible attack.

After a proposal is validated, the attacker may learn something new. Search then repeats with the larger knowledge set. A phase ends when every query has a contradiction or when a complete search round adds no knowledge and finds no new contradiction. Finding one counterexample is enough to fail a query; the report is not a catalog of every possible attack on it.

Validation

The solver cannot record a verdict. It proposes substitutions, which a separate validator checks and executes. A proposed signature under an unknown private key must be rejected even if installing it would make the recipient’s signature check pass.

The validator checks that:

• each changed value is a network input the attacker may control;

• the attacker can derive each replacement, subject to the primitive rules and declared assumptions;

• the replacement was available at the relevant delivery, not obtained only in a later phase or from an action that depends on that delivery;

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

• the resulting computation can execute without circular definitions or incompatible dependencies.

The principal then runs with the substitutions in place. Its ordinary computations and checks determine what happens. A failed check stops that principal, so later values and messages from that run are unavailable. Queries are evaluated on the state actually reached.

Two constraints deserve particular attention. Causal availability prevents a later output from being used to make the earlier check that enabled it succeed. History coherence prevents deductions from freely combining inconsistent executions of the same run. For example, Alice cannot both disclose a nonce under an attacker-chosen key and, in an incompatible execution of that same run, supply the honest ciphertext needed to exploit that nonce. These checks apply to substitutions, forwarded values and deductions that combine information from several runs.

Defeating a Check

The engine can also examine whether a failed check could be made to accept using an attacker-held key. This is called a guard bypass in the analysis code and some traces. It concerns a checked primitive; it does not give permission to overwrite a message protected by square brackets.

The key alone is insufficient. The attacker must also obtain the other constrained inputs, such as the signed message, or an AEAD nonce and associated data. Availability is checked at the check’s own position. A later leak cannot defeat an earlier check. Nor does defeating a check count as a forgery when restoring the honest input would already pass it.

A bypass represents the consequences of the attacker’s ability to provide an accepted value. The trace distinguishes it from a gate, where the displayed substituted term itself passes the check. The bypassed operation is not itself counted as successful use of its failed input; a later use may matter to a query. When reading a trace, follow the supplied value into that later computation.

What Each Principal Sees

A principal computes with its own values. 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. It keeps the original value, the value after substitution but before rewriting, and the resolved value after rewriting. It also records who created and sent the value, whether the attacker influenced it, and whether a check was bypassed. This record is its provenance.

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 must compare values that were actually reached in a compatible 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 must consider finitely many terms and executions. Several limits make that possible:

• 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. When the solver needs a complete shape, it draws from protocol terms, held terms and the supported construction patterns. A useful shape outside that basis may be missed.

• 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. Memoization, cycle detection, refinement choices and derivation filtering 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 passing query in that run then carries [search truncated: term depth]. This is a run-wide warning; it need not mean that the rejected proposal would affect every query.

Otherwise, a pass carries an envelope such as [search exhausted at 2 sessions]. Here exhausted means that Verifpal finished the search it defines. It does not mean that it enumerated all symbolic executions at two sessions. In particular, a missing term shape need not trigger a truncation warning.

Reading an Attack Trace

A trace lists attacker actions and ends with the condition that contradicts the query. Read the conclusion first to identify the claimed failure, then follow the steps that support it.

• Observations and leaks show where the attacker gets its ingredients.

• Constructions and decompositions show what the attacker computes or opens. A step that uses a weakening assumption names it.

• Replacements identify the delivery, the substituted value and the honest value it displaced.

• Replays identify a value obtained from another run. The signature or ciphertext may be perfectly valid; the failure is accepting one sending twice.

• Gates and bypasses explain why a checked operation does not stop the attacked execution.

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

The HTML and LaTeX reports draw the same steps as an attack diagram (HTML reports; LaTeX reports). The diagram’s numbers correspond to the text trace. The compact result code records only pass or fail and discards this explanation, including any subtype qualifier.

Witness Reduction and Diagnostic Notes

A solver proposal may contain changes that another query needed. Before reporting one contradiction, Verifpal tries simpler candidates and removes substitutions while checking that the contradiction still occurs. It tests the candidate against attacker knowledge available from the passive baseline and earlier justified steps. A grounded witness has replacements that the attacker can derive in that order.

The result is a reduced witness, not necessarily the smallest possible one: the reducer does not compare every subset of substitutions. Exact step order or the chosen witness may change between versions even when the same query fails.

Two diagnostic notes require closer inspection. A trace marked not causally ordered reproduces the query failure, but its displayed substitutions were not all derived in their listed order. A trace marked not a minimized witness records the search substitutions because reduction did not independently reproduce the failure. These notes describe the evidence the report could produce, and must remain attached when sharing it. Reduce such a model and report the case with its version and session count. The example checks reject both diagnostic notes.

What a Result Establishes

Validation establishes a narrower fact than an informal claim that a deployed protocol is secure. The reported state passes Verifpal’s validation rules and contradicts the query predicate defined in Writing security queries. A defect in the solver alone cannot bypass that validation path and record an arbitrary failure.

This separation does not prove the parser, primitive table, validator or query definitions correct. It also does not establish that the model faithfully describes an implementation. The companion paper distinguishes validation in Verifpal’s replay semantics from a proof about conventional concurrent execution (Kobeissi 2026).

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.

The search re-executes a principal from its baseline state under proposed inputs, propagates the values it sends, and accumulates justified attacker knowledge. Re-executing a session reuses that session’s nonce; it does not create a third session. Checks on causal order and compatible histories restrict how the accumulated knowledge can be used.

Earlier versions reported attacks by combining incompatible histories or failing to recognize an honest matching run. Regression models now cover the corrected cases. These safeguards should not be mistaken for a proof that replay search is equivalent to every interleaving in which each session executes once. The paper states that this correspondence is neither proved sound nor proved complete. Derivation filters follow selected recorded routes, and matching-run reconstruction examines particular routings. For a finding that matters, reconstruct the participants’ actions from the trace and check the exact query predicate.

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

Declared Assumptions and Implementation Scope

Other boundaries apply to every model:

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

Use Verifpal to examine concrete design questions and produce inspectable counterexamples. When the task requires an unbounded proof, behavioral equivalence or algebra outside this language, select a verifier that can state and analyze that property. Comparing results across tools is useful only after aligning their models, assumptions and query meanings.

Sources