Documentation / Command line and troubleshooting

Command line and troubleshooting

Run reproducible analyses, export reports, automate checks, diagnose models and migrate older Verifpal syntax.

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 --saturate

Compare counts 2, 3 and, if needed, 4. This overrides --sessions and stops at the first repeated code.

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

Emit a machine-readable report. Use html for an offline web report or tex (also latex) for a compilable LaTeX document. These formats conflict 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 has a top-level version, ok and models array. A model with ok: false carries an error; a successfully analyzed model carries analysis, including its 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 report’s ok fields concern successful analysis, not the absence of attacks. In a continuous-integration job, use --fail-on-attack for the latter:

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

A model intended to demonstrate an attack should instead retain its expected result 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.

Most analyses can use the default. Use --sessions 1 if a large model is too slow; cost grows steeply with the number of replicated principals, and a two-session analysis of a mid-sized model costs several times as much as a single-session analysis. A higher count can find attacks that require three or more sessions, but it also increases the cost.

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.

Testing verdict stability across session counts

--saturate overrides --sessions, compares counts 2, 3 and then 4, and stops at the first neighboring pair with equal result codes. It reports only the final run, with an Info line stating the outcome:

If the verdicts were still changing at four sessions, the line says so instead. This result is empirical, not a proof. It states only that the verdicts did not change over the counts examined. Because the ladder stops at the first repeated code, an attack that first requires four runs is missed when two and three sessions read alike, and nothing above four is examined. A claim about a particular count therefore requires an explicit --sessions run rather than an inference from --saturate. No finite session count removes the bound of 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, Verifpal warns on standard error that the result indicates an analysis error rather than a protocol property.

Generating Exploratory 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.

Use generated queries to explore a model, not as a substitute for a deliberate specification. A model submitted for review should contain a curated queries block whose entries correspond to documented security goals. If a generated query reveals a relevant failure, add that query explicitly and document why it matters.

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. Inspect the search envelope. 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; --saturate runs several analyses. Neither is 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 solver’s proposals, including rejected ones:

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

A proposal is not an attack until validation accepts it and a query fails. The debug log is useful when reporting an issue, but the ordinary trace is the explanation to read first. Include the smallest model that reproduces the problem, the exact command, the version and the expected behavior. The issue tracker is at https://github.com/symbolicsoft/verifpal/issues.

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 controls execution cost; it does not change the intended query semantics or session count. The WebAssembly build runs without this native thread pool.

Reading Older Models

Older examples may use syntax that current Verifpal rejects. Review the protocol meaning as well as replacing spellings:

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