Documentation / Command line and troubleshooting

Command line and troubleshooting

Run Verifpal from a terminal, save reports, automate checks and troubleshoot models.

For installation and editor setup, see the software page. In the browser, the Workbench provides verification, formatting, diagrams, downloads and shareable models without a local installation.

Command reference

Commands below assume that model.vp is in the current directory. Quote a path containing spaces. Each subcommand accepts --help; verifpal help verify gives detailed option descriptions.

verifpal verify model.vp

Analyze with the attacker declared in the file and two sessions per principal.

verifpal verify a.vp b.vp

Analyze independent models in order. An error in one does not prevent the others from being analyzed.

verifpal verify model.vp --sessions 3

Select a session count from 1 to 16, within the expansion limits.

verifpal verify model.vp --auto-queries

Temporarily replace the queries with generated confidentiality, authentication and freshness queries. The source file is unchanged.

verifpal verify model.vp --fail-on-attack

Exit with status 2 if an attack is found. Status 1 still takes precedence for a model error.

verifpal verify model.vp -q --result-code

Print only the compact code on standard output. With several models, each code is prefixed by its path. Warnings on standard error may still appear.

verifpal verify model.vp --format json

Print a JSON report. Use html for an offline web report or tex (also latex) for a LaTeX document you can compile. These formats cannot be combined with --result-code.

verifpal verify model.vp -q

Suppress progress while retaining verdicts, traces and warnings. -v adds deduction details; the two flags conflict.

verifpal verify model.vp --color never

Disable terminal color. The other choices are auto and always.

verifpal pretty model.vp

Print canonical formatting. Add --write to update the file or --check to return status 1 when formatting differs. Parsing is required; successful analysis is not.

verifpal diagram model.vp

Print a Mermaid sequence diagram. This describes the model’s declared protocol, not an attack trace, and does not validate or analyze the model.

verifpal completion bash

Print shell completions. Other supported shells are zsh, fish, elvish and PowerShell.

verifpal lsp

Start the language server over standard input and output. Editors normally launch it themselves.

verifpal about

Print version and project information. verifpal --version prints just the version.

Saving and automating results

Redirect a structured report to a new file:

verifpal verify model.vp --format html > report.html
verifpal verify model.vp --format json > report.json
verifpal verify model.vp --format tex > report.tex
tectonic report.tex

Do not redirect output to the input model’s own path: the shell truncates the destination before Verifpal reads it. Use pretty --write for in-place formatting.

The JSON report contains top-level version and ok fields and a models array. Each model has either ok: false with an error, or an analysis object with code, sessions, assumptions and queries. In a query entry, resolved: true means a contradiction was found. It does not mean that the query passed. The envelope describes search limits; subtype, when present, qualifies the finding. steps contains the structured trace.

The ok fields tell you whether analysis completed. To make a continuous-integration job fail when Verifpal finds an attack, use --fail-on-attack:

verifpal verify model.vp --sessions 2 --fail-on-attack

For a model that demonstrates an attack, check the result against its expected code. The documentation example checks preserve expected verdicts and check that each download matches its displayed fragments and documented variant edits.

Session counts and stability

Use --sessions to select 1–16 sessions per principal. The default is two; the reference explains which values each copy shares.

Start with the default of two sessions. Use --sessions 1 for an initial check if a large model is too slow. Runtime grows quickly with the number of principal copies; two sessions can take several times as long as one. Higher counts can find attacks that need three or more runs.

Each session clones every principal. The 128-principal limit described in Modeling a protocol applies after cloning. A model with 40 principals can therefore use at most three sessions. If the requested count exceeds the limit, Verifpal refuses the analysis and names a count that fits.

Comparing results across session counts

To see whether a verdict depends on the number of concurrent runs, analyze the model with explicit --sessions counts and compare the result codes. Matching codes show only that the results agree at the counts tested. A secret split into four shares that each travel in a different run, for example, holds at one, two and three sessions and is recovered at four. No finite count proves security for every number of sessions; see sessions and execution histories.

If a verdict changes between one and two sessions, at least one property depends on concurrent runs of a role. Examine the corresponding attack trace to understand that dependency.

Adding sessions gives the attacker more material. An attack found at a lower count must not disappear at a higher count. If it does, that is a bug in Verifpal rather than a property of the protocol; please report it.

Generating queries

An analysis covers only the queries in the model. The --auto-queries option temporarily replaces the model’s queries block with a generated set:

Verifpal generates the queries according to three rules:

• It asks for the confidentiality of every generated value and every value declared with knows private.

• It asks whether the recipient authenticates the declared sender for each transmitted value that the recipient later uses in a primitive.

• It asks whether each received value used in a primitive is fresh.

Verifpal does not generate unlinkability or equivalence queries because each requires a meaningful pair of values chosen by the model author. It does not generate query options either.

The option does not modify the file, and the model’s own queries block must still be present and valid because the model is validated before its queries are replaced. It may produce many unsurprising failures: a long-term public key is not fresh, for example, and a deliberately published value is not confidential. Its purpose is to reveal failures that the original query set omitted.

Before submitting a model for review, give it an explicit queries block that matches its documented security goals. Add any relevant queries found by --auto-queries and explain why they matter.

Troubleshooting

The shell cannot find Verifpal.

Run the extracted binary by its path first: ./verifpal on macOS or Linux, or .\verifpal.exe in PowerShell. If that works, add its directory to PATH and reopen the terminal. On Unix-like systems, command -v verifpal shows the selected binary; PowerShell provides Get-Command verifpal.

The model file cannot be loaded.

Check the working directory and filename. It must end in .vp; the filename, excluding its directory, must be no more than 64 characters. A Windows editor may have saved model.vp.txt. Use plain text rather than a word-processing format.

A name is unknown or already defined.

Check the spelling and the declaration order. Names are case-insensitive. An assignment or generates must introduce a new name. Several principals may repeat a compatible knows declaration to share prior knowledge.

A sender does not know a value.

The sender must declare, compute or receive that value before sending it. A similarly named value at another principal is not automatically local knowledge. A received constant cannot be delivered again to a principal that already knows it under that name.

An honest check fails.

Compare the encryption and decryption keys, nonces and associated data. Check signature-key direction and message arguments. For SPLIT, check the tuple nesting and selected output count. For KEM, confirm that the second encapsulation output is used as ciphertext. Keep a required check; correct the computation that makes it fail.

A query is rejected.

Authentication requires a transmitted value that the recipient uses in a primitive. Unlinkability and equivalence require at least two distinct names. nil cannot be queried for confidentiality or freshness. A precondition must name a message the model actually sends.

An expected attack does not appear.

Check that the attacker is active, the target message is unguarded where appropriate, the relevant peer scenario exists, and the required leak is reached. Try more sessions. Check the reported search limits. A passing query may also concern a value never used or a comparison never reached.

The editor and command line disagree.

Compare the selected binary versions, session counts and model contents. The editor may analyze an unsaved buffer while the command line reads the saved file. Check the extension’s binary-path setting and restart its language server after changing binaries.

An analysis is slow.

Try one session to locate basic modeling errors, then return to the count needed for the security claim. Reduce unnecessary scenarios and unrelated protocol actions. --auto-queries may add many questions and is not a speed option. Interrupt a terminal analysis with Ctrl-C; an interrupted run is not a passing result.

Diagnostics and performance controls

Parser and validation errors identify a line and column, underline the offending source and may add a note or suggested correction. Fix the first reported error and run again; later diagnostics may depend on it.

For a surprising active-attacker result, the following Unix-shell command saves the search log, which lists every set of substitutions the search executed:

VERIFPAL_SOLVE_DEBUG=1 verifpal verify model.vp 2> solve.log

Read the attack trace first. The debug log also lists executions that contradicted no query, and proposals whose replacements never became derivable, so that their recipients waited; these are not reported attacks. When reporting an issue, include the smallest model that reproduces it, the exact command, the version, the expected behavior and the debug log.

The native command-line engine can use worker threads. Set VERIFPAL_THREADS=1 to run sequentially or another positive count to select a pool size. Thread count affects performance. It should not change what queries mean or how many sessions are analyzed. The WebAssembly build runs without this native thread pool.

Reading older models

Older examples may use unsupported syntax. Check that each change still describes the intended protocol:

• Write PUBKEY(a) instead of the old public-key notation G^a, and DH_KEX(gb, a) for a shared-secret calculation.

• AEAD_ENC and AEAD_DEC each require four arguments: key, nonce, plaintext or ciphertext, and associated data. Choose how the real protocol obtains its nonce; inserting the same nil into every call may introduce nonce reuse.

• Replace SHAMIR_SPLIT with THRESHOLD_SPLIT[t] and SHAMIR_JOIN with THRESHOLD_JOIN. The split now requires its threshold explicitly.

• knows password and PW_HASH are no longer supported. Replacing them with a private constant and HASH would lose password-guessing behavior; it is not an equivalent migration.

• Use verify --format json instead of the removed internal-json command.

• Recheck assumptions about sessions, replay and preconditions. Current analysis defaults to two sessions, and a precondition requires its named send in the same execution as the violation.