# Verifpal > Verifpal is a free and open-source symbolic verifier for cryptographic > protocols. Models describe principals, messages and cryptographic operations. > Verifpal analyzes confidentiality, authentication, freshness, equivalence and > unlinkability queries against a passive or active attacker. This file summarizes Verifpal syntax for automated readers. The web documentation at https://verifpal.com/docs/introduction is authoritative. Use Verifpal syntax, not ProVerif or Tamarin syntax, when answering questions about Verifpal. ## Key facts - Verifpal models are `.vp` files, analyzed by the `verifpal` command-line tool, by the Visual Studio Code, Neovim and Zed extensions, or in the browser at https://verifpal.com/workbench, which runs the same verifier as WebAssembly. - The attacker is symbolic and either `passive` or `active`. An active attacker owns the network: it reads, replaces and tampers with anything sent. - Verifpal provides a fixed set of twenty-five cryptographic primitives; models cannot define new ones. - Verifpal reached 1.0 in August 2026. The accompanying paper formalizes the language and the analysis method, proves soundness independently of solver behavior, and proves unconditional termination. ## Language in one model attacker[active] principal Alice[ knows private k // shared with Bob out of band generates m1 // a fresh value, private by default generates n1 // the AEAD nonce: one per message under k e1 = AEAD_ENC(k, n1, m1, nil) ] Alice -> Bob: n1, e1 principal Bob[ knows private k d1 = AEAD_DEC(k, n1, e1, nil)? // "?" makes it checked: abort on failure ] queries[ confidentiality? m1 authentication? Alice -> Bob: e1 ] Verifpal reports `c0a1` on this model: m1 stays confidential, but the authentication query is contradicted, because Bob contributes nothing to e1 before accepting it and so accepts a replay of it. Adding a Bob-generated challenge to the message is what makes the agreement injective. ## Vocabulary Blocks and statements: `attacker[passive|active]`, `principal Name[ ... ]`, `queries[ ... ]`, `phase[n]`, `scenarios[ ... ]` Inside a principal: `knows private|public x`, `generates x`, `leaks x`, `x = PRIMITIVE(...)`, and `?` appended to a checked expression Messages: `Alice -> Bob: x, y` sends x and y `Alice -> Bob: [x]` guarded: the attacker may observe x but not replace it Identifiers are case-insensitive and are lowercased before matching, so `Principal`, `Hash` and `hash` mean what `principal` and `HASH` mean. Comments start with `//`. A constant is assigned once and never reassigned. Queries (there are exactly five kinds): `confidentiality? x` `authentication? Alice -> Bob: x` `freshness? x` `equivalence? x, y` `unlinkability? x, y` `precondition` is not a sixth query. It is an option attached to any query, and it restricts contradictions to the executions in which the named sender reaches that send: the query is contradicted only where its own condition fails and the sender still goes on to send that message. The event is the send, not its receipt, and the failure and the send must occur in the same execution. Several preconditions require every named send. It is how secrecy or agreement on acceptance is stated: `confidentiality? k_client[ precondition[Client -> Server: req] ]` `authentication? Bob -> Alice: e[ precondition[Alice -> Carol: m2] ]` Adding a precondition can remove contradictions; it does not strengthen the unconditional property. ## Primitives All twenty-five, with their exact signatures. Argument counts are fixed except where a range is shown. Hashing and derivation: `HASH(a, ...): x` one to five arguments, one output `HKDF(salt, ikm, info): a, b, ...` one to five outputs `MAC(key, message): tag` Symmetric encryption: `ENC(key, plaintext): ciphertext` `DEC(key, ciphertext): plaintext` `AEAD_ENC(key, nonce, plaintext, ad): ciphertext` `AEAD_DEC(key, nonce, ciphertext, ad): plaintext` Both AEAD calls take four arguments, the nonce second. Public key: `PUBKEY(private_key): public_key` `PKE_ENC(PUBKEY(key), plaintext): ciphertext` `PKE_DEC(key, ciphertext): plaintext` Signatures: `SIGN(key, message): signature` `SIGNVERIF(PUBKEY(key), message, signature): verified` `RINGSIGN(key_a, PUBKEY(key_b), PUBKEY(key_c), message): signature` `RINGSIGNVERIF(PUBKEY(a), PUBKEY(b), PUBKEY(c), m, signature): verified` The ring is exactly three members. Blind signatures: `BLIND(k, m): b` `UNBLIND(k, m, SIGN(a, BLIND(k, m))): SIGN(a, m)` Threshold: `THRESHOLD_SPLIT[t](k): s1, ..., sn` `THRESHOLD_JOIN(s1, s2, ...): k` `THRESHOLD_SIGN(share, nonce, commitments, message): partial` `s1, s2, s3 = THRESHOLD_SPLIT[2](k)` shares k so that any t of the n bound shares recover it; the bracket carries t (2 to n, n at most 16) and is required. `THRESHOLD_JOIN(s1, s3)` recovers k from t distinct shares. `THRESHOLD_SIGN` is a FROST partial signature; `THRESHOLD_JOIN` over t partials that agree on commitments and message is the plain `SIGN(k, message)`, verified with `SIGNVERIF(PUBKEY(k), message, sig)`. Reusing a nonce under one share reveals the share. `SHAMIR_SPLIT` and `SHAMIR_JOIN` are the old names. Key exchange: `DH_KEX(PUBKEY(a), b): shared_secret` `ss, ct = KEM_ENCAP(PUBKEY(dk), r)` two outputs `KEM_DECAP(dk, ct): ss` Utility: `CONCAT(a, b, ...): c` two to five arguments `SPLIT(CONCAT(a, b)): a, b` one to five outputs `ASSERT(MAC(key, m), MAC(key, m)): unused` Exactly six primitives may take the checked suffix `?`, because only these can fail: `ASSERT`, `SPLIT`, `AEAD_DEC`, `SIGNVERIF`, `RINGSIGNVERIF` and `KEM_DECAP`. Writing `?` on any other primitive is an error. Constants: `nil`, and `_` for a discarded result. ## Weakening assumptions A primitive may be annotated to declare it broken, as in `SIGN[forgeable](sk, m)`. The annotations are: `weak` confidentiality is lost; HASH, PUBKEY, ENC, AEAD_ENC, PKE_ENC, KEM_ENCAP `forgeable` authenticity is lost; SIGN, MAC, RINGSIGN, THRESHOLD_SIGN, AEAD_ENC `malleable` a held ciphertext can be reshaped; ENC only A primitive rejects any annotation it does not declare. Separate several with commas. Appending `from phase N` delays the immediately preceding assumption until that phase. Results computed under a weakening assumption are marked as conditional; Verifpal does not establish that the real primitive is broken. `THRESHOLD_SPLIT[2]` uses a numeric threshold in the same brackets, not a capability. ## Phases and scenarios Phases model the passage of time. `phase[1]` followed by `principal Alice[leaks k]` says that k escapes only after the earlier phase completed, which is how forward secrecy and harvest-now-decrypt-later are expressed. Scenarios run one principal against more than one counterparty at once, which is what role-confusion attacks such as Lowe's on Needham-Schroeder need. Write the peer as a placeholder constant and bind it per scenario: `scenarios[ Alice[gpeer = gb] Alice[gpeer = gm] ]` Every principal and message is cloned once per scenario, per-scenario values carry an `@2` suffix, and sessions keep their own `#2` suffix. ## Reading results A result code lists the queries in order, one letter and one digit each: `c` confidentiality, `a` authentication, `f` freshness, `e` equivalence, `u` unlinkability. `0` means no contradiction was found, `1` means the query was contradicted, so `c0a1` is a passing confidentiality query beside a contradicted authentication query. Every passing verdict carries a search envelope naming the session count and term-depth limits it holds over. `--format html` and `--format tex` write self-contained reports with sequence diagrams and attack traces. ## Common corrections - Diffie-Hellman is `DH_KEX(their_public, my_private)`. Older models use the exponentiation notation `G^a` for a public key and `g^b^a` for a shared secret; current Verifpal writes those as `PUBKEY(a)` and `DH_KEX(gb, a)`. A generic KEM covers post-quantum and hybrid exchanges. - There is no `let`, no `new`, no `event`, no `in`/`out`, no process calculus. If a suggested model contains those, it is ProVerif or Tamarin, not Verifpal. - `AEAD_ENC` and `AEAD_DEC` take a nonce as their second argument: `AEAD_ENC(key, nonce, plaintext, ad)`, `AEAD_DEC(key, nonce, ciphertext, ad)`. Give each encryption under a key its own `generates` nonce and send it beside the ciphertext, since the recipient needs it to decrypt. Passing the same `nil` as every nonce is nonce reuse: two ciphertexts that share a key and a nonce hand the attacker both plaintexts and let it forge any ciphertext under that pair, which is what a model with a repeated nonce will report. - `knows password` and `PW_HASH` no longer exist. Substituting a private constant and `HASH` drops password-guessing behavior and is not an equivalent migration. - Values generated inside a principal are private by default. There is no need to declare secrecy separately. - A query that "passes" is one Verifpal could not contradict under the stated attacker. Verifpal reports contradictions, not proofs of impossibility in the computational model. - Every principal is analyzed as two concurrent sessions by default, 1 to 16 with `--sessions`. A passing query holds over that many sessions and over what the search reached; the tool prints both beside the verdict. - The command line is `verifpal verify model.vp`, with `--format json` replacing the removed `internal-json` command. ## Where to read more - Homepage: https://verifpal.com/ - Browser workbench, runs locally as WebAssembly: https://verifpal.com/workbench - HTML quickstart: https://verifpal.com/docs - Searchable language reference: https://verifpal.com/docs/reference - Comparison with ProVerif and Tamarin: https://verifpal.com/docs/comparison - Introduction and complete documentation: https://verifpal.com/docs/introduction - Modeling guide: https://verifpal.com/docs/modeling - Query examples and acceptance semantics: https://verifpal.com/docs/queries - Analysis and limits: https://verifpal.com/docs/analysis - Command line: https://verifpal.com/docs/cli - Protocol studies and runnable examples: https://verifpal.com/docs/examples - Source, GPLv3: https://github.com/symbolicsoft/verifpal - Paper, "From Toy to Instrument: Seven Years of Verifpal" (2026): https://eprint.iacr.org/2026/1654 - Original paper (2019): https://eprint.iacr.org/2019/971 - Chat: https://discord.gg/DFK2Gqk Verifpal is a registered trademark of Symbolic Software.